The lattice defect of a p-adic permutation lattice

Let G be a group acting on a finite set X, and k a commutative ring of characteristic p. The p-adic permutation lattice ℤ_p[X] = X →₀ ℤ_[p], on which G acts by pushing the support forward, has the lattice defect of the integral permutation lattice ℤ[X], that is the permutation class [k[X]] (TauCeti.latticeDefect_finsupp_padicInt).

The inclusion ℤ[X] ⊆ ℤ_p[X] is not of finite index, but its cokernel (ℤ_p / ℤ)[X] is uniquely p-divisible: every p-adic integer is congruent to an integer modulo p, and a p-adic integer whose p-fold is an integer is itself an integer (TauCeti.PadicInt.exists_finsupp_eq_mapRange_intCast_add, TauCeti.PadicInt.mem_range_finsupp_mapRange_intCast_of_smul_mem). So the defect does not change (TauCeti.latticeDefect_eq_of_bijective_zsmul_quotient), and the defect of ℤ[X] is computed by TauCeti.latticeDefect_finsupp_int.

Finite free ℤ_p[G]-modules arise as Galois-stable lattices in p-adic fields, through normal bases; this is how their defects are computed.

Main results

• TauCeti.latticeDefect_finsupp_padicInt: the defect of ℤ_p[X] is [k[X]].

References

• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., Chapter I, Lemma 2.12.

instance TauCeti.finite_quotSMulTop_finsupp_padicInt (p : ℕ) [Fact (Nat.Prime p)] {X : Type} [Finite X] : Finite (QuotSMulTop (↑p) (X →₀ ℤ_[p]))

The reduction ℤ_p[X] ⧸ p of the p-adic permutation lattice is finite: it is the image of ℤ[X] ⧸ p.

theorem TauCeti.latticeDefect_finsupp_padicInt (p : ℕ) [Fact (Nat.Prime p)] {X : Type} [Finite X] (k G : Type) [CommRing k] [CharP k p] [Group G] [MulAction G X] : latticeDefect k G p (X →₀ ℤ_[p]) = permK0 k G X

The lattice defect of a p-adic permutation lattice ℤ_p[X] = X →₀ ℤ_[p], on which G acts by pushing the support forward, is the permutation class [k[X]] in characteristic p: the inclusion ℤ[X] ⊆ ℤ_p[X] has a uniquely p-divisible cokernel, so ℤ_p[X] has the defect of ℤ[X].