Module

AbsoluteAbelianization.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.AbsoluteAbelianization

14 declarations indexed from sourceView source ↗

Module documentation

Absolute abelianization inside the separable closure

For an arbitrary field, this module identifies the topological abelianization of the Galois group of its separable closure with the Galois group of the maximal abelian subextension. Working inside the separable closure makes the construction uniform in every characteristic.

Imports4

Mathlib.FieldTheory.Galois.Abelian
Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.IsSepClosed
Mathlib.Topology.Algebra.Group.TopologicalAbelianization

Imported by6

def

absoluteCommutatorClosure

L31 ↗

Documentation

The closure of the commutator subgroup of the separable absolute Galois group, packaged as a closed subgroup.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · full declaration

def absoluteCommutatorClosure :
    ClosedSubgroup Gal(SeparableClosure K / K) where
  toSubgroup :=
    (commutator Gal(SeparableClosure K / K)).topologicalClosure
  isClosed' := Subgroup.isClosed_topologicalClosure _

instance

absoluteCommutatorClosure_normal

L38 ↗

Documentation

The topological closure of the absolute commutator subgroup is normal.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

instance absoluteCommutatorClosure_normal :
    (absoluteCommutatorClosure K).Normal

def

maximalAbelianExtension

L45 ↗

Documentation

The maximal abelian subextension of the separable closure.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

def maximalAbelianExtension :
    IntermediateField K (SeparableClosure K)

instance

maximalAbelianExtension_isGalois

L50 ↗

Documentation

The maximal abelian subextension is Galois over the base field.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

instance maximalAbelianExtension_isGalois :
    IsGalois K (maximalAbelianExtension K)

def

absoluteAbelianizationMulEquivMaximalAbelianGalois

L63 ↗

Documentation

The algebraic quotient equivalence from the absolute topological abelianization to the Galois group of the maximal abelian extension.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

def absoluteAbelianizationMulEquivMaximalAbelianGalois :
    TopologicalAbelianization Gal(SeparableClosure K / K) ≃*
      Gal(maximalAbelianExtension K / K)

theorem

absoluteAbelianizationMulEquivMaximalAbelianGalois_mk

L71 ↗

Documentation

The algebraic equivalence sends a quotient class to restriction to the maximal abelian extension.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

theorem absoluteAbelianizationMulEquivMaximalAbelianGalois_mk
    (sigma : Gal(SeparableClosure K/K)) :
    absoluteAbelianizationMulEquivMaximalAbelianGalois K
        (QuotientGroup.mk sigma) =
      AlgEquiv.restrictNormalHom (maximalAbelianExtension K) sigma

theorem

absoluteAbelianizationMulEquivMaximalAbelianGalois_continuous

L79 ↗

Documentation

The algebraic equivalence from the absolute abelianization is continuous.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

theorem absoluteAbelianizationMulEquivMaximalAbelianGalois_continuous :
    Continuous (absoluteAbelianizationMulEquivMaximalAbelianGalois K)

def

absoluteTopologicalAbelianizationEquivMaximalAbelianGalois

L91 ↗

Documentation

The canonical topological identification of the absolute separable Galois group's abelianization with the maximal abelian Galois group.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

def absoluteTopologicalAbelianizationEquivMaximalAbelianGalois :
    TopologicalAbelianization Gal(SeparableClosure K / K) ≃ₜ*
      Gal(maximalAbelianExtension K / K)

instance

absoluteTopologicalAbelianization_totallyDisconnectedSpace

L108 ↗

Documentation

The absolute topological abelianization is totally disconnected.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

instance absoluteTopologicalAbelianization_totallyDisconnectedSpace :
    TotallyDisconnectedSpace
      (TopologicalAbelianization Gal(SeparableClosure K / K))

instance

maximalAbelianExtension_isAbelianGalois

L115 ↗

Documentation

The maximal abelian subextension has an abelian Galois group.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · full declaration

instance maximalAbelianExtension_isAbelianGalois :
    IsAbelianGalois K (maximalAbelianExtension K) where
  is_comm.comm sigma tau := by
    apply
      (absoluteTopologicalAbelianizationEquivMaximalAbelianGalois K).symm.injective
    simp only [map_mul]
    exact mul_comm _ _

theorem

finiteAbelianIntermediateField_le_maximalAbelianExtension

L125 ↗

Documentation

Every finite abelian intermediate field of the separable closure is contained in the maximal abelian extension.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

theorem finiteAbelianIntermediateField_le_maximalAbelianExtension
    (E : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K E] [IsAbelianGalois K E] :
    E ≤ maximalAbelianExtension K

def

finiteAbelianExtensionEmbeddingIntoMaximalAbelianExtension

L144 ↗

Documentation

A selected embedding of a finite abelian extension into the maximal abelian extension. Naming this embedding keeps downstream finite-coordinate arguments independent of the implementation of the separable closure.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

def finiteAbelianExtensionEmbeddingIntoMaximalAbelianExtension
    (L : Type*) [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    L →ₐ[K] maximalAbelianExtension K

def

finiteAbelianExtensionInMaximalAbelianExtension

L162 ↗

Documentation

The finite Galois intermediate field of the maximal abelian extension selected by a finite abelian extension.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

def finiteAbelianExtensionInMaximalAbelianExtension
    (L : Type*) [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    FiniteGaloisIntermediateField K (maximalAbelianExtension K)

def

finiteAbelianExtensionEquivInMaximalAbelianExtension

L173 ↗

Documentation

The selected finite layer is canonically equivalent to the original finite abelian extension.

Source context 3 commands

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

noncomputable section
open scoped IsMulCommutative
variable (K : Type) [Field K]

Lean source · statement

def finiteAbelianExtensionEquivInMaximalAbelianExtension
    (L : Type*) [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    L ≃ₐ[K] finiteAbelianExtensionInMaximalAbelianExtension K L

Module documentation

Absolute abelianization inside the separable closure

Declarations