Module

NormSubgroupSurjectivity.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.NormSubgroupSurjectivity

6 declarations indexed from sourceView source ↗

Module documentation

Surjectivity criteria for the local norm-subgroup map

This file translates the abstract existence theorem into ordinary field norms. It proves the compositum and intersection formulas, isolates the norm-topology criterion which makes the ordinary norm-subgroup order embedding surjective, and constructs norm-topology witnesses from concrete finite Galois extensions.

Imports4

Imported by3

theorem

finiteAbelianNormSubgroup_compositum

L39 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroup_compositum

Documentation

The ordinary norm subgroup of a compositum is the intersection of the two ordinary norm subgroups.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroup_compositum
    (L₁ L₂ : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    finiteAbelianNormSubgroup K (L₁.compositum L₂) =
      finiteAbelianNormSubgroup K L₁ ⊓
        finiteAbelianNormSubgroup K L₂

theorem

finiteAbelianNormSubgroup_intersection

L80 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroup_intersection

Documentation

The ordinary norm subgroup of an intersection field is the supremum of the two ordinary norm subgroups.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroup_intersection
    (L₁ L₂ : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    finiteAbelianNormSubgroup K (L₁.intersection L₂) =
      finiteAbelianNormSubgroup K L₁ ⊔
        finiteAbelianNormSubgroup K L₂

theorem

exists_finiteAbelianNormSubgroup_eq_of_normOpen

L119 ↗

LocalClassFieldTheory.exists_finiteAbelianNormSubgroup_eq_of_normOpen

Documentation

A native open finite-index subgroup which is open for the abstract norm topology is the ordinary norm subgroup of a finite abelian subextension.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_finiteAbelianNormSubgroup_eq_of_normOpen
    (H : OpenFiniteIndexSubgroup K)
    (hnormOpen :
      IsNormOpen (intrinsicAbsoluteUnits K) (intrinsicAbstractBase K)
        ((H.subgroup.toAddSubgroup.map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).toAddMonoidHom :
          AddSubgroup (ambientFixedAddSubgroup (intrinsicAbsoluteUnits K)
            (intrinsicAbstractBase K))) : Set _)) :
    ∃ L, finiteAbelianNormSubgroupMap K L = H

theorem

finiteAbelianNormSubgroupMap_surjective_of_normOpen

L180 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupMap_surjective_of_normOpen

Documentation

If all native finite-index subgroups are norm-open, the ordinary norm-subgroup order embedding is surjective.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroupMap_surjective_of_normOpen
    (hnormOpen : ∀ (H : Subgroup Kˣ) [H.FiniteIndex],
      IsNormOpen (intrinsicAbsoluteUnits K) (intrinsicAbstractBase K)
        ((H.toAddSubgroup.map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).toAddMonoidHom :
          AddSubgroup (ambientFixedAddSubgroup (intrinsicAbsoluteUnits K)
            (intrinsicAbstractBase K))) : Set _)) :
    Function.Surjective (finiteAbelianNormSubgroupMap K)

theorem

finiteIndexSubgroup_isNormOpen_of_normSubgroup_le

L197 ↗

LocalClassFieldTheory.finiteIndexSubgroup_isNormOpen_of_normSubgroup_le

Documentation

A finite Galois extension whose ordinary norm subgroup is contained in H witnesses that H is open for the abstract norm topology.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · full declaration

theorem finiteIndexSubgroup_isNormOpen_of_normSubgroup_le
    (E : Type) [Field E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    (H : Subgroup Kˣ) [H.FiniteIndex]
    (hnorm : localNormSubgroup K E ≤ H) :
    let A := intrinsicAbsoluteUnits K
    let B := intrinsicAbstractBase K
    let e := baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)
    IsNormOpen A B
      ((H.toAddSubgroup.map e.toAddMonoidHom :
        AddSubgroup (ambientFixedAddSubgroup A B)) :
        Set (ambientFixedAddSubgroup A B)) := by
  let A := intrinsicAbsoluteUnits K
  let B := intrinsicAbstractBase K
  let e := baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)
  let i := AlgebraicNumberTheory.separableEmbeddingIntoSeparableClosure K E
  let R : IntermediateField K (SeparableClosure K) := AlgHom.fieldRange i
  let : FiniteDimensional K R :=
    (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
  let : IsGalois K R := IsGalois.of_algEquiv (AlgEquiv.ofInjectiveField i)
  let L : FiniteGaloisSubextension B := {
    field := RamificationTheory.closedFixingSubgroup K (SeparableClosure K) R
    below := fixingSubgroupLeBase K (SeparableClosure K) R
    normal := inferInstance
    finite := baseFixingExtensionQuotient_finite
      K (SeparableClosure K) R }
  have hnormLe : additiveNormSubgroup K R ≤ H.toAddSubgroup := by
    intro x hx
    change Additive.toMul x ∈ localNormSubgroup K R at hx
    change Additive.toMul x ∈ H
    apply hnorm
    rw [← localNormSubgroup_fieldRange_eq K (SeparableClosure K) E i]
    exact hx
  have hmap :
      (L.normSubgroup A).map e.symm.toAddMonoidHom =
        additiveNormSubgroup K R := by
    simpa [A, B, L, R, e,
      FiniteGaloisSubextension.normSubgroup] using
      (map_finiteNormSubgroup_eq_additiveNormSubgroup
        K (SeparableClosure K) R)
  have hLE :
      L.normSubgroup A ≤ H.toAddSubgroup.map e.toAddMonoidHom := by
    intro x hx
    have hxmap : e.symm x ∈
        (L.normSubgroup A).map e.symm.toAddMonoidHom :=
      ⟨x, hx, rfl⟩
    rw [hmap] at hxmap
    exact ⟨e.symm x, hnormLe hxmap, e.apply_symm_apply x⟩
  exact (normTopology_addSubgroup_isOpen_iff A B
    (H.toAddSubgroup.map e.toAddMonoidHom)).2 ⟨L, hLE⟩

theorem

exists_finiteGaloisExtension_normSubgroup_map_le_of_normSubgroup_le

L252 ↗

LocalClassFieldTheory.exists_finiteGaloisExtension_normSubgroup_map_le_of_normSubgroup_le

Documentation

Package a concrete finite Galois extension in the absolute Galois model, retaining a prescribed upper bound for its ordinary norm subgroup.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K]
section LocalField
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem exists_finiteGaloisExtension_normSubgroup_map_le_of_normSubgroup_le
    (E : Type) [Field E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    (J : Subgroup Kˣ)
    (hnorm : localNormSubgroup K E ≤ J) :
    ∃ T : FiniteGaloisSubextension (intrinsicAbstractBase K),
      (T.normSubgroup (intrinsicAbsoluteUnits K)).map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom ≤
        J.toAddSubgroup

Module documentation

Surjectivity criteria for the local norm-subgroup map

Declarations

finiteAbelianNormSubgroup_compositum

finiteAbelianNormSubgroup_intersection

exists_finiteAbelianNormSubgroup_eq_of_normOpen

finiteAbelianNormSubgroupMap_surjective_of_normOpen

finiteIndexSubgroup_isNormOpen_of_normSubgroup_le

exists_finiteGaloisExtension_normSubgroup_map_le_of_normSubgroup_le