NYLL
Module

NormalBasisGaloisAction.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.NormalBasisGaloisAction
19 declarations indexed from sourceView source ↗

Module documentation

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

Imports4
Imported by3

Declarations

def

subgroupMulDistribMulActionOfStable

L33 ↗
LocalClassFieldTheory.subgroupMulDistribMulActionOfStable
Documentation

Restrict a multiplicative group action to an invariant subgroup. This is the honest action used below on the standard subgroups V^n.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
Lean source · full declaration
def subgroupMulDistribMulActionOfStable
    (G : Type uG) (A : Type uA) [Group G] [CommGroup A]
    [MulDistribMulAction G A] (V : Subgroup A)
    (hstable : ∀ (g : G) (a : A), a ∈ V → g • a ∈ V) :
    MulDistribMulAction G V where
  smul g a := ⟨g • (a : A), hstable g a a.2⟩
  one_smul := by
    intro a
    apply Subtype.ext
    exact one_smul G (a : A)
  mul_smul := by
    intro g h a
    apply Subtype.ext
    exact mul_smul g h (a : A)
  smul_mul := by
    intro g a b
    apply Subtype.ext
    exact MulDistribMulAction.smul_mul g (a : A) (b : A)
  smul_one := by
    intro g
    apply Subtype.ext
    exact MulDistribMulAction.smul_one g
theorem

quotientActionOfSubgroupStable

L58 ↗
LocalClassFieldTheory.quotientActionOfSubgroupStable
Documentation

An invariant subgroup satisfies the relation-preservation condition needed for the action on its quotient.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
Lean source · full declaration
theorem quotientActionOfSubgroupStable
    (G : Type uG) (A : Type uA) [Group G] [CommGroup A]
    [MulDistribMulAction G A] (V : Subgroup A)
    (hstable : ∀ (g : G) (a : A), a ∈ V → g • a ∈ V) :
    MulAction.QuotientAction G V where
  inv_mul_mem g a b hab := by
    have hsmul : g • (a⁻¹ * b) ∈ V := hstable g (a⁻¹ * b) hab
    simpa [MulDistribMulAction.smul_mul, map_inv] using hsmul
def

quotientMulDistribMulActionOfSubgroupStable

L70 ↗
LocalClassFieldTheory.quotientMulDistribMulActionOfSubgroupStable
Documentation

Descend an action by group automorphisms to the quotient by an invariant subgroup.

Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
Lean source · statement
def quotientMulDistribMulActionOfSubgroupStable
    (G : Type uG) (A : Type uA) [Group G] [CommGroup A]
    [MulDistribMulAction G A] (V : Subgroup A)
    (hstable : ∀ (g : G) (a : A), a ∈ V → g • a ∈ V) :
    MulDistribMulAction G (A ⧸ V)
theorem

galoisGroup_apply_mem_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice

L98 ↗
LocalClassFieldTheory.galoisGroup_apply_mem_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice
Documentation

Every dilate π_K^n M of the normal-basis lattice is stable under the actual action of Gal(L / K).

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
Lean source · statement
theorem galoisGroup_apply_mem_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice
    (n : Nat) (sigma : Gal(L/K)) {x : L}
    (hx : x ∈ chosenBaseUniformizerPowSubmodule K L n
      (chosenNormalBasisIntegerLattice K L)) :
    sigma x ∈ chosenBaseUniformizerPowSubmodule K L n
      (chosenNormalBasisIntegerLattice K L)
theorem

galoisGroup_smul_mem_chosenNormalBasisPrincipalUnitSet

L126 ↗
LocalClassFieldTheory.galoisGroup_smul_mem_chosenNormalBasisPrincipalUnitSet
Documentation

The actual integer-unit Galois action preserves each normal-basis principal-unit set V^n = 1 + π_K^n M.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · full declaration
theorem galoisGroup_smul_mem_chosenNormalBasisPrincipalUnitSet
    (n : Nat) (sigma : Gal(L/K)) {a : 𝒪[L]ˣ}
    (ha : a ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    sigma • a ∈ chosenNormalBasisPrincipalUnitSet K L n := by
  let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
  rw [mem_chosenNormalBasisPrincipalUnitSet_iff] at ha ⊢
  have hstable :=
    galoisGroup_apply_mem_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice
      (K := K) (L := L) n sigma ha
  simpa [galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul,
    map_sub, map_one] using hstable
def

chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction

L142 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction
Documentation

The restricted actual Galois action on any subgroup whose carrier is the standard V^n.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
def chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n) :
    MulDistribMulAction (Gal(L / K)) V
theorem

chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction_smul

L157 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction_smul
Documentation

The induced Galois action on the principal-unit subgroup agrees with the ambient action.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · full declaration
theorem chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction_smul
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (sigma : Gal(L/K)) (a : V) :
    letI := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction K L n V hV
    ((sigma • a : V) : 𝒪[L]ˣ) =
      letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
      sigma • (a : 𝒪[L]ˣ) :=
  rfl
theorem

chosenNormalBasisPrincipalUnitSubgroup_tateNorm_coe

L169 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroup_tateNorm_coe
Documentation

Coercing the subgroup Tate norm gives the ambient product over the Galois group.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · full declaration
theorem chosenNormalBasisPrincipalUnitSubgroup_tateNorm_coe
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (a : V) :
    letI := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction K L n V hV
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    ((tateNorm (Gal(L / K)) V a : V) : 𝒪[L]ˣ) =
      tateNorm (Gal(L / K)) 𝒪[L]ˣ (a : 𝒪[L]ˣ) := by
  let := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction K L n V hV
  let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
  unfold tateNorm
  change V.subtype (∏ g : Gal(L / K), g • a) =
    ∏ g : Gal(L / K), g • (a : 𝒪[L]ˣ)
  rw [map_prod]
  apply Finset.prod_congr rfl
  intro g _hg
  rfl
theorem

chosenNormalBasisPrincipalUnitSubgroup_sigmaMinusOne_coe

L189 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroup_sigmaMinusOne_coe
Documentation

Coercion commutes with the σ - 1 operation on the principal-unit subgroup.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · full declaration
theorem chosenNormalBasisPrincipalUnitSubgroup_sigmaMinusOne_coe
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (sigma : Gal(L/K)) (a : V) :
    letI := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction K L n V hV
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    ((sigmaMinusOne (Gal(L / K)) V sigma a : V) : 𝒪[L]ˣ) =
      sigmaMinusOne (Gal(L / K)) 𝒪[L]ˣ sigma (a : 𝒪[L]ˣ) := by
  let := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction K L n V hV
  let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
  rfl
def

chosenNormalBasisIntegerUnitsQuotMulDistribMulAction

L204 ↗
LocalClassFieldTheory.chosenNormalBasisIntegerUnitsQuotMulDistribMulAction
Documentation

The quotient action on 𝒪_Lˣ / V^n, descended from the actual integer-unit Galois action.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
def chosenNormalBasisIntegerUnitsQuotMulDistribMulAction
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n) :
    MulDistribMulAction (Gal(L / K)) (𝒪[L]ˣ ⧸ V)
def

chosenNormalBasisPrincipalUnitSubgroupInclusion

L220 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupInclusion
Documentation

Inclusion of a chosen normal-basis principal-unit subgroup into all integer units.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
def chosenNormalBasisPrincipalUnitSubgroupInclusion
    (V : Subgroup 𝒪[L]ˣ) : V →* 𝒪[L]ˣ
theorem

chosenNormalBasisPrincipalUnitSubgroupInclusion_apply

L226 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupInclusion_apply
Documentation

The principal-unit subgroup inclusion returns the underlying integer unit.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
theorem chosenNormalBasisPrincipalUnitSubgroupInclusion_apply
    (V : Subgroup 𝒪[L]ˣ) (a : V) :
    chosenNormalBasisPrincipalUnitSubgroupInclusion (L := L) V a = a
def

chosenNormalBasisIntegerUnitsQuotientMap

L232 ↗
LocalClassFieldTheory.chosenNormalBasisIntegerUnitsQuotientMap
Documentation

Projection of integer units to the quotient by V^n.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
def chosenNormalBasisIntegerUnitsQuotientMap
    (V : Subgroup 𝒪[L]ˣ) : 𝒪[L]ˣ →* (𝒪[L]ˣ ⧸ V)
theorem

chosenNormalBasisIntegerUnitsQuotientMap_apply

L238 ↗
LocalClassFieldTheory.chosenNormalBasisIntegerUnitsQuotientMap_apply
Documentation

The integer-unit quotient map sends a unit to its quotient class.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
theorem chosenNormalBasisIntegerUnitsQuotientMap_apply
    (V : Subgroup 𝒪[L]ˣ) (a : 𝒪[L]ˣ) :
    chosenNormalBasisIntegerUnitsQuotientMap (L := L) V a =
      QuotientGroup.mk a
theorem

chosenNormalBasisPrincipalUnitSubgroupInclusion_equivariant

L245 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupInclusion_equivariant
Documentation

Inclusion of the principal-unit subgroup is Galois equivariant.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · full declaration
theorem chosenNormalBasisPrincipalUnitSubgroupInclusion_equivariant
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (sigma : Gal(L/K)) (a : V) :
    letI := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction K L n V hV
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    chosenNormalBasisPrincipalUnitSubgroupInclusion (L := L) V (sigma • a) =
      sigma • chosenNormalBasisPrincipalUnitSubgroupInclusion (L := L) V a :=
  rfl
theorem

chosenNormalBasisIntegerUnitsQuotientMap_equivariant

L256 ↗
LocalClassFieldTheory.chosenNormalBasisIntegerUnitsQuotientMap_equivariant
Documentation

The quotient map on integer units is Galois equivariant.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · full declaration
theorem chosenNormalBasisIntegerUnitsQuotientMap_equivariant
    (n : Nat) (V : Subgroup 𝒪[L]ˣ)
    (hV : (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (sigma : Gal(L/K)) (a : 𝒪[L]ˣ) :
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    letI := chosenNormalBasisIntegerUnitsQuotMulDistribMulAction K L n V hV
    chosenNormalBasisIntegerUnitsQuotientMap (L := L) V (sigma • a) =
      sigma • chosenNormalBasisIntegerUnitsQuotientMap (L := L) V a := by
  rfl
theorem

chosenNormalBasisPrincipalUnitSubgroupInclusion_injective

L267 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupInclusion_injective
Documentation

Inclusion of the principal-unit subgroup is injective.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
theorem chosenNormalBasisPrincipalUnitSubgroupInclusion_injective
    (V : Subgroup 𝒪[L]ˣ) :
    Function.Injective (chosenNormalBasisPrincipalUnitSubgroupInclusion (L := L) V)
theorem

chosenNormalBasisIntegerUnitsQuotientMap_surjective

L273 ↗
LocalClassFieldTheory.chosenNormalBasisIntegerUnitsQuotientMap_surjective
Documentation

Every integer-unit quotient class has a representative.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
theorem chosenNormalBasisIntegerUnitsQuotientMap_surjective
    (V : Subgroup 𝒪[L]ˣ) :
    Function.Surjective (chosenNormalBasisIntegerUnitsQuotientMap (L := L) V)
theorem

chosenNormalBasisPrincipalUnitSubgroupInclusion_range_eq_ker_quotient

L280 ↗
LocalClassFieldTheory.chosenNormalBasisPrincipalUnitSubgroupInclusion_range_eq_ker_quotient
Documentation

Exactness at the integer-unit term of 1 → V^n → 𝒪_Lˣ → 𝒪_Lˣ/V^n → 1.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe uG uA u
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [IsIntegralClosure 𝒪[L] 𝒪[K] L]
Lean source · statement
theorem chosenNormalBasisPrincipalUnitSubgroupInclusion_range_eq_ker_quotient
    (V : Subgroup 𝒪[L]ˣ) :
    MonoidHom.range (chosenNormalBasisPrincipalUnitSubgroupInclusion (L := L) V) =
      MonoidHom.ker (chosenNormalBasisIntegerUnitsQuotientMap (L := L) V)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.