Module

FiniteGaloisRealizationSubextension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FiniteGaloisRealizationSubextension

8 declarations indexed from sourceView source ↗

Module documentation

The finite Galois subextension attached to a number-field tower

This module realizes L / K as a finite Galois subextension inside the common rational separable closure. It packages the relevant fixing subgroups, normality, and finite-index data for abstract reciprocity.

Imports2

Imported by4

theorem

numberFieldTowerExtensionSubgroup_normal

L42 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionSubgroup_normal

Documentation

The relative fixing subgroup in the compatible realization is normal. This is the existing LCFT ambient-embedding theorem specialized to the number-field tower.

Source context 11 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem numberFieldTowerExtensionSubgroup_normal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal

theorem

numberFieldTowerExtensionQuotient_finite

L66 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionQuotient_finite

Documentation

The relative quotient of fixing subgroups in the compatible realization is finite.

Source context 11 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

theorem numberFieldTowerExtensionQuotient_finite :
    letI :=
      numberFieldTowerExtensionSubgroup_normal K L
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let j := numberFieldSeparableClosureEmbedding L
  let i :=
    j.comp (IsScalarTower.toAlgHom ℚ K L)
  let : Algebra K (SeparableClosure ℚ) :=
    i.toRingHom.toAlgebra
  let e := numberFieldTowerSeparableClosureEquiv K L
  change
    Finite
      ((closedFixingSubgroup ℚ (SeparableClosure ℚ)
          (AlgHom.fieldRange i)).toSubgroup ⧸
        extensionSubgroup
          (closedFixingSubgroup ℚ (SeparableClosure ℚ)
            (AlgHom.fieldRange i))
          (closedFixingSubgroup ℚ (SeparableClosure ℚ)
            (AlgHom.fieldRange j))
          _)
  exact
    ambientEmbeddedExtensionQuotient_finite
      ℚ K L j e

def

numberFieldTowerFiniteGaloisSubextension

L97 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteGaloisSubextension

Documentation

The compatible realization of L / K as the finite Galois subextension consumed by abstract reciprocity.

Source context 11 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

def numberFieldTowerFiniteGaloisSubextension :
    FiniteGaloisSubextension
      (numberFieldTowerBaseSubgroup K L) where
  field := numberFieldTowerTopSubgroup L
  below := numberFieldTowerTopSubgroup_le_baseSubgroup K L
  normal := numberFieldTowerExtensionSubgroup_normal K L
  finite := by
    let :=
      numberFieldTowerExtensionSubgroup_normal K L
    exact numberFieldTowerExtensionQuotient_finite K L

def

numberFieldTowerFiniteAbstractField

L111 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteAbstractField

Documentation

The lower fixing subgroup, with its finite absolute-index witness, is the finite abstract field consumed by abstract reciprocity.

Source context 11 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

def numberFieldTowerFiniteAbstractField :
    FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ) where
  field := numberFieldTowerBaseSubgroup K L
  finite := by
    simpa only [numberFieldTowerBaseSubgroup,
      numberFieldTowerBaseField] using
      (ambientEmbeddedAbsoluteQuotientFinite
        ℚ K (numberFieldTowerLowerEmbedding K L))

theorem

numberFieldTowerBaseSubgroup_isOpen

L124 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseSubgroup_isOpen

Documentation

The compatible embedded absolute Galois subgroup of a number field is open in the rational absolute Galois group.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem numberFieldTowerBaseSubgroup_isOpen :
    IsOpen
      ((numberFieldTowerBaseSubgroup K L :
          ClosedSubgroup
            (Gal(SeparableClosure ℚ / ℚ))) :
        Set (Gal(SeparableClosure ℚ / ℚ)))

def

numberFieldTowerExtensionQuotientEquivGaloisGroup

L137 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionQuotientEquivGaloisGroup

Documentation

The quotient represented by the compatible abstract subextension is the actual Gal(L / K).

Source context 11 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def
    numberFieldTowerExtensionQuotientEquivGaloisGroup :
    (numberFieldTowerFiniteGaloisSubextension K L).extensionQuotient ≃*
      Gal(L / K)

theorem

numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_baseSubgroupEquiv

L171 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_baseSubgroupEquiv

Documentation

Under the compatible realization, the finite quotient class of an absolute automorphism is its genuine restriction to L.

Source context 11 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open AlgebraicNumberTheory
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

theorem
    numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_baseSubgroupEquiv
    (σ :
      letI : Algebra K (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureBaseAlgebra K L
      Gal(SeparableClosure ℚ / K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI :=
      numberFieldTowerExtensionSubgroup_normal K L
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
        (QuotientGroup.mk
          (numberFieldTowerSeparableClosureEquivBaseSubgroup
            K L σ)) =
      AlgEquiv.restrictNormalHom L σ := by
  let j :=
    numberFieldSeparableClosureEmbedding L
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let e :=
    numberFieldTowerSeparableClosureEquiv K L
  let :=
    numberFieldTowerExtensionSubgroup_normal K L
  apply AlgEquiv.ext
  intro x
  apply j.injective
  calc
    j
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (QuotientGroup.mk
            (numberFieldTowerSeparableClosureEquivBaseSubgroup
              K L σ)) x) =
        (numberFieldTowerSeparableClosureEquivBaseSubgroup
          K L σ).1.1 (j x) := by
      convert
        (ambientEmbeddedExtensionQuotientEquivGaloisGroup_mk_apply
          ℚ K L j e
          (numberFieldTowerSeparableClosureEquivBaseSubgroup
            K L σ) x) using 1; rfl
    _ = σ (j x) := rfl
    _ =
        j
          ((AlgEquiv.restrictNormalHom L σ) x) := by
      exact
        (AlgEquiv.restrictNormal_commutes σ L x).symm

def

numberFieldTowerFiniteAbelianSubextension

L241 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteAbelianSubextension

Documentation

The compatible finite Galois realization of an abelian number field extension, bundled with commutativity of its actual abstract quotient.

Source context 7 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

def numberFieldTowerFiniteAbelianSubextension
    [hAbelian : IsAbelianGalois K L] :
    FiniteAbelianSubextension
      (numberFieldTowerBaseSubgroup K L)

Module documentation

The finite Galois subextension attached to a number-field tower

Declarations