NYLL
Module

TowerRestriction.lean

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

Module documentation

Restriction in a finite-place Artin tower

This module restricts finite-place extensions through an intermediate field and proves restriction naturality for the corresponding global Artin homomorphisms.

Imports1
Imported by3

Declarations

def

restrictFinitePlaceExtension

L38 ↗
GlobalClassFieldTheory.Reciprocity.restrictFinitePlaceExtension
Documentation

Restrict an extension of a finite place through an intermediate field in a scalar tower.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
def restrictFinitePlaceExtension
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) E where
  val :=
    w.1.comp (f := algebraMap E L)
      (algebraMap E L).injective
  property x := by
    change
      w.1 (algebraMap E L (algebraMap K E x)) =
        NumberField.HeightOneSpectrum.adicAbv K v x
    rw [← IsScalarTower.algebraMap_apply K E L]
    exact w.2 x
theorem

absoluteValueCompletionMap_comp_of_isScalarTower

L61 ↗
GlobalClassFieldTheory.Reciprocity.absoluteValueCompletionMap_comp_of_isScalarTower
Documentation

Completion maps compose along a scalar tower when the three absolute values extend one another.

Source context 11 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L]
    [IsAbelianGalois K L] in
Lean source · statement
theorem absoluteValueCompletionMap_comp_of_isScalarTower
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    (vK : AbsoluteValue K ℝ)
    (vE : AbsoluteValue E ℝ)
    (vL : AbsoluteValue L ℝ)
    (hKE : AbsoluteValue.Extends vK vE)
    (hEL : AbsoluteValue.Extends vE vL)
    (hKL : AbsoluteValue.Extends vK vL) :
    (AbsoluteValue.completionMap vE vL hEL).comp
        (AbsoluteValue.completionMap vK vE hKE) =
      AbsoluteValue.completionMap vK vL hKL
def

finitePlaceRestrictedLocalizedCompletionAlgHom

L113 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceRestrictedLocalizedCompletionAlgHom
Documentation

The completion map in a number-field tower restricts to the corresponding algebraic localizations.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
def finitePlaceRestrictedLocalizedCompletionAlgHom
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let wE :=
      restrictFinitePlaceExtension
        (K := K) (L := L) (E := E) v wL
    let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
    let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
    letI : Algebra vK.Completion EL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := E) v wE
    letI : Algebra vK.Completion LL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := L) v wL
    EL →ₐ[vK.Completion] LL := by
  let vK := NumberField.HeightOneSpectrum.adicAbv K v
  let hvK : vK.IsNontrivial :=
    RayClass.adicAbv_isNontrivial v
  let wE :=
    restrictFinitePlaceExtension
      (K := K) (L := L) (E := E) v wL
  letI hEK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) wE.1
  letI : SMul K wE.1.Completion := hEK.toSMul
  letI : Algebra vK.Completion wE.1.Completion :=
    AbsoluteValue.completionAlgebra vK wE.1 wE.2
  letI hLK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) wL.1
  letI : SMul K wL.1.Completion := hLK.toSMul
  letI : Algebra vK.Completion wL.1.Completion :=
    AbsoluteValue.completionAlgebra vK wL.1 wL.2
  let hwEL : AbsoluteValue.Extends wE.1 wL.1 := by
    intro x
    rfl
  letI : Algebra wE.1.Completion wL.1.Completion :=
    AbsoluteValue.completionAlgebra wE.1 wL.1 hwEL
  have hcompletion :
      (AbsoluteValue.completionMap wE.1 wL.1 hwEL).comp
          (AbsoluteValue.completionMap vK wE.1 wE.2) =
        AbsoluteValue.completionMap vK wL.1 wL.2 :=
    absoluteValueCompletionMap_comp_of_isScalarTower
      (K := K) (L := L) (E := E)
      vK wE.1 wL.1 wE.2 hwEL wL.2
  let completionAlgHom :
      wE.1.Completion →ₐ[vK.Completion]
        wL.1.Completion :=
    { __ := AbsoluteValue.completionMap wE.1 wL.1 hwEL
      commutes' := fun x => by
        change
          AbsoluteValue.completionMap wE.1 wL.1 hwEL
              (AbsoluteValue.completionMap
                vK wE.1 wE.2 x) =
            AbsoluteValue.completionMap
              vK wL.1 wL.2 x
        exact DFunLike.congr_fun hcompletion x }
  let EL :=
    AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
  let LL :=
    AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
  let eE :
      EL ≃ₐ[vK.Completion] wE.1.Completion :=
    AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
      vK hvK wE
  let eL :
      LL ≃ₐ[vK.Completion] wL.1.Completion :=
    AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
      vK hvK wL
  let localizationAlgHom :
      EL →ₐ[vK.Completion] LL :=
    eL.symm.toAlgHom.comp
      (completionAlgHom.comp eE.toAlgHom)
  exact localizationAlgHom
theorem

finitePlaceRestrictedLocalizedCompletionAlgHom_toAlgebraicLocalization

L195 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceRestrictedLocalizedCompletionAlgHom_toAlgebraicLocalization
Documentation

The restricted-localization map agrees with the original number-field embedding on the intermediate field.

Source context 11 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [IsAbelianGalois K L] in
Lean source · full declaration
theorem finitePlaceRestrictedLocalizedCompletionAlgHom_toAlgebraicLocalization
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (x : E) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let wE :=
      restrictFinitePlaceExtension
        (K := K) (L := L) (E := E) v wL
    let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
    let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
    letI : Algebra vK.Completion EL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := E) v wE
    letI : Algebra vK.Completion LL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := L) v wL
    finitePlaceRestrictedLocalizedCompletionAlgHom
        (K := K) (L := L) (E := E) v wL
        (AbsoluteValue.toAlgebraicLocalization
          vK wE.1 wE.2 x) =
      AbsoluteValue.toAlgebraicLocalization
        vK wL.1 wL.2 (algebraMap E L x) := by
  let vK := NumberField.HeightOneSpectrum.adicAbv K v
  let hvK : vK.IsNontrivial :=
    RayClass.adicAbv_isNontrivial v
  let wE :=
    restrictFinitePlaceExtension
      (K := K) (L := L) (E := E) v wL
  let hEK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) wE.1
  let : SMul K wE.1.Completion := hEK.toSMul
  let : Algebra vK.Completion wE.1.Completion :=
    AbsoluteValue.completionAlgebra vK wE.1 wE.2
  let hLK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) wL.1
  let : SMul K wL.1.Completion := hLK.toSMul
  let : Algebra vK.Completion wL.1.Completion :=
    AbsoluteValue.completionAlgebra vK wL.1 wL.2
  let hwEL : AbsoluteValue.Extends wE.1 wL.1 := by
    intro z
    rfl
  let : Algebra wE.1.Completion wL.1.Completion :=
    AbsoluteValue.completionAlgebra wE.1 wL.1 hwEL
  let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
  let eL :
      LL ≃ₐ[vK.Completion] wL.1.Completion :=
    AlgebraicNumberTheory.Valuations.localizedCompletionEquivCompletion
      vK hvK wL
  apply eL.injective
  change
    AbsoluteValue.completionMap wE.1 wL.1 hwEL
        (AbsoluteValue.toCompletion wE.1 x) =
      AbsoluteValue.toCompletion wL.1
        (algebraMap E L x)
  rw [AbsoluteValue.toCompletion_eq_algebraMap,
    AbsoluteValue.completionMap_coe]
theorem

decompositionGroupEquivAlgebraicLocalizationAut_restrict_of_commutes

L261 ↗
GlobalClassFieldTheory.Reciprocity.decompositionGroupEquivAlgebraicLocalizationAut_restrict_of_commutes
Documentation

A compatible embedding of algebraic localizations carries restriction of decomposition-group elements to restriction of the corresponding local automorphisms.

Source context 11 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · full declaration
theorem decompositionGroupEquivAlgebraicLocalizationAut_restrict_of_commutes
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (wE : AbsoluteValueExtension vK E)
    (wL : AbsoluteValueExtension vK L) :
    letI hEK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) wE.1
    letI : SMul K wE.1.Completion := hEK.toSMul
    letI : Algebra vK.Completion wE.1.Completion :=
      AbsoluteValue.completionAlgebra vK wE.1 wE.2
    letI hLK :=
      AbsoluteValue.extensionCompletionAlgebra
        (K := K) wL.1
    letI : SMul K wL.1.Completion := hLK.toSMul
    letI : Algebra vK.Completion wL.1.Completion :=
      AbsoluteValue.completionAlgebra vK wL.1 wL.2
    let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
    let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
    ∀ (localizationEmbedding : EL →ₐ[vK.Completion] LL),
      letI hELL : Algebra EL LL :=
        localizationEmbedding.toRingHom.toAlgebra
      letI : SMul EL LL := hELL.toSMul
      letI : IsScalarTower vK.Completion EL LL :=
        IsScalarTower.of_algebraMap_eq' (by
          apply RingHom.ext
          intro x
          exact (localizationEmbedding.commutes x).symm)
      letI : FiniteDimensional vK.Completion EL :=
        AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
          vK hvK wE
      letI : IsAbelianGalois vK.Completion EL :=
        LocalClassFieldTheory.localizedCompletion_isAbelianGalois
          vK hvK wE
      let eDE :
          absoluteValueDecompositionGroup K wE.1 ≃*
            (EL ≃ₐ[vK.Completion] EL) :=
        decompositionGroupEquivAlgebraicLocalizationAut
          vK hvK wE
      let eDL :
          absoluteValueDecompositionGroup K wL.1 ≃*
            (LL ≃ₐ[vK.Completion] LL) :=
        decompositionGroupEquivAlgebraicLocalizationAut
          vK hvK wL
      (∀ z : E,
        localizationEmbedding
            (AbsoluteValue.toAlgebraicLocalization
              vK wE.1 wE.2 z) =
          AbsoluteValue.toAlgebraicLocalization
            vK wL.1 wL.2 (algebraMap E L z)) →
        ∀ tauL : LL ≃ₐ[vK.Completion] LL,
          AlgEquiv.restrictNormalHom E
              ((eDL.symm tauL).1 : L ≃ₐ[K] L) =
            ((eDE.symm
              (AlgEquiv.restrictNormalHom EL tauL)).1 :
                E ≃ₐ[K] E) := by
  let hEK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) wE.1
  let : SMul K wE.1.Completion := hEK.toSMul
  let : Algebra vK.Completion wE.1.Completion :=
    AbsoluteValue.completionAlgebra vK wE.1 wE.2
  let hLK :=
    AbsoluteValue.extensionCompletionAlgebra
      (K := K) wL.1
  let : SMul K wL.1.Completion := hLK.toSMul
  let : Algebra vK.Completion wL.1.Completion :=
    AbsoluteValue.completionAlgebra vK wL.1 wL.2
  let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
  let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
  change
    ∀ localizationEmbedding : EL →ₐ[vK.Completion] LL, _
  intro localizationEmbedding
  let hELL : Algebra EL LL :=
    localizationEmbedding.toRingHom.toAlgebra
  let : SMul EL LL := hELL.toSMul
  let : IsScalarTower vK.Completion EL LL :=
    IsScalarTower.of_algebraMap_eq' (by
      apply RingHom.ext
      intro x
      exact (localizationEmbedding.commutes x).symm)
  let : FiniteDimensional vK.Completion EL :=
    AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
      vK hvK wE
  let : IsAbelianGalois vK.Completion EL :=
    LocalClassFieldTheory.localizedCompletion_isAbelianGalois
      vK hvK wE
  let eDE :
      absoluteValueDecompositionGroup K wE.1 ≃*
        (EL ≃ₐ[vK.Completion] EL) :=
    decompositionGroupEquivAlgebraicLocalizationAut
      vK hvK wE
  let eDL :
      absoluteValueDecompositionGroup K wL.1 ≃*
        (LL ≃ₐ[vK.Completion] LL) :=
    decompositionGroupEquivAlgebraicLocalizationAut
      vK hvK wL
  change
    (∀ z : E,
      localizationEmbedding
          (AbsoluteValue.toAlgebraicLocalization
            vK wE.1 wE.2 z) =
        AbsoluteValue.toAlgebraicLocalization
          vK wL.1 wL.2 (algebraMap E L z)) →
      ∀ tauL : LL ≃ₐ[vK.Completion] LL, _
  intro hlocalization tauL
  let rhoL : absoluteValueDecompositionGroup K wL.1 :=
    eDL.symm tauL
  let tauE := AlgEquiv.restrictNormalHom EL tauL
  let rhoE : absoluteValueDecompositionGroup K wE.1 :=
    eDE.symm tauE
  change
    AlgEquiv.restrictNormalHom E
        (rhoL.1 : L ≃ₐ[K] L) =
      (rhoE.1 : E ≃ₐ[K] E)
  apply AlgEquiv.ext
  intro z
  apply (algebraMap E L).injective
  apply
    (AbsoluteValue.toAlgebraicLocalization
      vK wL.1 wL.2).injective
  let u : EL :=
    AbsoluteValue.toAlgebraicLocalization
      vK wE.1 wE.2 z
  have hcommutes :
      tauL (localizationEmbedding u) =
        localizationEmbedding
          ((AlgEquiv.restrictNormalHom EL tauL) u) := by
    change
      tauL (algebraMap EL LL u) =
        algebraMap EL LL
          ((AlgEquiv.restrictNormalHom EL tauL) u)
    exact
      (AlgEquiv.restrictNormal_commutes
        tauL EL u).symm
  calc
    AbsoluteValue.toAlgebraicLocalization vK wL.1 wL.2
        (algebraMap E L
          ((AlgEquiv.restrictNormalHom E
            (rhoL.1 : L ≃ₐ[K] L)) z)) =
      AbsoluteValue.toAlgebraicLocalization vK wL.1 wL.2
        ((rhoL.1 : L ≃ₐ[K] L)
          (algebraMap E L z)) := by
            exact congrArg
              (AbsoluteValue.toAlgebraicLocalization
                vK wL.1 wL.2)
              (AlgEquiv.restrictNormal_commutes
                (rhoL.1 : L ≃ₐ[K] L) E z)
    _ = eDL rhoL
        (AbsoluteValue.toAlgebraicLocalization
          vK wL.1 wL.2 (algebraMap E L z)) := by
            rw [localizationRamificationGroups_decompositionGroupEquiv_toLocalization]
    _ = tauL
        (AbsoluteValue.toAlgebraicLocalization
          vK wL.1 wL.2 (algebraMap E L z)) := by
            rw [eDL.apply_symm_apply]
    _ = tauL
        (localizationEmbedding
          (AbsoluteValue.toAlgebraicLocalization
            vK wE.1 wE.2 z)) := by
            rw [hlocalization]
    _ = localizationEmbedding
        ((AlgEquiv.restrictNormalHom EL tauL)
          (AbsoluteValue.toAlgebraicLocalization
            vK wE.1 wE.2 z)) := by
            exact hcommutes
    _ = localizationEmbedding
        (tauE
          (AbsoluteValue.toAlgebraicLocalization
            vK wE.1 wE.2 z)) := by
            rfl
    _ = localizationEmbedding
        (eDE rhoE
          (AbsoluteValue.toAlgebraicLocalization
            vK wE.1 wE.2 z)) := by
            rw [eDE.apply_symm_apply]
    _ = localizationEmbedding
        (AbsoluteValue.toAlgebraicLocalization vK wE.1 wE.2
          ((rhoE.1 : E ≃ₐ[K] E) z)) := by
            rw [localizationRamificationGroups_decompositionGroupEquiv_toLocalization]
    _ = AbsoluteValue.toAlgebraicLocalization vK wL.1 wL.2
        (algebraMap E L
          ((rhoE.1 : E ≃ₐ[K] E) z)) := by
            rw [hlocalization]
def

finitePlaceLocalRestrictionMonoidHom

L450 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalRestrictionMonoidHom
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
def finitePlaceLocalRestrictionMonoidHom
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let wE :=
      restrictFinitePlaceExtension
        (K := K) (L := L) (E := E) v wL
    let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
    let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
    letI : Algebra vK.Completion EL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := E) v wE
    letI : Algebra vK.Completion LL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := L) v wL
    (LL ≃ₐ[vK.Completion] LL) →*
      (EL ≃ₐ[vK.Completion] EL) := by
  let vK := NumberField.HeightOneSpectrum.adicAbv K v
  let wE :=
    restrictFinitePlaceExtension
      (K := K) (L := L) (E := E) v wL
  let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
  let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
  letI : Algebra vK.Completion EL :=
    finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := E) v wE
  letI : Algebra vK.Completion LL :=
    finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := L) v wL
  let localizationAlgHom :=
    finitePlaceRestrictedLocalizedCompletionAlgHom
      (K := K) (L := L) (E := E) v wL
  letI hELL : Algebra EL LL :=
    localizationAlgHom.toRingHom.toAlgebra
  letI : SMul EL LL := hELL.toSMul
  letI : IsScalarTower vK.Completion EL LL :=
    IsScalarTower.of_algebraMap_eq' (by
      apply RingHom.ext
      intro x
      exact (localizationAlgHom.commutes x).symm)
  letI : FiniteDimensional vK.Completion EL :=
    finitePlaceLocalArtinFiniteDimensional (K := K) (L := E) v wE
  letI : IsAbelianGalois vK.Completion EL :=
    finitePlaceLocalArtinIsAbelianGalois (K := K) (L := E) v wE
      (inferInstance : FiniteDimensional K E)
  letI hGaloisEL : IsGalois vK.Completion EL :=
    (inferInstance :
      IsAbelianGalois vK.Completion EL).toIsGalois
  letI : Normal vK.Completion EL :=
    hGaloisEL.to_normal
  exact AlgEquiv.restrictNormalHom EL
theorem

finitePlaceDecompositionTransport_restrict_tower_apply

L506 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceDecompositionTransport_restrict_tower_apply
Documentation

Restriction of global decomposition-group elements agrees with restriction of the corresponding automorphisms of algebraic localizations, pointwise on local automorphisms.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem finitePlaceDecompositionTransport_restrict_tower_apply
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let hvK : vK.IsNontrivial :=
      RayClass.adicAbv_isNontrivial v
    let wE :=
      restrictFinitePlaceExtension
        (K := K) (L := L) (E := E) v wL
    let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
    let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
    letI : Algebra vK.Completion EL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := E) v wE
    letI : Algebra vK.Completion LL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := L) v wL
    let localizationAlgHom :=
      finitePlaceRestrictedLocalizedCompletionAlgHom
        (K := K) (L := L) (E := E) v wL
    letI hELL : Algebra EL LL :=
      localizationAlgHom.toRingHom.toAlgebra
    letI : SMul EL LL := hELL.toSMul
    letI : IsScalarTower vK.Completion EL LL :=
      IsScalarTower.of_algebraMap_eq' (by
        apply RingHom.ext
        intro x
        exact (localizationAlgHom.commutes x).symm)
    letI : FiniteDimensional vK.Completion EL :=
      finitePlaceLocalArtinFiniteDimensional (K := K) (L := E) v wE
    letI : IsAbelianGalois vK.Completion EL :=
      finitePlaceLocalArtinIsAbelianGalois (K := K) (L := E) v wE
        (inferInstance : FiniteDimensional K E)
    let eDE :
        absoluteValueDecompositionGroup K wE.1 ≃*
          (EL ≃ₐ[vK.Completion] EL) :=
      decompositionGroupEquivAlgebraicLocalizationAut
        vK hvK wE
    let eDL :
        absoluteValueDecompositionGroup K wL.1 ≃*
          (LL ≃ₐ[vK.Completion] LL) :=
      decompositionGroupEquivAlgebraicLocalizationAut
        vK hvK wL
    ∀ tauL : LL ≃ₐ[vK.Completion] LL,
      AlgEquiv.restrictNormalHom E
          ((eDL.symm tauL).1 : L ≃ₐ[K] L) =
        ((eDE.symm
          (AlgEquiv.restrictNormalHom EL tauL)).1 : E ≃ₐ[K] E) := by
  exact
    decompositionGroupEquivAlgebraicLocalizationAut_restrict_of_commutes
      (K := K) (L := L) (E := E)
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (RayClass.adicAbv_isNontrivial v)
      (restrictFinitePlaceExtension
        (K := K) (L := L) (E := E) v wL)
      wL
      (finitePlaceRestrictedLocalizedCompletionAlgHom
        (K := K) (L := L) (E := E) v wL)
      (fun z =>
        finitePlaceRestrictedLocalizedCompletionAlgHom_toAlgebraicLocalization
          (K := K) (L := L) (E := E) v wL z)
theorem

finitePlaceDecompositionTransport_restrict_tower

L574 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceDecompositionTransport_restrict_tower
Documentation

Restriction of global decomposition-group elements agrees with restriction of the corresponding automorphisms of algebraic localizations.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem finitePlaceDecompositionTransport_restrict_tower
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let hvK : vK.IsNontrivial :=
      RayClass.adicAbv_isNontrivial v
    let wE :=
      restrictFinitePlaceExtension
        (K := K) (L := L) (E := E) v wL
    let EL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wE
    let LL := AlgebraicNumberTheory.Valuations.LocalizedCompletion vK wL
    letI : Algebra vK.Completion EL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := E) v wE
    letI : Algebra vK.Completion LL :=
      finitePlaceLocalArtinLocalizedAlgebra (K := K) (L := L) v wL
    let localizationAlgHom :=
      finitePlaceRestrictedLocalizedCompletionAlgHom
        (K := K) (L := L) (E := E) v wL
    letI hELL : Algebra EL LL :=
      localizationAlgHom.toRingHom.toAlgebra
    letI : SMul EL LL := hELL.toSMul
    letI : IsScalarTower vK.Completion EL LL :=
      IsScalarTower.of_algebraMap_eq' (by
        apply RingHom.ext
        intro x
        exact (localizationAlgHom.commutes x).symm)
    letI : FiniteDimensional vK.Completion EL :=
      finitePlaceLocalArtinFiniteDimensional (K := K) (L := E) v wE
    letI : IsAbelianGalois vK.Completion EL :=
      finitePlaceLocalArtinIsAbelianGalois (K := K) (L := E) v wE
        (inferInstance : FiniteDimensional K E)
    let eDE :
        absoluteValueDecompositionGroup K wE.1 ≃*
          (EL ≃ₐ[vK.Completion] EL) :=
      decompositionGroupEquivAlgebraicLocalizationAut
        vK hvK wE
    let eDL :
        absoluteValueDecompositionGroup K wL.1 ≃*
          (LL ≃ₐ[vK.Completion] LL) :=
      decompositionGroupEquivAlgebraicLocalizationAut
        vK hvK wL
    (AlgEquiv.restrictNormalHom E).comp
        ((absoluteValueDecompositionGroup K wL.1).subtype.comp
          eDL.symm.toMonoidHom) =
      ((absoluteValueDecompositionGroup K wE.1).subtype.comp
          eDE.symm.toMonoidHom).comp
        (AlgEquiv.restrictNormalHom EL) := by
  apply MonoidHom.ext
  intro tauL
  exact
    finitePlaceDecompositionTransport_restrict_tower_apply
      (K := K) (L := L) (E := E) v wL tauL
theorem

finitePlaceLocalArtinMonoidHom_restrict_tower

L634 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinMonoidHom_restrict_tower
Documentation

Local Artin maps on localized completions commute with restriction through an abelian intermediate field.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem finitePlaceLocalArtinMonoidHom_restrict_tower
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    (finitePlaceLocalRestrictionMonoidHom
        (K := K) (L := L) (E := E) v wL).comp
        (finitePlaceLocalArtinMonoidHom
          (K := K) (L := L) v wL) =
      finitePlaceLocalArtinMonoidHom
        (K := K) (L := E) v
        (restrictFinitePlaceExtension
          (K := K) (L := L) (E := E) v wL)
theorem

finitePlaceArtinMonoidHomOfExtension_restrict_tower

L710 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceArtinMonoidHomOfExtension_restrict_tower
Documentation

Finite-place Artin homomorphisms attached to specified place extensions commute with restriction through an abelian tower.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem finitePlaceArtinMonoidHomOfExtension_restrict_tower
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    (AlgEquiv.restrictNormalHom E).comp
        (finitePlaceArtinMonoidHomOfExtension
          (K := K) (L := L) v wL) =
      finitePlaceArtinMonoidHomOfExtension
        (K := K) (L := E) v
        (restrictFinitePlaceExtension
          (K := K) (L := L) (E := E) v wL)
theorem

chosenFinitePlaceArtinMonoidHom_restrict_tower

L787 ↗
GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_restrict_tower
Documentation

Finite local factors commute with restriction in an abelian number-field tower.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem chosenFinitePlaceArtinMonoidHom_restrict_tower
    {E : Type}
    [Field E] [Algebra K E] [Algebra E L]
    [IsScalarTower K E L]
    [FiniteDimensional K E] [IsAbelianGalois K E]
    (v : HeightOneSpectrum (𝓞 K)) :
    (AlgEquiv.restrictNormalHom E).comp
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v) =
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := E) v

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