NYLL
Module

CyclotomicUnramifiedLocalGlobalCompatibility.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.CyclotomicUnramifiedLocalGlobalCompatibility
11 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic unramified local--global compatibility

For an unramified finite abelian subextension of an abstract rational fixed field, the actual global norm-residue homomorphism agrees on every finite one-place idele class with the chosen local Artin homomorphism.

Imports2
Imported by2

Declarations

def

composeMonoidHom

L31 ↗
GlobalClassFieldTheory.Reciprocity.composeMonoidHom
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
def composeMonoidHom
    {M N P : Type*} [MulOne M] [MulOne N] [MulOne P]
    (f : M →* N) (g : N →* P) : M →* P
instance

abstractFixedFieldFiniteIdeleGroupGroup

L49 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldFiniteIdeleGroupGroup
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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
Lean source · statement
instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))
instance

abstractFixedFieldIdeleGroupGroup

L66 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldIdeleGroupGroup
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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
Lean source · statement
instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))
instance

abstractFixedFieldIdeleClassGroupGroup

L77 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldIdeleClassGroupGroup
Source context 9 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
Lean source · statement
instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))
theorem

restrictNormalHom_comp_infiniteGlobalArtinMonoidHom_of_tower

L90 ↗
GlobalClassFieldTheory.Reciprocity.restrictNormalHom_comp_infiniteGlobalArtinMonoidHom_of_tower
Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · statement
theorem
    restrictNormalHom_comp_infiniteGlobalArtinMonoidHom_of_tower
    (K E Ω : Type) [Field K] [NumberField K]
    [Field E] [NumberField E] [Algebra K E]
    [IsAbelianGalois K E]
    [Field Ω] [Algebra K Ω] [Algebra E Ω]
    [IsScalarTower K E Ω] [IsAbelianGalois K Ω] :
    (AlgEquiv.restrictNormalHom E).comp
        (infiniteGlobalArtinMonoidHom K Ω).toMonoidHom =
      globalArtinMonoidHom (K := K) (L := E)
theorem

abstractFixedFieldCyclotomicFiniteRestriction_comp_infiniteGlobalArtinMonoidHom

L143 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldCyclotomicFiniteRestriction_comp_infiniteGlobalArtinMonoidHom
Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · full declaration
theorem
    abstractFixedFieldCyclotomicFiniteRestriction_comp_infiniteGlobalArtinMonoidHom
    (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 U :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (rationalCyclotomicFieldInertia_le H.field)
    letI _ : NumberField F :=
      cyclotomicUnramifiedGeometricBaseNumberField H
    letI _ : NumberField E :=
      cyclotomicUnramifiedGeometricRelativeNumberField H L
    letI _ : Algebra F E := E.algebra'
    letI _ : Algebra F U := U.algebra'
    letI _ : IsAbelianGalois F E :=
      cyclotomicUnramifiedGeometricRelativeIsAbelianGalois H L
    letI _ : IsAbelianGalois F U :=
      cyclotomicUnramifiedGeometricMaximalIsAbelianGalois H
    letI _ : Algebra E U :=
      abstractFixedFieldCyclotomicFiniteUnramifiedInclusionAlgebra
        H L hUnramified
    letI _ : @IsScalarTower F E U
        Algebra.toSMul Algebra.toSMul Algebra.toSMul :=
      IsScalarTower.of_algHom
        (abstractFixedFieldCyclotomicFiniteUnramifiedInclusion
          H L hUnramified)
    (abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
        H L hUnramified).comp
        (infiniteGlobalArtinMonoidHom F U).toMonoidHom =
      globalArtinMonoidHom (K := F) (L := E) := by
  dsimp only
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) H.field
  let E :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below
  let U :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ)
      (rationalCyclotomicFieldInertia_le H.field)
  let fNumberField : NumberField F :=
    cyclotomicUnramifiedGeometricBaseNumberField H
  let eNumberField : NumberField E :=
    cyclotomicUnramifiedGeometricRelativeNumberField H L
  let fEAlgebra : Algebra F E := E.algebra'
  let fUAlgebra : Algebra F U := U.algebra'
  let fEIsAbelianGalois : IsAbelianGalois F E :=
    cyclotomicUnramifiedGeometricRelativeIsAbelianGalois H L
  let fUIsAbelianGalois : IsAbelianGalois F U :=
    cyclotomicUnramifiedGeometricMaximalIsAbelianGalois H
  let eUAlgebra : Algebra E U :=
    abstractFixedFieldCyclotomicFiniteUnramifiedInclusionAlgebra
      H L hUnramified
  let fEUTower : @IsScalarTower F E U
      Algebra.toSMul Algebra.toSMul Algebra.toSMul :=
    IsScalarTower.of_algHom
      (abstractFixedFieldCyclotomicFiniteUnramifiedInclusion
        H L hUnramified)
  calc
    (abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
        H L hUnramified).comp
        (infiniteGlobalArtinMonoidHom F U).toMonoidHom =
      (AlgEquiv.restrictNormalHom E).comp
        (infiniteGlobalArtinMonoidHom F U).toMonoidHom :=
      congrArg
        (fun f => f.comp
          (infiniteGlobalArtinMonoidHom F U).toMonoidHom)
        (abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom_eq_restrictNormalHom
          H L hUnramified)
    _ = globalArtinMonoidHom (K := F) (L := E) :=
      restrictNormalHom_comp_infiniteGlobalArtinMonoidHom_of_tower
        F E U
theorem

abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicRestrictionComp

L227 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicRestrictionComp
Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · full declaration
theorem
    abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicRestrictionComp
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData) :
    let rhs :=
      composeMonoidHom
        (abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom H)
        (abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
          H L hUnramified)
    abstractFixedFieldGlobalNormResidueMonoidHom H L = rhs := by
  dsimp only
  apply MonoidHom.ext
  intro c
  exact
    abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicFiniteRestriction
      H L hUnramified c
theorem

abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom_comp_finitePlaceIdeleClass

L248 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom_comp_finitePlaceIdeleClass
Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · full declaration
theorem
    abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom_comp_finitePlaceIdeleClass
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))) :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    let U :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (rationalCyclotomicFieldInertia_le H.field)
    letI _ : IsAbelianGalois F U :=
      abstractFixedFieldCyclotomic_isAbelianGalois H
    composeMonoidHom
        (IdeleGroup.finitePlaceIdeleClass v)
        (abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom H) =
      composeMonoidHom
        (IdeleGroup.finitePlaceIdele v)
        (infiniteGlobalArtinMonoidHom F U).toMonoidHom := by
  dsimp only
  apply MonoidHom.ext
  intro x
  exact
    abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom_mk
      H (IdeleGroup.finitePlaceIdele v x)
theorem

globalArtinMonoidHom_comp_finitePlaceIdele

L277 ↗
GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_comp_finitePlaceIdele
Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · statement
theorem globalArtinMonoidHom_comp_finitePlaceIdele
    (K E : Type) [Field K] [NumberField K]
    [Field E] [NumberField E] [Algebra K E]
    [IsAbelianGalois K E]
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    (globalArtinMonoidHom (K := K) (L := E)).comp
        (IdeleGroup.finitePlaceIdele v) =
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := E) v
theorem

abstractFixedFieldGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass

L294 ↗
GlobalClassFieldTheory.Reciprocity.abstractFixedFieldGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass
Documentation

The cyclotomic construction of fixed-field reciprocity satisfies finite-place local--global compatibility on every finite unramified abelian subextension.

Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · full declaration
theorem
    abstractFixedFieldGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData)
    (v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))) :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    let E :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below
    (abstractFixedFieldGlobalNormResidueMonoidHom H L).comp
        (IdeleGroup.finitePlaceIdeleClass v) =
      chosenFinitePlaceArtinMonoidHom
        (K := F) (L := E) v := by
  dsimp only
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) H.field
  let E :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) L.below
  let U :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ)
      (rationalCyclotomicFieldInertia_le H.field)
  let fUIsAbelianGalois : IsAbelianGalois F U :=
    abstractFixedFieldCyclotomic_isAbelianGalois H
  let finiteIdele := IdeleGroup.finitePlaceIdele v
  let finiteIdeleClass := IdeleGroup.finitePlaceIdeleClass v
  let restriction :=
    abstractFixedFieldCyclotomicFiniteRestrictionMonoidHom
      H L hUnramified
  let ideleClassArtin :=
    abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom H
  let infiniteArtin := infiniteGlobalArtinMonoidHom F U
  calc
    (abstractFixedFieldGlobalNormResidueMonoidHom H L).comp
          finiteIdeleClass =
        (restriction.comp ideleClassArtin).comp
          finiteIdeleClass :=
      congrArg
        (fun f => f.comp finiteIdeleClass)
        (abstractFixedFieldGlobalNormResidueMonoidHom_eq_cyclotomicRestrictionComp
          H L hUnramified)
    _ = restriction.comp
          (ideleClassArtin.comp finiteIdeleClass) := rfl
    _ = restriction.comp
          (infiniteArtin.toMonoidHom.comp finiteIdele) :=
      congrArg (fun f => restriction.comp f)
        (abstractFixedFieldCyclotomicIdeleClassArtinMonoidHom_comp_finitePlaceIdeleClass
          H v)
    _ = (restriction.comp infiniteArtin.toMonoidHom).comp
          finiteIdele := rfl
    _ = (globalArtinMonoidHom (K := F) (L := E)).comp
          finiteIdele :=
      congrArg (fun f => f.comp finiteIdele)
        (abstractFixedFieldCyclotomicFiniteRestriction_comp_infiniteGlobalArtinMonoidHom
          H L hUnramified)
    _ = chosenFinitePlaceArtinMonoidHom
          (K := F) (L := E) v :=
      globalArtinMonoidHom_comp_finitePlaceIdele F E v
theorem

globalNormResidueMonoidHomOfEmbedding_comp_finitePlaceIdeleClass_of_abstractFixedFieldUnramified

L365 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHomOfEmbedding_comp_finitePlaceIdeleClass_of_abstractFixedFieldUnramified
Documentation

The canonical inclusion realization of a finite unramified abstract fixed-field extension satisfies finite-place local--global compatibility.

Source context 10 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
attribute [local instance]
  rationalSeparableClosureAlgebra
  naturalityAbstractFixedFieldBaseQuotientFinite
  naturalityAbstractFixedFieldRelativeQuotientFinite
  naturalityAbstractFixedFieldFiniteDimensional
  naturalityAbstractRelativeFixedFieldFiniteDimensional
  naturalityAbstractFixedFieldRelativeScalarTower
  naturalityAbstractRelativeFixedFieldAbsoluteFiniteDimensional
  naturalityAbstractFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldNumberField
  naturalityAbstractRelativeFixedFieldIsAbelianGalois
@[reducible]
noncomputable local instance
    abstractFixedFieldFiniteIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (FiniteIdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  RestrictedProduct.instGroupCoeOfSubgroupClass
    (fun v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field)) =>
      (v.adicCompletion
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field))ˣ)
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  Prod.instGroup
@[reducible]
noncomputable local instance
    abstractFixedFieldIdeleClassGroupGroup
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Group
      (IdeleClassGroup
        (LocalClassFieldTheory.abstractFixedField
          ℚ (SeparableClosure ℚ) H.field)) :=
  QuotientGroup.Quotient.group
    (IdeleGroup.principalSubgroup
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))
Lean source · full declaration
theorem
    globalNormResidueMonoidHomOfEmbedding_comp_finitePlaceIdeleClass_of_abstractFixedFieldUnramified
    (H : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension H.field)
    (hUnramified :
      L.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData)
    (v : IsDedekindDomain.HeightOneSpectrum
      (𝓞 (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field))) :
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) H.field
    let E :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below
    let j : E →ₐ[ℚ] SeparableClosure ℚ :=
      E.val.restrictScalars ℚ
    (globalNormResidueMonoidHomOfEmbedding F E j).comp
        (IdeleGroup.finitePlaceIdeleClass v) =
      chosenFinitePlaceArtinMonoidHom
        (K := F) (L := E) v := by
  dsimp only
  rw [
    globalNormResidueMonoidHomOfEmbedding_abstractFixedFieldInclusion
      H L]
  exact
    abstractFixedFieldGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass
      H L hUnramified v

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