Module

NormalBasisFiniteQuotient.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.NormalBasisFiniteQuotient

5 declarations indexed from sourceView source ↗

Module documentation

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.NormalBasisFiniteQuotient Lean module.

Imports2

Imported by2

theorem

exists_principalUnits_le_chosenNormalBasisPrincipalUnitSet

L35 ↗

LocalClassFieldTheory.exists_principalUnits_le_chosenNormalBasisPrincipalUnitSet

Documentation

Since the normal-basis lattices π_K^n M are open for high n, each corresponding V^n contains an ordinary principal-unit subgroup.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe u
open scoped ValuativeRel
open Filter 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] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Module.Finite 𝒪[K] 𝒪[L]]

Lean source · statement

theorem exists_principalUnits_le_chosenNormalBasisPrincipalUnitSet :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∃ m : Nat, (principalUnits L m : Set 𝒪[L]ˣ) ⊆
        chosenNormalBasisPrincipalUnitSet K L n

def

integerUnitsModPrincipalUnitsToSubgroupQuotient

L60 ↗

LocalClassFieldTheory.integerUnitsModPrincipalUnitsToSubgroupQuotient

Documentation

The canonical map from 𝒪_Lˣ/U_L^m onto 𝒪_Lˣ/V whenever U_L^m ≤ V.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe u
open scoped ValuativeRel
open Filter 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] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Module.Finite 𝒪[K] 𝒪[L]]

Lean source · statement

def integerUnitsModPrincipalUnitsToSubgroupQuotient
    (m : Nat) (V : Subgroup 𝒪[L]ˣ) (h : principalUnits L m ≤ V) :
    IntegerUnitsModPrincipalUnitsAtLevel L m →* (𝒪[L]ˣ ⧸ V)

theorem

integerUnitsModPrincipalUnitsToSubgroupQuotient_surjective

L72 ↗

LocalClassFieldTheory.integerUnitsModPrincipalUnitsToSubgroupQuotient_surjective

Documentation

States the theorem integerUnitsModPrincipalUnitsToSubgroupQuotient_surjective.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe u
open scoped ValuativeRel
open Filter 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] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Module.Finite 𝒪[K] 𝒪[L]]
omit [TopologicalSpace L] [IsNonarchimedeanLocalField L] in

Lean source · statement

theorem integerUnitsModPrincipalUnitsToSubgroupQuotient_surjective
    (m : Nat) (V : Subgroup 𝒪[L]ˣ) (h : principalUnits L m ≤ V) :
    Function.Surjective
      (integerUnitsModPrincipalUnitsToSubgroupQuotient L m V h)

theorem

finite_chosenNormalBasisIntegerUnitsQuotient_of_principalUnits_le

L84 ↗

LocalClassFieldTheory.finite_chosenNormalBasisIntegerUnitsQuotient_of_principalUnits_le

Documentation

A quotient by a subgroup containing an ordinary principal-unit level is finite.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe u
open scoped ValuativeRel
open Filter 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] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Module.Finite 𝒪[K] 𝒪[L]]

Lean source · statement

theorem finite_chosenNormalBasisIntegerUnitsQuotient_of_principalUnits_le
    (m : Nat) (V : Subgroup 𝒪[L]ˣ) (h : principalUnits L m ≤ V) :
    Finite (𝒪[L]ˣ ⧸ V)

theorem

exists_finite_chosenNormalBasisIntegerUnitsQuotient

L95 ↗

LocalClassFieldTheory.exists_finite_chosenNormalBasisIntegerUnitsQuotient

Documentation

Finite-index boundary for the local class-field axiom: for sufficiently large n, every actual subgroup with carrier V^n has finite quotient in 𝒪_Lˣ.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe u
open scoped ValuativeRel
open Filter 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] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Module.Finite 𝒪[K] 𝒪[L]]

Lean source · statement

theorem exists_finite_chosenNormalBasisIntegerUnitsQuotient :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ (V : Subgroup 𝒪[L]ˣ),
        (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n →
          Finite (𝒪[L]ˣ ⧸ V)

Module documentation

Declarations

exists_principalUnits_le_chosenNormalBasisPrincipalUnitSet

integerUnitsModPrincipalUnitsToSubgroupQuotient

integerUnitsModPrincipalUnitsToSubgroupQuotient_surjective

finite_chosenNormalBasisIntegerUnitsQuotient_of_principalUnits_le

exists_finite_chosenNormalBasisIntegerUnitsQuotient