Module

TowerAlgEquivNaturality.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.TowerAlgEquivNaturality

10 declarations indexed from sourceView source ↗

Module documentation

Naturality of tower base change under number-field equivalences

The ordinary idele group of a finite extension is obtained from the relative tensor presentation by scalar extension. This file proves that this comparison is natural when both fields in the extension are replaced by compatible equivalent number fields. The proof passes through the fixed-bottom tower

(𝔸_ℚ ⊗[ℚ] K) ⊗[K] L

and therefore uses only tensor-product coherence; no new description of local components is introduced.

Imports2

Imported by9

theorem

relativeAdeleCongr_trans

L50 ↗

Documentation

Relative adelic transport over ℚ is functorial in the transported top field.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
section CongrComposition
variable
    {M N : Type}
    [Field M] [NumberField M]
    [Field N] [NumberField N]

Lean source · statement

theorem relativeAdeleCongr_trans
    (e : K ≃ₐ[ℚ] M)
    (f : M ≃ₐ[ℚ] N)
    (z : RelativeAdeleRing ℚ K) :
    relativeAdeleCongr (K := ℚ) f
        (relativeAdeleCongr (K := ℚ) e z) =
      relativeAdeleCongr (K := ℚ) (e.trans f) z

theorem

adeleCongr_trans

L67 ↗

Documentation

Canonical transport of ordinary adele rings is functorial.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
section CongrComposition
variable
    {M N : Type}
    [Field M] [NumberField M]
    [Field N] [NumberField N]

Lean source · statement

theorem adeleCongr_trans
    (e : K ≃ₐ[ℚ] M)
    (f : M ≃ₐ[ℚ] N)
    (a : NumberField.AdeleRing (𝓞 K) K) :
    adeleCongr f (adeleCongr e a) =
      adeleCongr (e.trans f) a

theorem

ideleCongr_trans

L93 ↗

Documentation

Canonical transport of ordinary ideles is functorial.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
section CongrComposition
variable
    {M N : Type}
    [Field M] [NumberField M]
    [Field N] [NumberField N]

Lean source · statement

theorem ideleCongr_trans
    (e : K ≃ₐ[ℚ] M)
    (f : M ≃ₐ[ℚ] N)
    (a : IdeleGroup K) :
    ideleCongr f (ideleCongr e a) =
      ideleCongr (e.trans f) a

theorem

ideleClassCongr_trans

L112 ↗

Documentation

Canonical transport of ordinary idele classes is functorial.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
section CongrComposition
variable
    {M N : Type}
    [Field M] [NumberField M]
    [Field N] [NumberField N]

Lean source · statement

theorem ideleClassCongr_trans
    (e : K ≃ₐ[ℚ] M)
    (f : M ≃ₐ[ℚ] N)
    (c : IdeleClassGroup K) :
    ideleClassCongr f (ideleClassCongr e c) =
      ideleClassCongr (e.trans f) c

theorem

ideleClassCongr_refl

L128 ↗

Documentation

Transport of ordinary idele classes along the identity number-field equivalence is the identity.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
section CongrComposition
variable
    {M N : Type}
    [Field M] [NumberField M]
    [Field N] [NumberField N]

Lean source · statement

theorem ideleClassCongr_refl
    (c : IdeleClassGroup K) :
    ideleClassCongr
        (AlgEquiv.refl : K ≃ₐ[ℚ] K) c =
      c

theorem

relativeAdeleCongrOfAlgEquiv_towerActual

L201 ↗

Documentation

Before passing to ordinary adeles, compatible transport of a tower agrees with transporting its flattened rational tensor presentation.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']
omit [FiniteDimensional K L] [FiniteDimensional K' L'] in

Lean source · statement

theorem relativeAdeleCongrOfAlgEquiv_towerActual
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (z : TowerRelativeAdeleRing ℚ K L) :
    relativeAdeleCongrOfAlgEquiv eK eL h
        (towerActualRelativeAdeleRingEquiv ℚ K L z) =
      towerActualRelativeAdeleRingEquiv ℚ K' L'
        (towerRelativeAdeleUnflatten ℚ K' L'
          (relativeAdeleCongr (K := ℚ) eL
            (towerRelativeAdeleFlatten ℚ K L z)))

theorem

relativeAdeleBaseChangeRingEquiv_congrOfAlgEquiv

L282 ↗

Documentation

The relative-to-ordinary adele comparison commutes with compatible equivalences of both fields in a finite extension.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']

Lean source · statement

theorem relativeAdeleBaseChangeRingEquiv_congrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (z : RelativeAdeleRing K L) :
    relativeAdeleBaseChangeRingEquiv
        (K := K') (L := L')
        (relativeAdeleCongrOfAlgEquiv eK eL h z) =
      adeleCongr eL
        (relativeAdeleBaseChangeRingEquiv
          (K := K) (L := L) z)

theorem

relativeIdeleBaseChangeMulEquiv_congrOfAlgEquiv

L363 ↗

Documentation

The relative-to-ordinary idele comparison commutes with compatible equivalences of both fields in a finite extension.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']

Lean source · statement

theorem relativeIdeleBaseChangeMulEquiv_congrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (a : RelativeIdeleGroup K L) :
    relativeIdeleBaseChangeMulEquiv
        (K := K') (L := L')
        (relativeIdeleCongrOfAlgEquiv eK eL h a) =
      ideleCongr eL
        (relativeIdeleBaseChangeMulEquiv
          (K := K) (L := L) a)

theorem

relativeIdeleClassBaseChangeMulEquiv_congrOfAlgEquiv

L391 ↗

Documentation

The relative-to-ordinary idele-class comparison commutes with compatible equivalences of both fields in a finite extension.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']

Lean source · statement

theorem relativeIdeleClassBaseChangeMulEquiv_congrOfAlgEquiv
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (c : RelativeIdeleGroup.ClassGroup K L) :
    relativeIdeleClassBaseChangeMulEquiv
        (K := K') (L := L')
        (relativeIdeleClassCongrOfAlgEquiv eK eL h c) =
      ideleClassCongr eL
        (relativeIdeleClassBaseChangeMulEquiv
          (K := K) (L := L) c)

theorem

ideleClassCongr_ideleClassNorm

L415 ↗

Documentation

Ordinary idele-class norms are natural under compatible equivalences of finite number-field extensions.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    {K K' L L' : Type}
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L] [Algebra K L]
    [Field L'] [NumberField L'] [Algebra K' L']
    [FiniteDimensional K L]
    [FiniteDimensional K' L']

Lean source · statement

theorem ideleClassCongr_ideleClassNorm
    (eK : K ≃ₐ[ℚ] K')
    (eL : L ≃ₐ[ℚ] L')
    (h : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (c : IdeleClassGroup L) :
    ideleClassCongr eK (_root_.ideleClassNorm K L c) =
      _root_.ideleClassNorm K' L' (ideleClassCongr eL c)

Module documentation

Naturality of tower base change under number-field equivalences

Declarations