# Number of subspaces of dimension d in F^n, if |F|=q

grassmann_count := (q::posint) -> proc(n,d)
 local i;
 return mul(q^(n-i)-1,i=0..d-1)/mul(q^(d-i)-1,i=0..d-1);
end:

# Number of splittings of F^(n+m) as a sum of subspaces of
# dimensions n and m, if |F| = q.

splitting_count := (q::posint) -> (n,m) ->
 grassman_count(q)(n+m,n) * q^(n*m);

# tanabe_N(p,n,r)(k) is the number of irreducible F-linear representations
# of Z_p^n that have dimension p^k over F.

tanabe_N := (p,n,r) -> (k) -> `if`(k = 0,p^(n*r),(p^n-1) * p^((n-1)*k + n*(r-1)));

# The socle of K^0(BGL_{p^k}(F)) is generated by
# euler(V)^{N-1}, where N = tanabe_N_bar(n,v,k)

tanabe_N_bar := (p,n,r) -> proc(k)
 local j;
 p^(n*r) + (p^n-1)*p^(n*(r-1))*sum(p^((n-1)*j),j=1..k);
end:

tanabe_N_star := (p,n,r) -> proc(k)
 local j;
 p^(n*r-1) * (p-1) * sum(p^((n-1)*j),j=0..k-1);
end:

tanabe_N_lim := (p,n,r) -> (k) -> p^(n*r+n*k-k) * (1-p^(-n))/(1-p^(1-n));

# The natural numbers can be partitioned as the disjoint union of
# the sets tanabe_NN(p,n,r)(k), of size tanabe_N(p,n,r)(k).

tanabe_NN := (p,n,r) -> proc(k::nonnegint)
 local i;
 if k = 0 then
  return [seq(i,i=0..tanabe_N_bar(p,n,r)(0)-1)];
 else
  return [seq(i,i=tanabe_N_bar(p,n,r)(k-1)..tanabe_N_bar(p,n,r)(k)-1)];
 fi;
end:

# tanabe_s(p,n,r)(m) is the unique k such that m lies in tanabe_NN(p,n,r)(k).
tanabe_s := (p,n,r) -> proc(m)
 local k;
 k := 0;
 while m >= tanabe_N_bar(p,n,r)(k) do
  k := k+1;
 od;
 return k;
end:

# tanabe_X(p,n,r)(k) is the set of generators for E^0(BGL_*(F)) in
# degree p^k.

tanabe_X := (p,n,r) -> proc(k)
 local j;
 return [seq(c[p^k] ^ j, j = 0..tanabe_N(p,n,r)(k)-1)]; 
end:

# tanabe_prim_gen(p,n,r)(k) is a generator for the primitives
# in K^0(BGL_*(F)) in degree p^k
tanabe_prim_gen := (p,n,r) -> (k) -> c[p^k] ^ tanabe_N_bar(p,n,r)(k-1);

# tanabe_soc_gen(p,n,r)(k) is a generator for the socle of
# K^0(BGL_{p^k}(F))
tanabe_soc_gen  := (p,n,r) -> (k) -> c[p^k] ^ (tanabe_N_bar(p,n,r)(k) - 1);

# tanabe_m(p)(k) has p-adic valuation k and divides
# tanabe_m(p)(k+1).  Moreover, any positive integer n divides
# tanabe_m(p)(k) when k is sufficiently large.

tanabe_m := (p) -> proc(k) 
  local m,i;
  m := 1;
  i := 1;
  while ithprime(i) <= p + k do
    m := m * ithprime(i) ^ k;
    i := i + 1;
  od:
  return m;
end:

check_tanabe_m := proc(p,k)
  _ASSERT(padic_val(tanabe_m(p)(k),p) = k,
          "v_p(m[k])");

  _ASSERT(type(tanabe_m(p)(k+1)/tanabe_m(p)(k),posint),
          "m[k] divides m[k+1]");
end:

# Given a polynomial f over the integers and a prime q, return
# the first irreducible factor of f mod q, in the standard
# Maple order.

first_factor := proc(f,q)
 local F;
 F := :-Factor(f) mod q;
 if type(F,`*`) then F := [op(F)] else F := [F]; fi:
 F := sort(map(g -> `if`(type(g,`^`),op(1,g),g),F));
 return F[1];
end:

# Return an irreducible polynomial f[k](x) of degree v0 * p^k over
# Z/q0.  This gives a field F(k) of degree p^k over F = F(0),
# where F(0) has order q = q0 ^ v0.  The polynomials are arranged
# so that the canonical primitive element x[k] in F(k) generates
# the group of units, and there is an inclusion F(k) -> F(k+1)
# sending x[k] to x[k+1] ^ m, where m = |F(k+1)^x|/|F(k)^x|.
tanabe_FF_poly := (q0,v0,p) -> proc(k::nonnegint)
 option remember;
 local q,m,f;

 q := q0 ^ v0;
 if k = 0 then 
  f := NumberTheory[CyclotomicPolynomial](q0 ^ v0 - 1,x);
 else
  m := (q ^ (p ^ k) - 1)/(q ^ (p ^ (k - 1)) - 1);
  f := subs(x = x ^ m, tanabe_FF_poly(q0,v0,p)(k - 1));
 end:

 return first_factor(f,q0);
end:

# tanabe_F(q0,v0)(m) is the field denoted by F[m] in the paper,
# where q = q0 ^ v0 with q0 prime and v0 > 0.
# tanabe_FF(q0,v0)(p,k) is F(k) = F[p^k].

tanabe_F := (q0,v0) -> (m) -> GF(q0,v0 * m);
tanabe_FF := (q0,v0) -> (p,k) -> GF(q0,v0 * p ^ k,tanabe_FF_poly);

# Orders of various groups: G is the general linear group,
# N is the subgroup of monomial matrices, H is the block
# diagonal subgroup of p' index as in prop-non-p-power.

tanabe_G_order := (q) -> proc(d)
 local k;
 return mul(q ^ d - q ^ k,k = 0..d-1);
end:

tanabe_N_order := (q) -> (d) -> d! * (q - 1)^d;

tanabe_H_order := (q,p) -> proc(d)
 local dd,m,i;
 dd := digit_list(d,p);
 m := nops(dd);
 mul(tanabe_G_order(q)(p ^ i) ^ dd[i+1], i = 0..m-1);
end:


# The E^2 page of the AHSS converging to K_*(BV) has a trigrading
# with E^2_{ijk} = H_i(BV_k;K_j).  It has even generators
# b[i] and u, and odd generators e[i] with
#   |b[i]| = tanabe_b_trideg(p,n,r)(i) = [2i,0,1]
#   |e[i]| = tanabe_e_trideg(p,n,r)(i) = [2i+1,0,1]
#   |u|    = tanabe_u_trideg(p,n,r)    = [0,2,0].

tanabe_b_trideg  := (p,n,r) -> (i) -> [2*i,0,1];
tanabe_e_trideg  := (p,n,r) -> (i) -> [2*i+1,0,1];
tanabe_u_trideg  := (p,n,r) -> [0,2,0];

# The only nontrivial differentials have the form d_r, where
# r = tanabe_AHSS_page(p,n,r)(k) for some k >= 0
# [From now on we refer to this as the k'th differential,
#  and the page on which it occurs as the k'th page.]

tanabe_AHSS_page := (p,n,r) -> (k) -> 2*p^(n*(r+k)) - 1;

# Tridegree of the k'th differential
tanabe_AHSS_d_trideg := (p,n,r) -> (k) ->
 [1-2*p^(n*(r+k)),2*p^(n*(r+k))-2,0];

# The k'th page can be described in terms of generators
# bb[m,i] and ee[m,i]

tanabe_bb_defined := (p,n,r) -> (k) -> (m,i) ->
  m >= min(k,tanabe_s(p,n,r)(i));

tanabe_bb_indec := (p,n,r) -> (k) -> (m,i) ->
  m = min(k,tanabe_s(p,n,r)(i));

tanabe_ee_defined := (p,n,r) -> (k) -> (m,i) ->
  m = k and i >= tanabe_N_star(p,n,r)(k);

tanabe_bb_trideg := (p,n,r) -> (m,i) -> [2*p^m*i,0,p^m];
tanabe_ee_trideg := (p,n,r) -> (m,i) -> [2*p^m*i + 1,0,p^m];

tanabe_dbb0 := (p,n,r) -> (k) -> (m,i) ->
  ee[k,i - tanabe_N_bar(p,n,r)(k) + tanabe_N_star(p,n,r)(k)] *
    u ^ (p^(n * (k + r)) - 1);

tanabe_dbb := (p,n,r) -> (k) -> (m,i) ->
  `if`(m < k, 0, `if`(i < tanabe_N_bar(p,n,r)(k), 0, tanabe_dbb0(p,n,r)(k)(m,i)));

# This is the part of the inverse Poincare series contributed by
# irreducible representations of dimension at most p^k.

tanabe_inverse_poincare_series := (p,n,r) -> proc(k)
 local j;
 (1-t)^(p^(n*r)) * mul((1 - t^(p^j))^(p^(n*(r+j))*(1-1/p^n)),j=1..k);
end:

tanabe_poincare_series := (p,n,r) -> (k) ->
 convert(series(1/tanabe_inverse_poincare_series(p,n,r)(k),t=0,p^k+1),
         polynom,t);

tanabe_trideg := (p,n,r) -> proc(x)
 local d,d0,y;
 
 if type(x,indexed) then
  if op(0,x) = b then
   return tanabe_b_trideg(p,n,r)(op(x));
  elif op(0,x) = e then
   return tanabe_e_trideg(p,n,r)(op(x));
  elif op(0,x) = bb then
   return tanabe_bb_trideg(p,n,r)(op(x));
  elif op(0,x) = ee then
   return tanabe_ee_trideg(p,n,r)(op(x));
  else
   return [0,0,0];
  fi;
 elif x = u then
  return tanabe_u_trideg(p,n,r);
 elif type(x,`+`) then
  d := map(tanabe_trideg(p,n,r),{op(x)});
  if nops(d) = 1 then
   return op(d);
  else
   return FAIL;
  fi;
 elif type(x,`*`) then
  d := [0,0,0];
  for y in [op(x)] do
   d0 := tanabe_trideg(p,n,r)(y);
   if d0 = FAIL then return FAIL; fi;
   d := d +~ d0;
  od;
  return d;
 elif type(x,`^`) then
  return tanabe_trideg(p,n,r)(op(1,x)) *~ op(2,x);
 else
  return [0,0,0];
 fi;
end:

######################################################################

# Check v_p(q ^ j - 1) = r + v_p(j) 
check_lem_vp := (p) -> proc(q::posint,j::posint)
 local r;
 r := padic_val(q - 1,p);
 _ASSERT(r > 0, "r > 0");

 _ASSERT(padic_val(q ^ j - 1,p) = r + padic_val(j,p),
         sprintf("v_{%d}(%d ^ %d - 1)",p,q,j));
end;

check_tanabe_numbers := proc()
 local n,r,k,p,L,N,N_bar,N_star,N_lim,P,err;

 assume(n::posint);
 assume(r::posint);
 assume(k::posint);
 assume(p::posint);

 N      := tanabe_N(p,n,r);
 N_bar  := tanabe_N_bar(p,n,r);
 N_star := tanabe_N_star(p,n,r);
 N_lim  := tanabe_N_lim(p,n,r);
 
 _ASSERT(
  simplify(N_bar(k) - N_bar(k-1) - N(k)) = 0,
  "N_bar(k) - N_bar(k-1) = N(k)"
 );

 _ASSERT(
  simplify(N_star(k) - (N_bar(k) - p^(n*k + n*r - k))) = 0,
  "N_star(k) = N_bar(k) - p^(n*k + n*r - k)"
 );

 _ASSERT(
  simplify(p^k * (N_bar(k) - N_star(k)) - p^(n * (k + r))) = 0,
  "p^k * (N_bar(k) - N_star(k)) = p^(n * (k + r))"
 );
 
 _ASSERT(
  simplify(p^(k + 1) * (N_bar(k) - N_star(k + 1)) - p^(n * (k + r))) = 0,
  "p^(k + 1) * (N_bar(k) - N_star(k + 1)) = p^(n * (k + r))"
 );
 
 _ASSERT(
  simplify(N(0) + sum(p^j * N(j),j=1..k) - p^(n*(r+k))) = 0,
  "sum(p^j * N(j),j=0..k) = p^(n*(r+k))"
 );

 _ASSERT(
  simplify((1 - p^(-k)) * N(0) +
           sum(expand((1 - p^(j - k)) * N(j)),j=1..k) - N_star(k)) = 0,
  "sum((1 - p^(j-k)) * N(j),j=0..k) = N_star(k)"
 );

 _ASSERT(
  simplify(p^(k + 1) * N_star(k + 1) - p^k * N_star(k) - (p - 1) * p^k * N_bar(k)) = 0,
  "p^(k + 1) * N_star(k + 1) = p^k * N_star(k) + (p - 1) * p^k * N_bar(k)"
 );

 _ASSERT(
  simplify(factor(N_bar(k) - (N_star(k)*(p^n-1)/(p-1) + p^(n*r)))) = 0,
  "N_bar(k) = N_star(k)*(p^n-1)/(p-1) + p^(n*r)"
 );

 _ASSERT(
  simplify(sum(p^j*(p-1)*N_bar(j),j=0..k-1) - p^k*N_bar(k) + p^(n*(r+k))) = 0,
  "sum(p^j*(p-1)*N_bar(j),j=0..k-1)"
 );
 
 _ASSERT(
  limit(simplify(N_bar(k)/N_lim(k)-1),k=infinity) = 0,
  "N_bar(k) is asymptotic to N_lim(k)"
 );
end:


check_factorial_congruences := proc() 
 local p,i;
 p := ithprime(20);

 _ASSERT(
  {seq(modp((-1)^i * (i - 1)! * (p - i)!,p),i=1..p-1)} = {1},
  "(-1)^i * (i - 1)! * (p - i)! = 1 mod p"
 );

 _ASSERT(
  {seq(mods((-1)^i * binomial(p-1,i-1),p),i=1..p-1)} = {-1},
  "(-1)^i * binomial(p-1,i-1) = -1 mod p"
 );
end:


check_valuations := proc()
 local q0,v0,q,p,r,d,m;
 q0 := 19;
 v0 := 1;
 q  := q0 ^ v0;
 p  := 3;
 r  := padic_val(q - 1, p);
 d  := 20;
 
 _ASSERT(
  padic_val(tanabe_G_order(q)(d),p) - (d * r + (d - digit_sum(d,p))/(p - 1)) = 0,
  "valuation of |G(d)|"
 );

 m := tanabe_G_order(q)(d) / tanabe_N_order(q)(d):
 _ASSERT(type(m,posint) and padic_val(m,p) = 0,
  "N(d) has p' index in G(d)"
 );

 m := tanabe_G_order(q)(d) / tanabe_H_order(q,p)(d):
 _ASSERT(type(m,posint) and padic_val(m,p) = 0,
  "H(d) has p' index in G(d)"
 );

end:

check_diff_trideg := proc()
 local p,n,r,k,m,i,err,d0,d1,d2;

 d0 := tanabe_bb_trideg(p,n,r)(k,i);
 d1 := tanabe_AHSS_d_trideg(p,n,r)(k);
 d2 := tanabe_trideg(p,n,r)(tanabe_dbb0(p,n,r)(k)(m,i));

 err := simplify(d0 + d1 - d2, symbolic);

 _ASSERT(err = [0,0,0], "differential respects tridegrees");
end:
