Galois-stable lattices from normal bases of local fields

Let L/K be a finite Galois extension of nonarchimedean local fields with Galois group G = L ≃ₐ[K] L. By the normal basis theorem (IsGalois.normalBasis) there is α ∈ L whose conjugates σ α form a K-basis of L; after multiplying by a nonzero element of 𝒪[K] it may be taken in 𝒪[L]. The 𝒪[K]-span A of the orbit of such an α is then:

• stable under G (Mathlib's Module.End.span_orbit_mem_invtSubmodule);
• free over 𝒪[K] on the conjugates of α, that is, free of rank one over the group ring 𝒪[K][G] with generator α (TauCeti.spanOrbitEquiv);
• open in 𝒪[L]: it contains a power of the maximal ideal 𝓂[L].

In general 𝒪[L] itself is not free over 𝒪[K][G] (this holds only for tamely ramified extensions), so the lattice A is the substitute. Scaling α further by a nonzero element of 𝒪[K] shrinks A without changing these properties, and makes it nearly closed under multiplication: for any nonzero ϖ ∈ 𝒪[K] one can arrange A * A ≤ ϖ • A. For ϖ a uniformizer this is the condition under which the sets 1 + ϖ ^ j • A form a decreasing chain of Galois-stable open subgroups of the units of 𝒪[L], with every successive quotient isomorphic to A / ϖ • A, a free module over the group ring (𝒪[K] ⧸ ϖ)[G]. Such a filtration of the local units is how their Herbrand quotient is computed in the cyclic case.

Main definitions

• TauCeti.spanOrbitEquiv: the isomorphism of representations from the group ring 𝒪[K][G] onto the 𝒪[K]-span of the orbit of an element of 𝒪[L] whose conjugates form a K-basis of L.

Main results

• TauCeti.exists_linearIndependent_algEquiv_apply_integerRing: some element of 𝒪[L] has conjugates forming a K-basis of L.
• TauCeti.linearIndependent_smul_integerRing: the conjugates of such an element are linearly independent over 𝒪[K].
• TauCeti.exists_pow_maximalIdeal_le_span_orbit: the 𝒪[K]-span of the orbit of such an element contains a power of 𝓂[L].
• TauCeti.exists_span_orbit_mul_le_smul: for every nonzero ϖ ∈ 𝒪[K] there is such an element whose orbit spans a lattice A with A * A ≤ ϖ • A.

These elements lie in 𝒪[L] and their conjugates form a K-basis of L; they need not give an 𝒪[K]-basis of 𝒪[L].

References

• J.-P. Serre, Local class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI.
• J. Neukirch, Algebraic Number Theory, Chapter V, §1.

theorem TauCeti.linearIndependent_smul_integerRing {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {α : ↥(ValuativeRel.valuation L).integer} (h : LinearIndependent K fun (σ : Gal(L/K)) => σ ↑α) : LinearIndependent ↥(ValuativeRel.valuation K).integer fun (σ : Gal(L/K)) => σ • α

If the conjugates of an element of 𝒪[L] are linearly independent over K, they are linearly independent over 𝒪[K] as elements of 𝒪[L].

noncomputable def TauCeti.spanOrbitEquiv {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {α : ↥(ValuativeRel.valuation L).integer} (h : LinearIndependent K fun (σ : Gal(L/K)) => σ ↑α) : (Representation.leftRegular ↥(ValuativeRel.valuation K).integer Gal(L/K)).Equiv ((Representation.ofDistribMulAction ↥(ValuativeRel.valuation K).integer Gal(L/K) ↥(ValuativeRel.valuation L).integer).subrepresentation (Submodule.span (↥(ValuativeRel.valuation K).integer) (MulAction.orbit Gal(L/K) α)) ⋯)

The span of the orbit is free of rank one over the group ring. If the conjugates of α ∈ 𝒪[L] are linearly independent over K, then ∑ σ, r_σ σ ↦ ∑ σ, r_σ • σ α is an isomorphism from the group ring 𝒪[K][G], with G acting by left multiplication, onto the 𝒪[K]-span of the orbit of α, with the Galois action restricted from 𝒪[L].

@[simp]

theorem TauCeti.coe_spanOrbitEquiv_single {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {α : ↥(ValuativeRel.valuation L).integer} (h : LinearIndependent K fun (σ : Gal(L/K)) => σ ↑α) (σ : Gal(L/K)) (r : ↥(ValuativeRel.valuation K).integer) : ↑((spanOrbitEquiv h) (MonoidAlgebra.single σ r)) = r • σ • α

spanOrbitEquiv sends r σ ∈ 𝒪[K][G] to r • σ α.

theorem TauCeti.exists_linearIndependent_algEquiv_apply_integerRing (K : Type u_1) (L : Type u_2) [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] : ∃ (α : ↥(ValuativeRel.valuation L).integer), LinearIndependent K fun (σ : Gal(L/K)) => σ ↑α

Some element of 𝒪[L] has conjugates forming a K-basis of L: a normal basis element of L/K scaled into 𝒪[L].

theorem TauCeti.exists_pow_maximalIdeal_le_span_orbit {K : Type u_1} {L : Type u_2} [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] {α : ↥(ValuativeRel.valuation L).integer} (h : LinearIndependent K fun (σ : Gal(L/K)) => σ ↑α) : ∃ (n : ℕ), Submodule.restrictScalars (↥(ValuativeRel.valuation K).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ n) ≤ Submodule.span (↥(ValuativeRel.valuation K).integer) (MulAction.orbit Gal(L/K) α)

The span of the orbit is open: if the conjugates of α ∈ 𝒪[L] form a K-basis of L, the 𝒪[K]-span of the orbit of α contains a power of the maximal ideal of 𝒪[L].

theorem TauCeti.exists_span_orbit_mul_le_smul {K : Type u_1} {L : Type u_2} [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] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : ϖ ≠ 0) : ∃ (α : ↥(ValuativeRel.valuation L).integer), (LinearIndependent K fun (σ : Gal(L/K)) => σ ↑α) ∧ Submodule.span (↥(ValuativeRel.valuation K).integer) (MulAction.orbit Gal(L/K) α) * Submodule.span (↥(ValuativeRel.valuation K).integer) (MulAction.orbit Gal(L/K) α) ≤ ϖ • Submodule.span (↥(ValuativeRel.valuation K).integer) (MulAction.orbit Gal(L/K) α)

A Galois-stable lattice that is almost closed under multiplication. For every nonzero ϖ ∈ 𝒪[K] there is α ∈ 𝒪[L] whose conjugates form a K-basis of L such that the 𝒪[K]-span A of its orbit satisfies A * A ≤ ϖ • A. By spanOrbitEquiv and exists_pow_maximalIdeal_le_span_orbit, this A is free of rank one over 𝒪[K][G] on α and contains a power of 𝓂[L].