Module

StandardSubgroupIntersection.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.StandardSubgroupIntersection

3 declarations indexed from sourceView source ↗

Module documentation

Intersecting standard norm conditions

The unramified degree-d factor forces the normalized valuation to be divisible by d. The totally ramified Lubin--Tate factor forces an element to lie in ⟨ϖ⟩ U^n. Their intersection therefore lies in ⟨ϖ^d⟩ U^n. This is the elementary subgroup calculation used in local existence proofs.

Imports6

Imported by4

theorem

unramifiedNormSubgroup_inf_uniformizerPrincipalSubgroup_le

L37 ↗

LocalClassFieldTheory.unramifiedNormSubgroup_inf_uniformizerPrincipalSubgroup_le

Documentation

The intersection of the unramified valuation condition and the principal-unit condition is contained in the corresponding standard subgroup.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
universe u

Lean source · statement

theorem unramifiedNormSubgroup_inf_uniformizerPrincipalSubgroup_le
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (d n : ℕ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    unramifiedNormSubgroup K d ⊓
        LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 n ≤
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ d n

theorem

finiteGaloisCompositum_normSubgroup_le_of_standard

L88 ↗

LocalClassFieldTheory.finiteGaloisCompositum_normSubgroup_le_of_standard

Documentation

If an unramified norm condition and a principal-unit norm condition are realized by finite Galois subextensions, their compositum has norm subgroup contained in every subgroup containing the corresponding standard subgroup.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
universe u

Lean source · statement

theorem finiteGaloisCompositum_normSubgroup_le_of_standard
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : Subgroup Kˣ)
    (ϖ : Kˣ) (d n : ℕ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (hstandard : LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ d n ≤ H)
    (U T : ClassFormation.FiniteGaloisSubextension (intrinsicAbstractBase K))
    (hUle :
      (U.normSubgroup (intrinsicAbsoluteUnits K)).map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom ≤
        (unramifiedNormSubgroup K d).toAddSubgroup)
    (hTle :
      (T.normSubgroup (intrinsicAbsoluteUnits K)).map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom ≤
        (LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 n).toAddSubgroup) :
    (U.compositum T).normSubgroup (intrinsicAbsoluteUnits K) ≤
      H.toAddSubgroup.map
        (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).toAddMonoidHom

theorem

finiteAbelianCompositum_normSubgroup_le_of_standard

L135 ↗

LocalClassFieldTheory.finiteAbelianCompositum_normSubgroup_le_of_standard

Documentation

The same standard-subgroup containment while retaining both inputs and their compositum as finite abelian subextensions.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
universe u

Lean source · statement

theorem finiteAbelianCompositum_normSubgroup_le_of_standard
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : Subgroup Kˣ)
    (ϖ : Kˣ) (d n : ℕ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (hstandard : LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ d n ≤ H)
    (U T : ClassFormation.FiniteAbelianSubextension
      (intrinsicAbstractBase K))
    (hUle :
      (U.normSubgroup (intrinsicAbsoluteUnits K)).map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom ≤
        (unramifiedNormSubgroup K d).toAddSubgroup)
    (hTle :
      (T.normSubgroup (intrinsicAbsoluteUnits K)).map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom ≤
        (LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 n).toAddSubgroup) :
    (U.compositum T).normSubgroup (intrinsicAbsoluteUnits K) ≤
      H.toAddSubgroup.map
        (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).toAddMonoidHom

Module documentation

Intersecting standard norm conditions

Declarations

unramifiedNormSubgroup_inf_uniformizerPrincipalSubgroup_le

finiteGaloisCompositum_normSubgroup_le_of_standard

finiteAbelianCompositum_normSubgroup_le_of_standard