Module

PrincipalIdealTower.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.PrincipalIdealTower

9 declarations indexed from sourceView source ↗

Module documentation

Galois structure on a conjugate-stable abelian tower

The principal ideal theorem uses two successive finite abelian class fields. The upper field is Galois over the original base once its absolute Galois subgroup is stable under conjugation by the base subgroup. This file packages that actual subgroup statement as a finite Galois subextension, so that the commutator-intermediate-field and transfer APIs can be applied to the tower.

Imports4

Imported by2

theorem

conjugateClosedSubgroup_eq_self_of_mem

L43 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.conjugateClosedSubgroup_eq_self_of_mem

Documentation

Conjugation by an element of a closed subgroup preserves that subgroup. This is the subgroup form of the fact that every field automorphism over the base fixes the base field setwise.

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section Conjugation
variable [ContinuousMul G]

Lean source · statement

theorem conjugateClosedSubgroup_eq_self_of_mem
    (K : ClosedSubgroup G) {s : G} (hs : s ∈ K) :
    conjugateClosedSubgroup K s = K

def

conjugateFiniteAbelianSubextension

L60 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFiniteAbelianSubextension

Documentation

Conjugating both endpoints of a finite abelian extension produces the actual conjugate finite abelian extension.

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section Conjugation
variable [ContinuousMul G]

Lean source · full declaration

def conjugateFiniteAbelianSubextension
    (L : FiniteAbelianSubextension K) (s : G) :
    FiniteAbelianSubextension (conjugateClosedSubgroup K s) where
  toFiniteGaloisExtension :=
    { field := conjugateClosedSubgroup L.field s
      below := conjugateClosedSubgroup_mono L.below s
      normal := by
        let :
            (CyclicCohomology.extensionSubgroup K L.field L.below).Normal :=
          L.normal
        infer_instance
      finite := by
        let : Finite
            (K.toSubgroup ⧸
              CyclicCohomology.extensionSubgroup K L.field L.below) :=
          L.finite
        exact finite_conjugateExtension K L.field L.below s }
  commutative := by
    let : (CyclicCohomology.extensionSubgroup K L.field L.below).Normal :=
      L.normal
    let e :=
      finiteReciprocityNaturalityConjugation K L.field L.below s
    refine ⟨⟨?_⟩⟩
    intro x y
    obtain ⟨x', rfl⟩ := e.surjective x
    obtain ⟨y', rfl⟩ := e.surjective y
    calc
      e x' * e y' = e (x' * y') := (map_mul e x' y').symm
      _ = e (y' * x') := congrArg e (L.commutative.is_comm.comm _ _)
      _ = e y' * e x' := map_mul e y' x'

theorem

conjugateFiniteAbelianSubextension_field

L92 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.conjugateFiniteAbelianSubextension_field

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section Conjugation
variable [ContinuousMul G]

Lean source · statement

theorem conjugateFiniteAbelianSubextension_field
    (L : FiniteAbelianSubextension K) (s : G) :
    (conjugateFiniteAbelianSubextension L s).field =
      conjugateClosedSubgroup L.field s

def

galoisSubextensionOfConjugateStableAbelianTower

L101 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.galoisSubextensionOfConjugateStableAbelianTower

Documentation

Two successive finite abelian extensions form a finite Galois extension over the original base when the top-field subgroup is stable under conjugation by every element of the base subgroup.

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section Conjugation
variable [ContinuousMul G]

Lean source · full declaration

def galoisSubextensionOfConjugateStableAbelianTower
    (L : FiniteAbelianSubextension K)
    (M : FiniteAbelianSubextension L.field)
    (hstable : ∀ s : K.toSubgroup,
      conjugateClosedSubgroup M.field s.1 = M.field) :
    FiniteGaloisSubextension K where
  field := M.field
  below := M.below.trans L.below
  normal := by
    refine Subgroup.Normal.mk ?_
    intro q hq r
    apply
      (mem_extensionSubgroup_iff
        K M.field (M.below.trans L.below) _).2
    have hqM : (q : G) ∈ M.field :=
      (mem_extensionSubgroup_iff
        K M.field (M.below.trans L.below) q).1 hq
    have hqConj :
        (q : G) ∈ conjugateClosedSubgroup M.field (r : G) := by
      rw [hstable r]
      exact hqM
    exact
      (conjugateClosedSubgroup_mem M.field (r : G) (q : G)).1 hqConj
  finite := by
    let : Finite
        (L.field.toSubgroup ⧸
          CyclicCohomology.extensionSubgroup L.field M.field M.below) :=
      M.finite
    let : Finite
        (K.toSubgroup ⧸
          CyclicCohomology.extensionSubgroup K L.field L.below) :=
      L.finite
    exact
      FiniteGaloisSubextension.finite_extension_trans M.below L.below

theorem

galoisSubextensionOfConjugateStableAbelianTower_field

L137 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.galoisSubextensionOfConjugateStableAbelianTower_field

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section Conjugation
variable [ContinuousMul G]

Lean source · statement

theorem galoisSubextensionOfConjugateStableAbelianTower_field
    (L : FiniteAbelianSubextension K)
    (M : FiniteAbelianSubextension L.field)
    (hstable : ∀ s : K.toSubgroup,
      conjugateClosedSubgroup M.field s.1 = M.field) :
    (galoisSubextensionOfConjugateStableAbelianTower
      L M hstable).field = M.field

def

maximalAbelianSubextension

L154 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.maximalAbelianSubextension

Documentation

The intermediate field fixed by the commutator of a finite Galois extension, bundled as the actual maximal finite abelian subextension.

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section MaximalAbelianIntermediate
variable [IsTopologicalGroup G]

Lean source · statement

def maximalAbelianSubextension
    (P : FiniteGaloisSubextension K) :
    FiniteAbelianSubextension K

theorem

maximalAbelianSubextension_field

L161 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.maximalAbelianSubextension_field

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section MaximalAbelianIntermediate
variable [IsTopologicalGroup G]

Lean source · statement

theorem maximalAbelianSubextension_field
    (P : FiniteGaloisSubextension K) :
    (maximalAbelianSubextension P).field =
      P.abelianIntermediateField

theorem

abelianIntermediateField_le_of_finiteAbelianIntermediate

L174 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.abelianIntermediateField_le_of_finiteAbelianIntermediate

Documentation

Every finite abelian intermediate extension of a finite Galois extension is contained in the commutator-fixed intermediate field.

In subgroup order the displayed inclusion is reversed: the subgroup representing the maximal abelian intermediate field lies inside the subgroup representing the given abelian intermediate field.

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section MaximalAbelianIntermediate
variable [IsTopologicalGroup G]

Lean source · statement

theorem abelianIntermediateField_le_of_finiteAbelianIntermediate
    (P : FiniteGaloisSubextension K)
    (L : FiniteAbelianSubextension K)
    (hPL : P.field.toSubgroup ≤ L.field.toSubgroup) :
    P.abelianIntermediateField.toSubgroup ≤
      L.field.toSubgroup

theorem

finiteAbelianIntermediate_le_maximalAbelianSubextension

L215 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.finiteAbelianIntermediate_le_maximalAbelianSubextension

Documentation

In field order, every finite abelian intermediate extension lies below the maximal abelian subextension cut out by the commutator.

Source context 9 commands

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

noncomputable section
universe u
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation KummerTheory
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : ClosedSubgroup G}
section MaximalAbelianIntermediate
variable [IsTopologicalGroup G]

Lean source · statement

theorem finiteAbelianIntermediate_le_maximalAbelianSubextension
    (P : FiniteGaloisSubextension K)
    (L : FiniteAbelianSubextension K)
    (hPL : P.field.toSubgroup ≤ L.field.toSubgroup) :
    L ≤ maximalAbelianSubextension P

Module documentation

Galois structure on a conjugate-stable abelian tower

Declarations