NYLL
Module

CyclotomicTorsionFixedField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicTorsionFixedField
6 declarations indexed from sourceView source ↗

Module documentation

The cyclotomic torsion fixed field

rationalCyclotomicField now denotes the actual field ℚ(μ∞) inside SeparableClosure ℚ. Its actual Galois group is therefore the standard mathlib type rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField; its finite cyclotomic levels form a divisibility-directed system with supremum the whole field. The torsion fixed field is the actual intermediate field rationalCyclotomicTorsionFixedField.

The actual continuous cyclotomic character identifies the full Galois group with ℤ̂ˣ. Applying infinite Galois correspondence to the actual torsion closure and the group-theoretic decomposition of ℤ̂ˣ gives the cyclotomic ℤ̂-extension.

Imports14
Imported by2

Declarations

def

rationalCyclotomicTorsionRestrictionEquiv

L52 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicTorsionRestrictionEquiv
Source context 7 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open scoped IsMulCommutative
open KummerTheory
open ClassFormation
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (continuousMulEquivOfCompactToT2) in
Lean source · statement
def rationalCyclotomicTorsionRestrictionEquiv :
    (rationalCyclotomicField ≃ₐ[ℚ]
        rationalCyclotomicField) ⧸
        rationalCyclotomicTorsionClosure.toSubgroup ≃ₜ*
      (rationalCyclotomicTorsionFixedField ≃ₐ[ℚ]
        rationalCyclotomicTorsionFixedField)
def

rationalCyclotomicTorsionFixedFieldGalEquivZHat

L77 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicTorsionFixedFieldGalEquivZHat
Documentation

The Galois group of the actual torsion fixed field in ℚ(μ∞) is the additive group of the profinite integers, written multiplicatively.

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open scoped IsMulCommutative
open KummerTheory
open ClassFormation
Lean source · statement
def rationalCyclotomicTorsionFixedFieldGalEquivZHat :
    (rationalCyclotomicTorsionFixedField ≃ₐ[ℚ]
      rationalCyclotomicTorsionFixedField) ≃ₜ*
        Multiplicative ZHat
theorem

rationalCyclotomicTorsionRestrictionEquiv_apply_mk

L90 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicTorsionRestrictionEquiv_apply_mk
Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open scoped IsMulCommutative
open KummerTheory
open ClassFormation
Lean source · statement
theorem rationalCyclotomicTorsionRestrictionEquiv_apply_mk
    (σ :
      rationalCyclotomicField ≃ₐ[ℚ]
        rationalCyclotomicField) :
    rationalCyclotomicTorsionRestrictionEquiv
        (QuotientGroup.mk σ) =
      AlgEquiv.restrictNormalHom
        rationalCyclotomicTorsionFixedField σ
theorem

rationalCyclotomicTorsionRestrictionEquiv_symm_restrictNormal

L102 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicTorsionRestrictionEquiv_symm_restrictNormal
Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open scoped IsMulCommutative
open KummerTheory
open ClassFormation
Lean source · statement
theorem rationalCyclotomicTorsionRestrictionEquiv_symm_restrictNormal
    (σ :
      rationalCyclotomicField ≃ₐ[ℚ]
        rationalCyclotomicField) :
    rationalCyclotomicTorsionRestrictionEquiv.symm
        (AlgEquiv.restrictNormalHom
          rationalCyclotomicTorsionFixedField σ) =
      QuotientGroup.mk σ
theorem

rationalCyclotomicTorsionCoordinate_restrictNormal

L113 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicTorsionCoordinate_restrictNormal
Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open scoped IsMulCommutative
open KummerTheory
open ClassFormation
Lean source · statement
theorem rationalCyclotomicTorsionCoordinate_restrictNormal
    (σ :
      rationalCyclotomicField ≃ₐ[ℚ]
        rationalCyclotomicField) :
    torsionQuotientEquivOfZHatMulDecomposition
        (rationalCyclotomicField ≃ₐ[ℚ]
          rationalCyclotomicField)
        CyclotomicFinitePart
        (rationalCyclotomicCharacterContinuousMulEquiv.trans
          zHatUnitsDecomposition)
        dense_torsion_cyclotomicFinitePart
        (rationalCyclotomicTorsionRestrictionEquiv.symm
          (AlgEquiv.restrictNormalHom
            rationalCyclotomicTorsionFixedField σ)) =
      (zHatUnitsDecomposition
        (rationalCyclotomicCharacterContinuousMulEquiv σ)).1
theorem

rationalCyclotomicTorsionFixedFieldGalEquivZHat_restrictNormal

L142 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicTorsionFixedFieldGalEquivZHat_restrictNormal
Documentation

Restriction of an actual automorphism of the full rational cyclotomic field to the torsion fixed field is sent to the genuine torsion-free coordinate of its cyclotomic character.

Source context 6 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open scoped IsMulCommutative
open KummerTheory
open ClassFormation
Lean source · statement
theorem
    rationalCyclotomicTorsionFixedFieldGalEquivZHat_restrictNormal
    (σ :
      rationalCyclotomicField ≃ₐ[ℚ]
        rationalCyclotomicField) :
    rationalCyclotomicTorsionFixedFieldGalEquivZHat
        (AlgEquiv.restrictNormalHom
          rationalCyclotomicTorsionFixedField σ) =
      (zHatUnitsDecomposition
        (rationalCyclotomicCharacterContinuousMulEquiv σ)).1

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