Documentation

TauCeti.NumberTheory.LocalField.UnitFiltration.Lattice

The unit filtration of a lattice #

Let L/K be an extension of nonarchimedean local fields, let Ο– β‰  0 be an element of the maximal ideal of π’ͺ[K], and let A βŠ† π’ͺ[L] be an π’ͺ[K]-submodule which is open, that is, contains a power of 𝓂[L], and which satisfies A * A ≀ Ο– β€’ A. Then for every j : β„• the set

1 + Ο– ^ j β€’ A = {1 + Ο– ^ j β€’ a | a ∈ A}

is an open subgroup of LΛ£, contained in U(L, j + 1). These subgroups form a decreasing, separated and complete filtration, and 1 + Ο– ^ j β€’ a ↦ a mod Ο– β€’ A is a surjective homomorphism onto the additive group of A β§Έ Ο– β€’ A whose kernel is 1 + Ο– ^ (j + 1) β€’ A: every graded piece of the filtration is A β§Έ Ο– β€’ A. If A is stable under the automorphisms of L/K, so is each step.

For a finite Galois extension with group G a lattice of this kind is supplied by a scaled normal basis element (TauCeti.exists_span_orbit_mul_le_smul), and is then free over π’ͺ[K][G], so that every graded piece is free over (π’ͺ[K] β§Έ Ο–)[G]. This filtration therefore replaces the unit filtration U(L, i) of L, whose graded pieces are the residue field and are in general not free over the group ring, when one computes the Tate cohomology of the units of L by successive approximation: this is how the Herbrand quotient of π’ͺ[L]Λ£ is shown to be 1 for cyclic G.

Main definitions #

Main results #

References #

source
structure TauCeti.IsUnitFiltrationLattice {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] (Ο– : β†₯(ValuativeRel.valuation K).integer) (A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) :
Prop

A is a lattice defining a unit filtration with respect to Ο–: Ο– is a nonzero element of the maximal ideal of π’ͺ[K], and A is an π’ͺ[K]-submodule of π’ͺ[L] that contains a power of 𝓂[L] and satisfies A * A ≀ Ο– β€’ A. The sets 1 + Ο– ^ j β€’ A are then subgroups of LΛ£ (TauCeti.IsUnitFiltrationLattice.filtration).

Instances For
    source
    theorem TauCeti.IsUnitFiltrationLattice.mem_maximalIdeal_of_mem {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) {a : β†₯(ValuativeRel.valuation L).integer} (ha : a ∈ A) :
    a ∈ IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation L).integer

    Every element of A lies in the maximal ideal of π’ͺ[L]: its square lies in Ο– β€’ A.

    source
    def TauCeti.IsUnitFiltrationLattice.filtration {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
    Subgroup LΛ£

    The unit filtration of a lattice. For a lattice A defining a unit filtration with respect to Ο–, the subgroup 1 + Ο– ^ j β€’ A of LΛ£: the units of the form 1 + Ο– ^ j β€’ a with a ∈ A.

    Instances For
      source
      theorem TauCeti.IsUnitFiltrationLattice.mem_filtration_iff {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) {j : β„•} {x : LΛ£} :
      x ∈ hA.filtration j ↔ βˆƒ a ∈ A, ↑x = ↑(1 + Ο– ^ j β€’ a)

      Membership in the unit filtration of a lattice: x = 1 + Ο– ^ j β€’ a with a ∈ A.

      source
      theorem TauCeti.IsUnitFiltrationLattice.filtration_le_unitFiltration_succ {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
      hA.filtration j ≀ unitFiltration L (j + 1)

      The step 1 + Ο– ^ j β€’ A lies in U(L, j + 1).

      source
      theorem TauCeti.IsUnitFiltrationLattice.exists_unitFiltration_le_filtration {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
      βˆƒ (m : β„•), unitFiltration L m ≀ hA.filtration j

      The step 1 + Ο– ^ j β€’ A contains some U(L, m).

      source
      theorem TauCeti.IsUnitFiltrationLattice.isOpen_filtration {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
      IsOpen ↑(hA.filtration j)

      Each step 1 + Ο– ^ j β€’ A is an open subgroup of LΛ£.

      source
      theorem TauCeti.IsUnitFiltrationLattice.filtration_antitone {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) :
      Antitone hA.filtration

      The unit filtration of a lattice is decreasing.

      source
      theorem TauCeti.IsUnitFiltrationLattice.iInf_filtration {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) :
      β¨… (j : β„•), hA.filtration j = βŠ₯

      The unit filtration of a lattice separates points: an element lying in every step is 1.

      source
      theorem TauCeti.IsUnitFiltrationLattice.exists_forall_div_prod_mem_filtration {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (y : β„• β†’ LΛ£) (hy : βˆ€ (n : β„•), y n ∈ hA.filtration n) :
      βˆƒ s ∈ hA.filtration 0, βˆ€ (n : β„•), s / ∏ i ∈ Finset.range n, y i ∈ hA.filtration n

      The unit filtration of a lattice is complete. If y n lies in the n-th step 1 + Ο– ^ n β€’ A for every n, the infinite product ∏ n, y n converges to some s in step zero, in the sense that s differs from the n-th partial product by an element of the n-th step.

      The graded pieces #

      source
      noncomputable def TauCeti.IsUnitFiltrationLattice.filtrationToQuotient {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
      β†₯(hA.filtration j) β†’* Multiplicative (β†₯A β§Έ Ο– β€’ ⊀)

      The graded pieces of the unit filtration of a lattice. The homomorphism 1 + Ο– ^ j β€’ a ↦ a mod Ο– β€’ A from the j-th step onto the additive group of A β§Έ Ο– β€’ A. Its kernel is the next step (TauCeti.IsUnitFiltrationLattice.ker_filtrationToQuotient), and it is surjective (TauCeti.IsUnitFiltrationLattice.filtrationToQuotient_surjective).

      Instances For
        source
        theorem TauCeti.IsUnitFiltrationLattice.filtrationToQuotient_apply {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) {j : β„•} (x : β†₯(hA.filtration j)) {a : β†₯(ValuativeRel.valuation L).integer} (ha : a ∈ A) (hx : ↑↑x = ↑(1 + Ο– ^ j β€’ a)) :
        (hA.filtrationToQuotient j) x = Multiplicative.ofAdd (Submodule.Quotient.mk ⟨a, ha⟩)

        The value of filtrationToQuotient at 1 + Ο– ^ j β€’ a is a mod Ο– β€’ A.

        source
        theorem TauCeti.IsUnitFiltrationLattice.ker_filtrationToQuotient {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
        (hA.filtrationToQuotient j).ker = (hA.filtration (j + 1)).subgroupOf (hA.filtration j)

        The kernel of filtrationToQuotient on the j-th step is the (j + 1)-st step: the graded piece of the unit filtration of A at j embeds into A β§Έ Ο– β€’ A.

        source
        theorem TauCeti.IsUnitFiltrationLattice.filtrationToQuotient_surjective {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) (j : β„•) :
        Function.Surjective ⇑(hA.filtrationToQuotient j)

        filtrationToQuotient is surjective: every class in A β§Έ Ο– β€’ A is the class of the coordinate of some 1 + Ο– ^ j β€’ a.

        Galois stability #

        source
        theorem TauCeti.IsUnitFiltrationLattice.unitsMap_mem_filtration {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] {Ο– : β†₯(ValuativeRel.valuation K).integer} {A : Submodule β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer} (hA : IsUnitFiltrationLattice Ο– A) [Module.Finite K L] (Οƒ : Gal(L/K)) (hΟƒ : βˆ€ a ∈ A, Οƒ β€’ a ∈ A) {j : β„•} {x : LΛ£} (hx : x ∈ hA.filtration j) :
        (Units.map ↑σ) x ∈ hA.filtration j

        If the lattice A is stable under an automorphism Οƒ of L/K, so is every step 1 + Ο– ^ j β€’ A of its unit filtration.

        source
        theorem TauCeti.exists_isUnitFiltrationLattice_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 K).integer} (hΟ– : Ο– β‰  0) (hΟ–m : Ο– ∈ IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer) :
        βˆƒ (Ξ± : β†₯(ValuativeRel.valuation L).integer), (LinearIndependent K fun (Οƒ : Gal(L/K)) => Οƒ ↑α) ∧ IsUnitFiltrationLattice Ο– (Submodule.span (β†₯(ValuativeRel.valuation K).integer) (MulAction.orbit Gal(L/K) Ξ±))

        Lattices defining a unit filtration exist. For a finite Galois extension L/K of nonarchimedean local fields and a nonzero Ο– ∈ 𝓂[K], some Ξ± ∈ π’ͺ[L] has conjugates forming a K-basis of L and is such that the π’ͺ[K]-span of its orbit defines a unit filtration with respect to Ο–. That span is stable under the Galois group and free over π’ͺ[K][G] on Ξ± (TauCeti.spanOrbitEquiv).