Module

PrincipalUnitGraded.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.PrincipalUnitGraded

5 declarations indexed from sourceView source ↗

Module documentation

Successive principal-unit quotients of normal-basis lattices

The map sending an integer unit to its difference from one compares successive principal-unit quotients with the corresponding lattice quotients. The file proves injectivity and constructs this comparison at sufficiently deep uniformizer levels.

Imports2

Imported by2

theorem

chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_injective

L40 ↗

LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_injective

Documentation

The map u ↦ u - 1 on successive normal-basis principal-unit quotients is injective. Its kernel calculation is exactly the statement that u - 1 ∈ π_K^(n+1)M if and only if u ∈ V^(n+1).

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalClassFieldTheory
open CyclicCohomology LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_injective
    {n : Nat} {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) =
      chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hV : Vsucc ≤ Vn)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L)) :
    Function.Injective
      (chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom
        K L n hVn hVsucc hV hmul_error)

theorem

chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_surjective_of_le_maximalIdeal

L97 ↗

LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_surjective_of_le_maximalIdeal

Documentation

If the high normal-basis lattice lies in the maximal ideal, every additive successive-quotient class is represented by a unit 1 + x; hence the map u ↦ u - 1 is surjective.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalClassFieldTheory
open CyclicCohomology LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_surjective_of_le_maximalIdeal
    {n : Nat} {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) =
      chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hV : Vsucc ≤ Vn)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L))
    (hle : chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L) :
    Function.Surjective
      (chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom
        K L n hVn hVsucc hV hmul_error)

def

chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot

L165 ↗

LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot

Documentation

The actual isomorphism V^n/V^(n+1) ≃ π_K^nM/π_K^(n+1)M once the high-lattice bound and multiplicative-error estimate hold.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalClassFieldTheory
open CyclicCohomology LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot
    {n : Nat} {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) =
      chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hV : Vsucc ≤ Vn)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L))
    (hle : chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L) :
    chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV ≃*
      Multiplicative (chosenNormalBasisLatticeSuccQuot K L n)

theorem

chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot_mk

L193 ↗

LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot_mk

Documentation

States the theorem chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot_mk.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalClassFieldTheory
open CyclicCohomology LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot_mk
    {n : Nat} {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) =
      chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hV : Vsucc ≤ Vn)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L))
    (hle : chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    (u : Vn) :
    chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot
        K L hVn hVsucc hV hmul_error hle
        (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u) =
      Multiplicative.ofAdd
        (chosenNormalBasisPrincipalUnitLatticeClass K L n (u : 𝒪[L]ˣ)
          (by exact hVn ▸ u.2)) :=
  rfl

theorem

exists_chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot

L221 ↗

LocalClassFieldTheory.exists_chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot

Documentation

Existential high-degree boundary used in the proof of the local class-field-axiom theorem: for every sufficiently large n, the actual successive principal-unit quotient is isomorphic to the corresponding normal-basis lattice quotient.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalClassFieldTheory
open CyclicCohomology LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem exists_chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot
    [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∃ Vn Vsucc : Subgroup 𝒪[L]ˣ,
        ∃ hV : Vsucc ≤ Vn,
          ∃ hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n,
            (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1) ∧
              ∃ Φ : chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV ≃*
                  Multiplicative (chosenNormalBasisLatticeSuccQuot K L n),
                Vn ≤ principalUnits L 1 ∧
                  ∀ u : Vn,
                    Φ (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u) =
                      Multiplicative.ofAdd
                        (chosenNormalBasisPrincipalUnitLatticeClass K L n
                          (u : 𝒪[L]ˣ) (by exact hVn ▸ u.2)) := by
  rcases exists_chosenNormalBasisPrincipalUnitSubgroupSuccPair
      (K := K) (L := L) with ⟨c₁, hc₁⟩
  rcases exists_chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ
      (K := K) (L := L) with ⟨c₂, hc₂⟩
  rcases
    exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdeal_and_mul_closed
      (K := K) (L := L) with ⟨c₃, hc₃⟩
  refine ⟨max c₁ (max c₂ c₃), ?_⟩
  intro n hn
  have hc₁n : c₁ ≤ n :=
    le_trans (le_max_left c₁ (max c₂ c₃)) hn
  have hcrest : max c₂ c₃ ≤ max c₁ (max c₂ c₃) :=
    le_max_right c₁ (max c₂ c₃)
  have hc₂n : c₂ ≤ n :=
    le_trans (le_trans (le_max_left c₂ c₃) hcrest) hn
  have hc₃n : c₃ ≤ n :=
    le_trans (le_trans (le_max_right c₂ c₃) hcrest) hn
  rcases hc₁ n hc₁n with ⟨Vn, Vsucc, hVn, hVsucc, hV, hVnle⟩
  let hmul_error := hc₂ n hc₂n
  let hle := (hc₃ n hc₃n).1
  let Φ : chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV ≃*
      Multiplicative (chosenNormalBasisLatticeSuccQuot K L n) :=
    chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot
      K L hVn hVsucc hV hmul_error hle
  refine ⟨Vn, Vsucc, hV, hVn, hVsucc, Φ, hVnle, ?_⟩
  intro u
  rfl

Module documentation

Successive principal-unit quotients of normal-basis lattices

Declarations

chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_injective

chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_surjective_of_le_maximalIdeal

chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot

chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot_mk

exists_chosenNormalBasisPrincipalUnitSuccQuotMulEquivLatticeSuccQuot