NYLL
Module

FiniteGaloisRealizationCore.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FiniteGaloisRealizationCore
28 declarations indexed from sourceView source ↗

Module documentation

Finite Galois number-field extensions in the rational separable closure

An actual tower L / K / ℚ must be realized by compatible embeddings before the rational absolute class formation can be applied. We choose only the upper embedding L →ₐ[ℚ] SeparableClosure ℚ; the lower embedding is its restriction along K →ₐ[ℚ] L. Thus the two field ranges, their fixing subgroups, and the norm comparison all come from the existing mathlib and LCFT constructions.

No second model of a number field, an idele class group, or a norm quotient is introduced here.

Imports10
Imported by3

Declarations

def

numberFieldTowerLowerEmbedding

L54 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerLowerEmbedding
Documentation

The embedding of the lower field obtained by restricting the one chosen embedding of the top field.

Source context 10 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 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 numberFieldTowerLowerEmbedding :
    K →ₐ[ℚ] SeparableClosure ℚ
def

numberFieldTowerBaseField

L61 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseField
Documentation

The copy of K obtained from the chosen copy of L; this is the lower field in the compatible realization of L / K.

Source context 10 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 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 numberFieldTowerBaseField :
    IntermediateField ℚ (SeparableClosure ℚ)
theorem

numberFieldTowerBaseField_le_topField

L68 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseField_le_topField
Documentation

The compatible embedded copy of K lies in the chosen embedded copy of 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 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 numberFieldTowerBaseField_le_topField :
    numberFieldTowerBaseField K L ≤
      numberFieldInRationalSeparableClosure L
instance

numberFieldTowerBaseFieldAlgebra

L76 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseFieldAlgebra
Documentation

The standard inclusion algebra on the two nested field ranges.

Source context 10 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 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
instance numberFieldTowerBaseFieldAlgebra :
    Algebra (numberFieldTowerBaseField K L)
      (numberFieldInRationalSeparableClosure L)
instance

numberFieldTowerBaseFieldScalarTower

L82 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseFieldScalarTower
Source context 10 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 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
instance numberFieldTowerBaseFieldScalarTower :
    IsScalarTower ℚ (numberFieldTowerBaseField K L)
      (numberFieldInRationalSeparableClosure L)
instance

numberFieldTowerBaseField_finiteDimensional

L87 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseField_finiteDimensional
Source context 10 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 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
instance numberFieldTowerBaseField_finiteDimensional :
    FiniteDimensional ℚ (numberFieldTowerBaseField K L)
instance

numberFieldTowerBaseField_numberField

L91 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseField_numberField
Source context 10 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 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
instance numberFieldTowerBaseField_numberField :
    NumberField (numberFieldTowerBaseField K L)
instance

numberFieldTowerTopField_finiteDimensional

L95 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerTopField_finiteDimensional
Source context 10 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 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
instance numberFieldTowerTopField_finiteDimensional :
    FiniteDimensional (numberFieldTowerBaseField K L)
      (numberFieldInRationalSeparableClosure L)
theorem

numberFieldTowerFieldRangeEquiv_algebraMap

L106 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFieldRangeEquiv_algebraMap
Documentation

The two field-range equivalences form the same square as the original tower 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 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 numberFieldTowerFieldRangeEquiv_algebraMap (x : K) :
    (numberFieldSeparableClosureEmbedding L).equivFieldRange
        (algebraMap K L x) =
      algebraMap (numberFieldTowerBaseField K L)
        (numberFieldInRationalSeparableClosure L)
        ((numberFieldTowerLowerEmbedding K L).equivFieldRange x)
instance

numberFieldTowerTopField_isGalois

L114 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerTopField_isGalois
Source context 10 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 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
instance numberFieldTowerTopField_isGalois :
    IsGalois (numberFieldTowerBaseField K L)
      (numberFieldInRationalSeparableClosure L)
def

numberFieldTowerBaseSubgroup

L138 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseSubgroup
Documentation

The closed subgroup representing the compatible embedded copy of K.

Source context 10 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 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 numberFieldTowerBaseSubgroup :
    ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
def

numberFieldTowerTopSubgroup

L145 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerTopSubgroup
Documentation

The closed subgroup representing the chosen embedded copy of L.

Source context 10 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 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 numberFieldTowerTopSubgroup :
    ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
theorem

numberFieldTowerTopSubgroup_le_baseSubgroup

L154 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerTopSubgroup_le_baseSubgroup
Documentation

Inclusion of compatible field ranges gives the contravariant inclusion of their fixing subgroups.

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 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 numberFieldTowerTopSubgroup_le_baseSubgroup :
    (numberFieldTowerTopSubgroup L).toSubgroup ≤
      (numberFieldTowerBaseSubgroup K L).toSubgroup
def

numberFieldTowerSeparableClosureEquiv

L167 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureEquiv
Documentation

The separable closure of K is identified with SeparableClosure ℚ endowed with the algebra structure induced by the compatible lower embedding.

Source context 10 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 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 numberFieldTowerSeparableClosureEquiv :
    let i := numberFieldTowerLowerEmbedding K L
    letI : Algebra K (SeparableClosure ℚ) :=
      i.toRingHom.toAlgebra
    SeparableClosure K ≃ₐ[K] SeparableClosure ℚ := by
  dsimp only
  let i := numberFieldTowerLowerEmbedding K L
  let _ : Algebra K (SeparableClosure ℚ) :=
    i.toRingHom.toAlgebra
  letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    IsScalarTower.of_algebraMap_eq' i.comp_algebraMap.symm
  letI : Algebra.IsSeparable K (SeparableClosure ℚ) :=
    Algebra.isSeparable_tower_top_of_isSeparable
      ℚ K (SeparableClosure ℚ)
  letI : IsSepClosure K (SeparableClosure ℚ) :=
    ⟨inferInstance, inferInstance⟩
  exact
    IsSepClosure.equiv K
      (SeparableClosure K) (SeparableClosure ℚ)
def

numberFieldTowerSeparableClosureBaseAlgebra

L190 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureBaseAlgebra
Documentation

The algebra structure on the rational separable closure induced by the compatible lower embedding in a number-field tower.

Source context 10 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 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 numberFieldTowerSeparableClosureBaseAlgebra :
    Algebra K (SeparableClosure ℚ)
def

numberFieldTowerSeparableClosureTopAlgebra

L197 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureTopAlgebra
Documentation

The algebra structure on the rational separable closure induced by the chosen embedding of the top number field.

Source context 10 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 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 numberFieldTowerSeparableClosureTopAlgebra :
    Algebra L (SeparableClosure ℚ)
theorem

numberFieldTowerSeparableClosureBaseScalarTower

L204 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureBaseScalarTower
Documentation

The compatible lower embedding also realizes the standard ℚ → K scalar tower inside the rational separable closure.

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 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 · full declaration
theorem numberFieldTowerSeparableClosureBaseScalarTower :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    IsScalarTower ℚ K (SeparableClosure ℚ) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  exact
    IsScalarTower.of_algebraMap_eq'
      (numberFieldTowerLowerEmbedding K L).comp_algebraMap.symm
theorem

numberFieldTowerSeparableClosureTopScalarTower

L216 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureTopScalarTower
Documentation

The chosen top-field embedding realizes the standard ℚ → L scalar tower inside the rational separable closure.

Source context 10 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 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 numberFieldTowerSeparableClosureTopScalarTower :
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    IsScalarTower ℚ L (SeparableClosure ℚ) := by
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  exact
    IsScalarTower.of_algebraMap_eq'
      (numberFieldSeparableClosureEmbedding L).comp_algebraMap.symm
theorem

numberFieldSeparableClosureTop_isGalois

L229 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldSeparableClosureTop_isGalois
Documentation

With the algebra structure induced by its chosen rational embedding, the rational separable closure is a genuine Galois overfield of a number field.

Source context 10 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 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 numberFieldSeparableClosureTop_isGalois :
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    IsGalois L (SeparableClosure ℚ) := by
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower ℚ L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopScalarTower L
  let : Algebra.IsSeparable L (SeparableClosure ℚ) :=
    Algebra.isSeparable_tower_top_of_isSeparable
      ℚ L (SeparableClosure ℚ)
  let : IsSepClosure L (SeparableClosure ℚ) :=
    ⟨inferInstance, inferInstance⟩
  exact
    IsGalois.of_algEquiv
      (IsSepClosure.equiv L
        (SeparableClosure L) (SeparableClosure ℚ))
theorem

numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower

L249 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower
Documentation

The actual cyclotomic ZHat-compositum of a number field and the chosen rational separable closure form the expected scalar tower.

Source context 10 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 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
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower :
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) := by
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  exact IsScalarTower.of_algebraMap_eq' rfl
theorem

numberFieldTowerSeparableClosureScalarTower

L263 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureScalarTower
Documentation

The two compatible embeddings make the rational separable closure an actual scalar tower over K → 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 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 · full declaration
theorem numberFieldTowerSeparableClosureScalarTower :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    IsScalarTower K L (SeparableClosure ℚ) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  exact IsScalarTower.of_algebraMap_eq' rfl
theorem

numberFieldTowerSeparableClosure_isGalois

L278 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosure_isGalois
Documentation

With the compatible lower embedding, the rational separable closure is a genuine Galois overfield of the original base field.

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 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 · full declaration
theorem numberFieldTowerSeparableClosure_isGalois :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    IsGalois K (SeparableClosure ℚ) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  exact
    IsGalois.of_algEquiv
      (numberFieldTowerSeparableClosureEquiv K L)
def

numberFieldTowerSeparableClosureRestriction

L291 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureRestriction
Documentation

Continuous restriction from the compatible separable closure to the actual finite Galois extension in the original number-field tower.

Source context 10 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 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 numberFieldTowerSeparableClosureRestriction :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    Gal(SeparableClosure ℚ / K) →ₜ*
      Gal(L / K) := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let _ : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let _ : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let eL : L →ₐ[K] SeparableClosure ℚ :=
    IsScalarTower.toAlgHom K L (SeparableClosure ℚ)
  let E : IntermediateField K (SeparableClosure ℚ) :=
    eL.fieldRange
  letI : FiniteDimensional K E :=
    eL.equivFieldRange.toLinearEquiv.finiteDimensional
  letI : IsGalois K E :=
    IsGalois.of_algEquiv eL.equivFieldRange
  let c :
      Gal(L / K) ≃*
        Gal(E / K) :=
    AlgEquiv.autCongr eL.equivFieldRange
  let rE :
      Gal(SeparableClosure ℚ / K) →*
        Gal(E / K) :=
    AlgEquiv.restrictNormalHom E
  refine
    { toMonoidHom :=
        AlgEquiv.restrictNormalHom L
      continuous_toFun := ?_ }
  have hrE : Continuous rE :=
    InfiniteGalois.restrictNormalHom_continuous E
  have hc : Continuous c.symm :=
    continuous_of_discreteTopology
  apply (hc.comp hrE).congr
  intro σ
  apply AlgEquiv.ext
  intro x
  apply eL.injective
  change
    eL
        (((AlgEquiv.autCongr eL.equivFieldRange).symm
          (AlgEquiv.restrictNormalHom E σ)) x) =
      eL ((AlgEquiv.restrictNormalHom L σ) x)
  have he (y : E) :
      eL (eL.equivFieldRange.symm y) = E.val y := by
    exact
      congrArg Subtype.val
        (eL.equivFieldRange.apply_symm_apply y)
  calc
    eL
          (((AlgEquiv.autCongr eL.equivFieldRange).symm
            (AlgEquiv.restrictNormalHom E σ)) x) =
        E.val
          ((AlgEquiv.restrictNormalHom E σ)
            (eL.equivFieldRange x)) := by
      simpa only [AlgEquiv.autCongr_symm,
        AlgEquiv.autCongr_apply, AlgEquiv.trans_apply,
        AlgEquiv.symm_symm] using
        he
          ((AlgEquiv.restrictNormalHom E σ)
            (eL.equivFieldRange x))
    _ = σ (eL x) := by
      exact
        AlgEquiv.restrictNormal_commutes σ E
          (eL.equivFieldRange x)
    _ = eL ((AlgEquiv.restrictNormalHom L σ) x) := by
      exact
        (AlgEquiv.restrictNormal_commutes σ L x).symm
theorem

numberFieldTowerSeparableClosureRestriction_apply

L369 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureRestriction_apply
Documentation

The compatible continuous restriction evaluates as ordinary normal-field restriction.

Source context 10 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 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 numberFieldTowerSeparableClosureRestriction_apply
    (σ :
      letI : Algebra K (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureBaseAlgebra K L
      letI : Algebra L (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureTopAlgebra L
      letI : IsScalarTower K L (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureScalarTower 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
    numberFieldTowerSeparableClosureRestriction K L σ =
      AlgEquiv.restrictNormalHom L σ := by
  let _ : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let _ : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let _ : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  change
    (numberFieldTowerSeparableClosureRestriction K L).toMonoidHom σ =
      AlgEquiv.restrictNormalHom L σ
  rfl
theorem

numberFieldTowerSeparableClosureRestriction_surjective

L399 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureRestriction_surjective
Documentation

Restriction from the compatible separable closure onto the finite Galois top field is surjective.

Source context 10 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 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 numberFieldTowerSeparableClosureRestriction_surjective :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    Function.Surjective
      (numberFieldTowerSeparableClosureRestriction K L) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let _ : IsGalois K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosure_isGalois K L
  intro τ
  obtain ⟨σ, hσ⟩ :=
    AlgEquiv.restrictNormalHom_surjective
      (F := K) (K₁ := L) (E := SeparableClosure ℚ) τ
  refine ⟨σ, ?_⟩
  rw [numberFieldTowerSeparableClosureRestriction_apply]
  exact hσ
def

numberFieldTowerSeparableClosureToBaseSubgroup

L427 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureToBaseSubgroup
Documentation

A K-automorphism of the common rational separable closure, viewed as the corresponding rational automorphism fixing the embedded copy of K.

Source context 10 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 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 numberFieldTowerSeparableClosureToBaseSubgroup :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    Gal(SeparableClosure ℚ / K) →*
      (numberFieldTowerBaseSubgroup K L).toSubgroup := by
  let _ : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  refine
    { toFun := fun σ =>
        ⟨AlgEquiv.restrictScalars ℚ σ, ?_⟩
      map_one' := by
        apply Subtype.ext
        rfl
      map_mul' := by
        intro σ τ
        apply Subtype.ext
        rfl }
  change
    AlgEquiv.restrictScalars ℚ σ ∈
      (numberFieldTowerBaseField K L).fixingSubgroup
  rw [IntermediateField.mem_fixingSubgroup_iff]
  intro x hx
  obtain ⟨y, rfl⟩ := hx
  exact σ.commutes y
def

numberFieldTowerSeparableClosureEquivBaseSubgroup

L455 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureEquivBaseSubgroup
Documentation

The compatible K-absolute Galois group is exactly the fixing subgroup of the embedded copy of K inside the rational absolute Galois group.

Source context 10 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 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 numberFieldTowerSeparableClosureEquivBaseSubgroup :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    Gal(SeparableClosure ℚ / K) ≃*
      (numberFieldTowerBaseSubgroup K L).toSubgroup := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  refine
    { toFun := numberFieldTowerSeparableClosureToBaseSubgroup K L
      invFun := fun τ =>
        { τ.1 with
          commutes' := fun x => ?_ }
      left_inv := ?_
      right_inv := ?_
      map_mul' := map_mul
        (numberFieldTowerSeparableClosureToBaseSubgroup K L) }
  · have hτ :
        ∀ z ∈ numberFieldTowerBaseField K L,
          τ.1 z = z := by
      exact
        (IntermediateField.mem_fixingSubgroup_iff
          (numberFieldTowerBaseField K L) τ.1).1 τ.2
    exact
      hτ
        (numberFieldTowerLowerEmbedding K L x)
        ⟨x, rfl⟩
  · intro σ
    apply AlgEquiv.ext
    intro x
    rfl
  · intro τ
    apply Subtype.ext
    apply AlgEquiv.ext
    intro x
    rfl
theorem

numberFieldTowerSeparableClosureEquivBaseSubgroup_apply_coe

L495 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerSeparableClosureEquivBaseSubgroup_apply_coe
Documentation

Coercing the base-subgroup comparison equivalence gives restriction of scalars to the rational base.

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 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 · full declaration
theorem numberFieldTowerSeparableClosureEquivBaseSubgroup_apply_coe
    (σ :
      letI : Algebra K (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureBaseAlgebra K L
      Gal(SeparableClosure ℚ / K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    ((numberFieldTowerSeparableClosureEquivBaseSubgroup K L σ :
        (numberFieldTowerBaseSubgroup K L).toSubgroup) :
      Gal(SeparableClosure ℚ / ℚ)) =
      AlgEquiv.restrictScalars ℚ σ := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  change
    (numberFieldTowerSeparableClosureToBaseSubgroup K L σ).1 =
      AlgEquiv.restrictScalars ℚ σ
  rfl

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.