Module

RelativeAbelianization.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.RelativeAbelianization

9 declarations indexed from sourceView source ↗

Module documentation

Relative topological abelianization

For a possibly infinite Galois extension M/F, this file identifies the topological abelianization of Gal(M/F) with the Galois group of the intermediate field fixed by the closed commutator subgroup.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.AbsoluteAbelianization

Imported by1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.All

def

relativeCommutatorClosure

L30 ↗

ClassFieldTower.Martinet.relativeCommutatorClosure

Documentation

Closed commutator subgroup of a relative, possibly infinite, Galois group.

Source context 6 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]

Lean source · full declaration

def relativeCommutatorClosure : ClosedSubgroup Gal(M / F) where
  toSubgroup := (commutator Gal(M / F)).topologicalClosure
  isClosed' := Subgroup.isClosed_topologicalClosure _

instance

relativeCommutatorClosure_normal

L34 ↗

ClassFieldTower.Martinet.relativeCommutatorClosure_normal

Source context 6 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]

Lean source · statement

instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal

def

relativeMaximalAbelianSubextension

L40 ↗

ClassFieldTower.Martinet.relativeMaximalAbelianSubextension

Documentation

Maximal abelian intermediate field of a relative Galois extension.

Source context 7 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance

Lean source · statement

def relativeMaximalAbelianSubextension : IntermediateField F M

theorem

relativeMaximalAbelianSubextension_isGalois

L44 ↗

ClassFieldTower.Martinet.relativeMaximalAbelianSubextension_isGalois

Documentation

The relative maximal abelian subextension is Galois.

Source context 7 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance

Lean source · statement

theorem relativeMaximalAbelianSubextension_isGalois :
    IsGalois F (relativeMaximalAbelianSubextension F M)

instance

instIsGalois

L54 ↗

ClassFieldTower.Martinet.relativeMaximalAbelianSubextension.instIsGalois

Source context 7 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance

Lean source · statement

instance relativeMaximalAbelianSubextension.instIsGalois :
    IsGalois F (relativeMaximalAbelianSubextension F M)

def

relativeAbelianizationMulEquiv

L59 ↗

ClassFieldTower.Martinet.relativeAbelianizationMulEquiv

Documentation

Algebraic quotient equivalence for relative abelianization.

Source context 8 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance
local instance relativeMaximalAbelianSubextension.instIsGalois :
    IsGalois F (relativeMaximalAbelianSubextension F M) :=
  relativeMaximalAbelianSubextension_isGalois F M

Lean source · statement

def relativeAbelianizationMulEquiv :
    TopologicalAbelianization Gal(M / F) ≃*
      Gal(relativeMaximalAbelianSubextension F M / F)

theorem

relativeAbelianizationMulEquiv_mk

L66 ↗

ClassFieldTower.Martinet.relativeAbelianizationMulEquiv_mk

Documentation

The quotient equivalence sends a class to restriction.

Source context 8 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance
local instance relativeMaximalAbelianSubextension.instIsGalois :
    IsGalois F (relativeMaximalAbelianSubextension F M) :=
  relativeMaximalAbelianSubextension_isGalois F M

Lean source · statement

theorem relativeAbelianizationMulEquiv_mk (sigma : Gal(M/F)) :
    relativeAbelianizationMulEquiv F M (QuotientGroup.mk sigma) =
      AlgEquiv.restrictNormalHom (relativeMaximalAbelianSubextension F M) sigma

theorem

relativeAbelianizationMulEquiv_continuous

L72 ↗

ClassFieldTower.Martinet.relativeAbelianizationMulEquiv_continuous

Documentation

The algebraic relative-abelianization equivalence is continuous.

Source context 8 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance
local instance relativeMaximalAbelianSubextension.instIsGalois :
    IsGalois F (relativeMaximalAbelianSubextension F M) :=
  relativeMaximalAbelianSubextension_isGalois F M

Lean source · statement

theorem relativeAbelianizationMulEquiv_continuous :
    Continuous (relativeAbelianizationMulEquiv F M)

def

relativeTopologicalAbelianizationEquiv

L83 ↗

ClassFieldTower.Martinet.relativeTopologicalAbelianizationEquiv

Documentation

The topological abelianization is the Galois group of the maximal relative abelian subfield.

Source context 8 commands

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

open scoped IsMulCommutative
noncomputable section
universe u v
namespace ClassFieldTower.Martinet
variable (F : Type u) (M : Type v)
variable [Field F] [Field M] [Algebra F M] [IsGalois F M]
local instance relativeCommutatorClosure_normal :
    (relativeCommutatorClosure F M).Normal := by
  change ((commutator Gal(M / F)).topologicalClosure).Normal
  infer_instance
local instance relativeMaximalAbelianSubextension.instIsGalois :
    IsGalois F (relativeMaximalAbelianSubextension F M) :=
  relativeMaximalAbelianSubextension_isGalois F M

Lean source · statement

def relativeTopologicalAbelianizationEquiv :
    TopologicalAbelianization Gal(M / F) ≃ₜ*
      Gal(relativeMaximalAbelianSubextension F M / F)

Module documentation

Relative topological abelianization

Declarations