NYLL
Module

SmallHilbertClassFieldNaturality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldNaturality
9 declarations indexed from sourceView source ↗

Module documentation

Naturality of the small Hilbert class field

An equivalence of number fields carries the small-Hilbert norm subgroup exactly onto the small-Hilbert norm subgroup. Consequently it induces the canonical equivalence of the corresponding reciprocity quotients. Transport of ordinary ideal classes is obtained from this quotient equivalence and is therefore compatible with the canonical quotient--class-group equivalences.

Imports2
Imported by3

Declarations

theorem

smallHilbertNaturalityIdeleClassIsMulCommutative

L32 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertNaturalityIdeleClassIsMulCommutative
Documentation

Supply the canonical commutativity used by both small-Hilbert quotients.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
Lean source · statement
theorem smallHilbertNaturalityIdeleClassIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

smallHilbertClassFieldNormSubgroup_map_ideleClassCongr

L47 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup_map_ideleClassCongr
Documentation

Transport of ordinary idele classes along an equivalence of number fields carries the small-Hilbert norm subgroup exactly onto the small-Hilbert norm subgroup of the target.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem smallHilbertClassFieldNormSubgroup_map_ideleClassCongr
    (e : K ≃ₐ[ℚ] M) :
    (smallHilbertClassFieldNormSubgroup (K := K)).map
        (ideleClassCongr e).toMonoidHom =
      smallHilbertClassFieldNormSubgroup (K := M)
def

smallHilbertClassFieldQuotientCongr

L58 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientCongr
Documentation

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

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
def smallHilbertClassFieldQuotientCongr
    (e : K ≃ₐ[ℚ] M) :
    (IdeleClassGroup K ⧸
        smallHilbertClassFieldNormSubgroup (K := K)) ≃*
      (IdeleClassGroup M ⧸
        smallHilbertClassFieldNormSubgroup (K := M))
theorem

smallHilbertClassFieldQuotientCongr_mk

L73 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientCongr_mk
Documentation

On representatives, the small-Hilbert quotient transport is induced by the existing transport of ordinary idele classes.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem smallHilbertClassFieldQuotientCongr_mk
    (e : K ≃ₐ[ℚ] M)
    (c : IdeleClassGroup K) :
    smallHilbertClassFieldQuotientCongr e
        (QuotientGroup.mk'
          (smallHilbertClassFieldNormSubgroup (K := K)) c) =
      QuotientGroup.mk'
        (smallHilbertClassFieldNormSubgroup (K := M))
        (ideleClassCongr e c)
def

smallHilbertClassGroupCongr

L86 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassGroupCongr
Documentation

The canonical transport of ordinary ideal classes determined by the small-Hilbert reciprocity quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
def smallHilbertClassGroupCongr
    (e : K ≃ₐ[ℚ] M) :
    ClassGroup (𝓞 K) ≃* ClassGroup (𝓞 M)
theorem

smallHilbertClassFieldQuotientEquivClassGroup_naturality

L98 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup_naturality
Documentation

Naturality of the canonical identification of the small-Hilbert reciprocity quotient with the ordinary ideal class group.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem smallHilbertClassFieldQuotientEquivClassGroup_naturality
    (e : K ≃ₐ[ℚ] M)
    (q : IdeleClassGroup K ⧸
      smallHilbertClassFieldNormSubgroup (K := K)) :
    smallHilbertClassFieldQuotientEquivClassGroup
        (K := M)
        (smallHilbertClassFieldQuotientCongr e q) =
      smallHilbertClassGroupCongr e
        (smallHilbertClassFieldQuotientEquivClassGroup
          (K := K) q)
theorem

smallHilbertClassFieldQuotientEquivClassGroup_naturality_hom

L112 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup_naturality_hom
Documentation

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

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem smallHilbertClassFieldQuotientEquivClassGroup_naturality_hom
    (e : K ≃ₐ[ℚ] M) :
    (smallHilbertClassFieldQuotientEquivClassGroup
        (K := M)).toMonoidHom.comp
        (smallHilbertClassFieldQuotientCongr
          (K := K) (M := M) e).toMonoidHom =
      (smallHilbertClassGroupCongr
        (K := K) (M := M) e).toMonoidHom.comp
        (smallHilbertClassFieldQuotientEquivClassGroup
          (K := K)).toMonoidHom
theorem

smallHilbertClassGroupCongr_idealClass

L132 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassGroupCongr_idealClass
Documentation

On an idele representative, the induced transport of ordinary ideal classes is the ideal class of the transported idele. Thus the class-group transport above is characterized by the actual idelic transport, rather than by a choice of representatives in the quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem smallHilbertClassGroupCongr_idealClass
    (e : K ≃ₐ[ℚ] M)
    (a : IdeleGroup K) :
    smallHilbertClassGroupCongr e
        (IdeleGroup.idealClass a) =
      IdeleGroup.idealClass (ideleCongr e a)
theorem

smallHilbertClassGroupCongr_naturality

L166 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassGroupCongr_naturality
Documentation

Homomorphism form of naturality for ordinary ideal classes under the small-Hilbert class-group transport.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] smallHilbertNaturalityIdeleClassIsMulCommutative
variable
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
Lean source · statement
theorem smallHilbertClassGroupCongr_naturality
    (e : K ≃ₐ[ℚ] M) :
    (smallHilbertClassGroupCongr e).toMonoidHom.comp
        (IdeleGroup.idealClass (K := K)) =
      (IdeleGroup.idealClass (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.