Module

CyclotomicUnramifiedRestriction.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicUnramifiedRestriction

8 declarations indexed from sourceView source ↗

Module documentation

Finite restriction of cyclotomic fixed-field reciprocity

For an unramified finite abelian subextension of an abstract fixed number field, this file constructs the genuine restriction from the cyclotomic maximal-unramified Galois group to the finite Galois group. It then identifies the restriction of the chosen-local-factor cyclotomic Artin map with the actual global norm-residue map.

Imports2

Imported by2

instance

cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField

L35 ↗

GlobalClassFieldTheory.Reciprocity.cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField

Documentation

The actual fixed field attached to H is a number field. Keeping this as one file-local instance makes it available while later idele-class binders are elaborated.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory

Lean source · statement

instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

theorem

abstractFixedFieldAbelianizedExtensionQuotientEquivGaloisGroup_of

L56 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldAbelianizedExtensionQuotientEquivGaloisGroup_of

Documentation

The abelianized fixed-field quotient comparison sends the class of an actual finite quotient element to the corresponding automorphism of the concrete relative fixed field.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

Lean source · statement

theorem
    abstractFixedFieldAbelianizedExtensionQuotientEquivGaloisGroup_of
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (q : L.extensionQuotient) :
    abstractFixedFieldAbelianizedExtensionQuotientEquivGaloisGroup H L
        (Additive.ofMul (Abelianization.of q)) =
      Additive.ofMul
        ((L.extensionQuotientMulEquiv.trans
          (LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
            ℚ (SeparableClosure ℚ)
            H.field L.field L.below L.normal)) q)

def

abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom

L98 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom

Documentation

Genuine restriction from the cyclotomic maximal-unramified extension of an abstract fixed field to a finite unramified abelian subextension. The construction uses the canonical quotient presentations of both actual Galois groups.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

Lean source · full declaration

def abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData) :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    let E :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below
    let hI :=
      rationalCyclotomicFieldInertia_le H.field
    let U :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) hI
    Gal(U / F) →* Gal(E / F) := by
  dsimp only
  let qFinite :
      L.toFiniteGaloisExtension.extensionQuotient ≃*
        Gal(
          LocalClassFieldTheory.abstractRelativeFixedField
            ℚ (SeparableClosure ℚ) L.below /
          LocalClassFieldTheory.abstractFixedField
            ℚ (SeparableClosure ℚ) H.field) :=
    L.toFiniteGaloisExtension.extensionQuotientMulEquiv.trans
      (LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
        ℚ (SeparableClosure ℚ)
        H.field L.field L.below L.normal)
  let finiteRestriction :=
    DegreeData.finiteUnramifiedRestriction
      rationalCyclotomicDegreeData
      (H.toFiniteResidueAbstractField rationalCyclotomicDegreeData)
      L.toFiniteGaloisExtension hUnramified
  let degreeEquiv :=
    rationalCyclotomicDegreeData.maximalUnramifiedDegreeEquiv
      (H.toFiniteResidueAbstractField rationalCyclotomicDegreeData)
  let galEquiv := abstractFixedFieldCyclotomicGalEquivZHat H
  exact
    @MonoidHom.comp _ _ _ _ _ _ qFinite.toMonoidHom
      (@MonoidHom.comp _ _ _ _ _ _ finiteRestriction
        (@MonoidHom.comp _ _ _ _ _ _
          degreeEquiv.symm.toMonoidHom galEquiv.toMonoidHom))

theorem

abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom_apply

L145 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom_apply

Documentation

Evaluate the finite cyclotomic restriction through its quotient coordinates.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

Lean source · statement

theorem abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom_apply
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData)
    (σ : Gal(LocalClassFieldTheory.abstractRelativeFixedField
          ℚ (SeparableClosure ℚ)
          (rationalCyclotomicFieldInertia_le H.field)/LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :
    abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom H L hUnramified σ =
      (L.toFiniteGaloisExtension.extensionQuotientMulEquiv.trans
        (LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
          ℚ (SeparableClosure ℚ)
          H.field L.field L.below L.normal))
        (DegreeData.finiteUnramifiedRestriction
          rationalCyclotomicDegreeData
          (H.toFiniteResidueAbstractField rationalCyclotomicDegreeData)
          L.toFiniteGaloisExtension hUnramified
          ((rationalCyclotomicDegreeData.maximalUnramifiedDegreeEquiv
            (H.toFiniteResidueAbstractField
              rationalCyclotomicDegreeData)).symm
            (abstractFixedFieldCyclotomicGalEquivZHat H σ)))

theorem

abstractFixedFieldCyclotomicIdeleClassArtin_fixed_coordinate

L173 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldCyclotomicIdeleClassArtin_fixed_coordinate

Documentation

In the canonical ZHat coordinate, the genuine cyclotomic Artin symbol recovers the abstract maximal-unramified quotient class.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

Lean source · statement

theorem
    abstractFixedFieldCyclotomicIdeleClassArtin_fixed_coordinate
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (a :
      ambientFixedAddSubgroup
        rationalIdeleClassRepresentation H.field) :
    (rationalCyclotomicDegreeData.maximalUnramifiedDegreeEquiv
        (H.toFiniteResidueAbstractField
          rationalCyclotomicDegreeData)).symm
        (abstractFixedFieldCyclotomicGalEquivZHat H
          (abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom H
            (Additive.toMul
              ((rationalAbstractFixedFieldIdeleClassEquivFixed H.field
                (hfinite := H.finite)).symm
                a)))) =
      (ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol
        rationalCyclotomicIdeleClassValuationData H a).toMul

theorem

abstractFixedFieldCyclotomicFiniteRestriction_ideleClassArtin_fixed

L212 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldCyclotomicFiniteRestriction_ideleClassArtin_fixed

Documentation

On a fixed-part idele class, finite restriction of the genuine cyclotomic Artin symbol is the finite restriction of the maximal-unramified norm-residue symbol.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

Lean source · statement

theorem
    abstractFixedFieldCyclotomicFiniteRestriction_ideleClassArtin_fixed
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData)
    (a :
      ambientFixedAddSubgroup
        rationalIdeleClassRepresentation H.field) :
    abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
        H L hUnramified
        (abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom H
          (Additive.toMul
            ((rationalAbstractFixedFieldIdeleClassEquivFixed H.field
              (hfinite := H.finite)).symm
              a))) =
      (L.extensionQuotientMulEquiv.trans
        (LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
          ℚ (SeparableClosure ℚ)
          H.field L.field L.below L.normal))
        (DegreeData.finiteUnramifiedRestriction
          rationalCyclotomicDegreeData
          (H.toFiniteResidueAbstractField
            rationalCyclotomicDegreeData)
          L.toFiniteGaloisExtension hUnramified
          (ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol
            rationalCyclotomicIdeleClassValuationData H a).toMul)

theorem

abstractFixedFieldGlobalNormResidueMonoidHom_fixed_eq_finiteUnramifiedRestriction

L277 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldGlobalNormResidueMonoidHom_fixed_eq_finiteUnramifiedRestriction

Documentation

The actual fixed-field global norm-residue value on a fixed-part class is the finite restriction of the maximal-unramified cyclotomic symbol.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)
open _root_.ClassFormation.ValuationData (
  normResidueSymbol_finiteNormClass_eq_maximalUnramifiedRestriction
) in

Lean source · statement

theorem
    abstractFixedFieldGlobalNormResidueMonoidHom_fixed_eq_finiteUnramifiedRestriction
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData)
    (a :
      ambientFixedAddSubgroup
        rationalIdeleClassRepresentation H.field) :
    abstractFixedFieldGlobalNormResidueMonoidHom H L
        (Additive.toMul
          ((rationalAbstractFixedFieldIdeleClassEquivFixed H.field
            (hfinite := H.finite)).symm
            a)) =
      (L.extensionQuotientMulEquiv.trans
        (LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
          ℚ (SeparableClosure ℚ)
          H.field L.field L.below L.normal))
        (DegreeData.finiteUnramifiedRestriction
          rationalCyclotomicDegreeData
          (H.toFiniteResidueAbstractField
            rationalCyclotomicDegreeData)
          L.toFiniteGaloisExtension hUnramified
          (ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol
            rationalCyclotomicIdeleClassValuationData H a).toMul)

theorem

abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicFiniteRestriction

L350 ↗

GlobalClassFieldTheory.Reciprocity.abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicFiniteRestriction

Documentation

Finite restriction of the genuine cyclotomic chosen-local-factor Artin map is exactly the actual global norm-residue map for every finite unramified abelian fixed-field extension.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
/-- The actual fixed field attached to `H` is a number field.  Keeping
this as one file-local instance makes it available while later idele-class
binders are elaborated. -/
noncomputable local instance
    cyclotomicUnramifiedRestriction_abstractFixedFieldNumberField
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) := by
  let : FiniteDimensional ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field) :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) H.field H.finite
  exact
    NumberField.of_module_finite ℚ
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)

Lean source · statement

theorem
    abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicFiniteRestriction
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData)
    (c :
      IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :
    abstractFixedFieldGlobalNormResidueMonoidHom H L c =
      abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
        H L hUnramified
        (abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom H c)

Module documentation

Finite restriction of cyclotomic fixed-field reciprocity

Declarations