The lattice defect of the ring of integers

Let L/K be a finite Galois extension of nonarchimedean local fields with Galois group G = L ≃ₐ[K] L, where K is a finite extension of ℚ_[p], and let k be a field of characteristic p. This file computes the lattice defect (TauCeti.latticeDefect) of the G-module 𝒪[L] in the Grothendieck group G₀(k[G]):

latticeDefect 𝒪[L] = [K : ℚ_p] · [k[G]] (TauCeti.latticeDefect_integerRing_eq_finrank_smul).

The ring 𝒪[L] need not be free over 𝒪[K][G], but it contains a lattice which is. For θ ∈ 𝒪[L] whose conjugates form a K-basis of L, a scaled normal basis element (TauCeti.exists_linearIndependent_algEquiv_apply_integerRing), the 𝒪[K]-span M of the orbit of θ contains a power of 𝓂[L] (TauCeti.exists_pow_maximalIdeal_le_span_orbit), so it has finite index in 𝒪[L], and the two have the same defect (TauCeti.latticeDefect_eq_of_finiteIndex). Through a basis b of 𝒪[K] over ℤ_p, the elements b_j • σ θ form a ℤ_p-basis of M permuted by G, so M is the p-adic permutation lattice ℤ_p[X] on the disjoint union X of [K : ℚ_p] copies of G. Finally ℤ[X] ⊆ ℤ_p[X] has a uniquely p-divisible cokernel, so ℤ_p[X] has the defect of the permutation lattice ℤ[X], which is the permutation class [k[X]] = [K : ℚ_p] · [k[G]] (TauCeti.latticeDefect_finsupp_padicInt, TauCeti.permK0_sigma_fin).

Main results

• TauCeti.latticeDefect_integerRing_eq_finrank_smul: the p-defect of 𝒪[L] is [K : ℚ_p] · [k[G]].

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), §VII.3, proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., Chapter I, Lemma 2.12 and the proof of Theorem 2.8.

theorem TauCeti.latticeDefect_integerRing_eq_finrank_smul (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (k : Type) [CommRing k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [FinitePadicExtension K p] [NeZero ↑p] : latticeDefect k Gal(L/K) p ↥(ValuativeRel.valuation L).integer = Module.finrank ℚ_[p] K • permK0 k Gal(L/K) Gal(L/K)

The lattice defect of the ring of integers: for a finite Galois extension L/K of nonarchimedean local fields, with K/ℚ_p finite, the p-defect of 𝒪[L] in G₀(k[Gal(L/K)]) is [K : ℚ_p] · [k[G]], for k of characteristic p. The instance NeZero (p : L), which holds since L has characteristic zero, is what makes the defect of 𝒪[L] defined.