NYLL
Module

BigHilbertClassFieldNaturality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassFieldNaturality
20 declarations indexed from sourceView source ↗

Module documentation

Naturality of the big Hilbert class field

An equivalence of number fields preserves both finite integrality and positivity at the real infinite places. Consequently the actual idele-class transport carries the big-Hilbert norm subgroup exactly onto the corresponding subgroup of the target field. This gives canonical transport on the big-Hilbert reciprocity quotient and on the narrow class group, with formulas on genuine idele representatives.

Imports2
Imported by2

Declarations

theorem

bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk

L37 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk
    (a : IdeleGroup K) :
    bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K))
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      QuotientGroup.mk'
        (RayClass.narrowDenominator (K := K)) a
def

infinitePlaceCompletionCongrHom

L49 ↗
GlobalClassFieldTheory.GlobalClassFields.infinitePlaceCompletionCongrHom
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
def infinitePlaceCompletionCongrHom
    (e : K ≃ₐ[ℚ] M)
    (W : InfinitePlace M) :
    (W.comap e.toRingHom).Completion →+*
      W.Completion
theorem

infinitePlaceCompletionCongrHom_algebraMap

L64 ↗
GlobalClassFieldTheory.GlobalClassFields.infinitePlaceCompletionCongrHom_algebraMap
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem infinitePlaceCompletionCongrHom_algebraMap
    (e : K ≃ₐ[ℚ] M)
    (W : InfinitePlace M)
    (x : K) :
    infinitePlaceCompletionCongrHom e W
        (algebraMap K (W.comap e.toRingHom).Completion x) =
      algebraMap M W.Completion (e x)
theorem

relativeAdeleBaseChangeRingEquiv_relativeAdeleCongr_infiniteComponent_tmul

L99 ↗
GlobalClassFieldTheory.GlobalClassFields.relativeAdeleBaseChangeRingEquiv_relativeAdeleCongr_infiniteComponent_tmul
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem
    relativeAdeleBaseChangeRingEquiv_relativeAdeleCongr_infiniteComponent_tmul
    (e : K ≃ₐ[ℚ] M)
    (b : NumberField.AdeleRing (𝓞 ℚ) ℚ)
    (x : K)
    (W : InfinitePlace M) :
    (relativeAdeleBaseChangeRingEquiv
        (K := ℚ) (L := M) (b ⊗ₜ[ℚ] e x)).1 W =
      infinitePlaceCompletionCongrHom e W
        ((relativeAdeleBaseChangeRingEquiv
          (K := ℚ) (L := K) (b ⊗ₜ[ℚ] x)).1
            (W.comap e.toRingHom))
theorem

adeleCongr_infiniteComponent

L179 ↗
GlobalClassFieldTheory.GlobalClassFields.adeleCongr_infiniteComponent
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem adeleCongr_infiniteComponent
    (e : K ≃ₐ[ℚ] M)
    (a : NumberField.AdeleRing (𝓞 K) K)
    (W : InfinitePlace M) :
    (adeleCongr e a).1 W =
      infinitePlaceCompletionCongrHom e W
        (a.1 (W.comap e.toRingHom))
theorem

ideleCongr_infiniteComponent

L224 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleCongr_infiniteComponent
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem ideleCongr_infiniteComponent
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K)
    (W : InfinitePlace M) :
    IdeleGroup.infiniteComponent W (ideleCongr e a) =
      Units.map
        (infinitePlaceCompletionCongrHom e W).toMonoidHom
        (IdeleGroup.infiniteComponent
          (W.comap e.toRingHom) a)
theorem

infinitePlaceCompletionCongrHom_extensionEmbeddingOfIsReal

L241 ↗
GlobalClassFieldTheory.GlobalClassFields.infinitePlaceCompletionCongrHom_extensionEmbeddingOfIsReal
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem
    infinitePlaceCompletionCongrHom_extensionEmbeddingOfIsReal
    (e : K ≃ₐ[ℚ] M)
    (W : InfinitePlace M)
    (hW : W.IsReal)
    (x : (W.comap e.toRingHom).Completion) :
    InfinitePlace.Completion.extensionEmbeddingOfIsReal hW
        (infinitePlaceCompletionCongrHom e W x) =
      InfinitePlace.Completion.extensionEmbeddingOfIsReal
        (hW.comap e.toRingHom) x
theorem

infinitePlaceCompletionCongrHom_mem_infinitePositiveSubgroup_iff

L276 ↗
GlobalClassFieldTheory.GlobalClassFields.infinitePlaceCompletionCongrHom_mem_infinitePositiveSubgroup_iff
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem
    infinitePlaceCompletionCongrHom_mem_infinitePositiveSubgroup_iff
    (e : K ≃ₐ[ℚ] M)
    (W : InfinitePlace M)
    (x : (W.comap e.toRingHom).Completionˣ) :
    Units.map
          (infinitePlaceCompletionCongrHom e W).toMonoidHom x ∈
        RayClass.infinitePositiveSubgroup W ↔
      x ∈
        RayClass.infinitePositiveSubgroup
          (W.comap e.toRingHom)
theorem

ideleCongr_mem_infiniteCongruenceSubgroup_iff

L322 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleCongr_mem_infiniteCongruenceSubgroup_iff
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem ideleCongr_mem_infiniteCongruenceSubgroup_iff
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K) :
    (ideleCongr e a).1 ∈
        RayClass.narrowInfiniteCongruenceSubgroup (K := M) ↔
      a.1 ∈
        RayClass.narrowInfiniteCongruenceSubgroup (K := K)
theorem

ideleCongr_mem_ideleCongruenceSubgroup_zero_iff

L370 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleCongr_mem_ideleCongruenceSubgroup_zero_iff
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem ideleCongr_mem_ideleCongruenceSubgroup_zero_iff
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K) :
    ideleCongr e a ∈
        (RayClass.Modulus.narrowOfFinite
          (0 : RayClass.FiniteModulus M)).ideleCongruenceSubgroup ↔
      a ∈
        (RayClass.Modulus.narrowOfFinite
          (0 : RayClass.FiniteModulus K)).ideleCongruenceSubgroup
theorem

ideleCongruenceSubgroup_zero_map_ideleCongr

L402 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleCongruenceSubgroup_zero_map_ideleCongr
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem ideleCongruenceSubgroup_zero_map_ideleCongr
    (e : K ≃ₐ[ℚ] M) :
    ((RayClass.Modulus.narrowOfFinite
        (0 : RayClass.FiniteModulus K)).ideleCongruenceSubgroup).map
          (ideleCongr e).toMonoidHom =
      (RayClass.Modulus.narrowOfFinite
        (0 : RayClass.FiniteModulus M)).ideleCongruenceSubgroup
theorem

narrowDenominator_map_ideleCongr

L426 ↗
GlobalClassFieldTheory.GlobalClassFields.narrowDenominator_map_ideleCongr
Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem narrowDenominator_map_ideleCongr
    (e : K ≃ₐ[ℚ] M) :
    (RayClass.narrowDenominator (K := K)).map
        (ideleCongr e).toMonoidHom =
      RayClass.narrowDenominator (K := M)
theorem

bigHilbertClassFieldNormSubgroup_map_ideleClassCongr

L448 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_map_ideleClassCongr
Documentation

Transport of actual idele classes along a number-field equivalence carries the big-Hilbert norm subgroup exactly onto the big-Hilbert norm subgroup of the target field.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem bigHilbertClassFieldNormSubgroup_map_ideleClassCongr
    (e : K ≃ₐ[ℚ] M) :
    (bigHilbertClassFieldNormSubgroup (K := K)).map
        (ideleClassCongr e).toMonoidHom =
      bigHilbertClassFieldNormSubgroup (K := M)
def

bigHilbertClassFieldQuotientCongr

L481 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientCongr
Documentation

The canonical equivalence of big-Hilbert reciprocity quotients induced by an equivalence of number fields.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
def bigHilbertClassFieldQuotientCongr
    (e : K ≃ₐ[ℚ] M) :
    (IdeleClassGroup K ⧸
        bigHilbertClassFieldNormSubgroup (K := K)) ≃*
      (IdeleClassGroup M ⧸
        bigHilbertClassFieldNormSubgroup (K := M))
theorem

bigHilbertClassFieldQuotientCongr_mk

L496 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientCongr_mk
Documentation

The big-Hilbert quotient equivalence is induced on representatives by the actual transport of idele classes.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem bigHilbertClassFieldQuotientCongr_mk
    (e : K ≃ₐ[ℚ] M)
    (c : IdeleClassGroup K) :
    bigHilbertClassFieldQuotientCongr e
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)) c) =
      QuotientGroup.mk'
        (bigHilbertClassFieldNormSubgroup (K := M))
        (ideleClassCongr e c)
def

bigHilbertNarrowClassGroupCongr

L509 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNarrowClassGroupCongr
Documentation

Canonical transport of narrow ideal classes determined by the big-Hilbert reciprocity quotient.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
def bigHilbertNarrowClassGroupCongr
    (e : K ≃ₐ[ℚ] M) :
    RayClass.NarrowClassGroup K ≃*
      RayClass.NarrowClassGroup M
theorem

bigHilbertClassFieldQuotientEquivNarrowClassGroup_naturality

L522 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientEquivNarrowClassGroup_naturality
Documentation

Naturality of the canonical identification of the big-Hilbert reciprocity quotient with the narrow class group.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem bigHilbertClassFieldQuotientEquivNarrowClassGroup_naturality
    (e : K ≃ₐ[ℚ] M)
    (q : IdeleClassGroup K ⧸
      bigHilbertClassFieldNormSubgroup (K := K)) :
    bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := M)
        (bigHilbertClassFieldQuotientCongr e q) =
      bigHilbertNarrowClassGroupCongr e
        (bigHilbertClassFieldQuotientEquivNarrowClassGroup
          (K := K) q)
theorem

bigHilbertClassFieldQuotientEquivNarrowClassGroup_naturality_hom

L537 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientEquivNarrowClassGroup_naturality_hom
Documentation

Homomorphism form of naturality for the big-Hilbert quotient--narrow-class-group identification.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem
    bigHilbertClassFieldQuotientEquivNarrowClassGroup_naturality_hom
    (e : K ≃ₐ[ℚ] M) :
    (bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := M)).toMonoidHom.comp
        (bigHilbertClassFieldQuotientCongr
          (K := K) (M := M) e).toMonoidHom =
      (bigHilbertNarrowClassGroupCongr
        (K := K) (M := M) e).toMonoidHom.comp
        (bigHilbertClassFieldQuotientEquivNarrowClassGroup
          (K := K)).toMonoidHom
theorem

bigHilbertNarrowClassGroupCongr_mk

L556 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNarrowClassGroupCongr_mk
Documentation

On an idele representative, canonical transport of narrow ideal classes is represented by the transported idele itself.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem bigHilbertNarrowClassGroupCongr_mk
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K) :
    bigHilbertNarrowClassGroupCongr e
        (QuotientGroup.mk'
          (RayClass.narrowDenominator (K := K)) a) =
      QuotientGroup.mk'
        (RayClass.narrowDenominator (K := M))
        (ideleCongr e a)
theorem

bigHilbertNarrowClassGroupCongr_naturality

L597 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertNarrowClassGroupCongr_naturality
Documentation

Homomorphism form of naturality for narrow ideal classes under the big-Hilbert narrow-class-group transport.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver TensorProduct
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem bigHilbertNarrowClassGroupCongr_naturality
    (e : K ≃ₐ[ℚ] M) :
    (bigHilbertNarrowClassGroupCongr e).toMonoidHom.comp
        (QuotientGroup.mk'
          (RayClass.narrowDenominator (K := K))) =
      (QuotientGroup.mk'
        (RayClass.narrowDenominator (K := M))).comp
          (ideleCongr e).toMonoidHom

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