Module

RayClassFieldRealization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassFieldRealization

43 declarations indexed from sourceView source ↗

Module documentation

Actual ray class fields

For a modulus m of a number field K, its ray congruence subgroup C_K^m is closed and has finite index. The finite-index class-field construction therefore selects an actual finite abelian extension whose determinant-norm range is exactly C_K^m.

The construction first occurs over the canonical fixed-field copy of K inside the rational separable closure. We then install the canonical scalar structure from the original field, identify the norm range over that original field, and obtain the genuine reciprocity equivalence

Gal(K^m / K) ≃ C_K / C_K^m.

Imports16

Imported by8

abbrev

rayClassFieldNormAmbient

L59 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldNormAmbient

Documentation

The concrete finite Galois norm neighbourhood used to select the ray class field attached to m.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldNormAmbient
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) : Type

abbrev

rayClassFieldBaseSubgroup

L68 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldBaseSubgroup

Documentation

The compatible abstract base subgroup used by the selected ray class-field realization.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldBaseSubgroup
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K)

abbrev

rayClassFieldSubextension

L77 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldSubextension

Documentation

The finite abelian subextension selected by the ray congruence subgroup C_K^m.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldSubextension
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) :
    FiniteAbelianSubextension
      (rayClassFieldBaseSubgroup K m)

abbrev

rayClassFieldBase

L88 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldBase

Documentation

The canonical fixed-field copy of the original number field in the selected ray class-field realization.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldBase
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) : Type

abbrev

rayClassField

L98 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField

Documentation

A chosen finite ray-class-field realization attached to m, selected inside the rational separable closure. Its intrinsic realization in the fixed separable closure of K is rayClassFieldSubfield.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassField
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) : Type

abbrev

rayClassFieldBaseEquiv

L107 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldBaseEquiv

Documentation

The canonical equivalence from K to the fixed-field base of its selected ray class field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldBaseEquiv
    (m : RayClass.Modulus K) :
    K ≃ₐ[ℚ] rayClassFieldBase K m

def

rayClassFieldTransportedCongruenceSubgroup

L116 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldTransportedCongruenceSubgroup

Documentation

The ray congruence subgroup transported to the fixed-field base of the selected realization.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassFieldTransportedCongruenceSubgroup
    (m : RayClass.Modulus K) :
    Subgroup
      (IdeleClassGroup (rayClassFieldBase K m))

theorem

rayClassField_ideleClassNorm_range

L126 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField_ideleClassNorm_range

Documentation

The determinant-norm range over the fixed-field base of the selected ray class field is the transported ray congruence subgroup.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassField_ideleClassNorm_range
    (m : RayClass.Modulus K) :
    (_root_.ideleClassNorm
      (rayClassFieldBase K m)
      (rayClassField K m)).range =
      rayClassFieldTransportedCongruenceSubgroup
        (K := K) m

abbrev

rayClassFieldBaseAlgebraOverOriginal

L141 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldBaseAlgebraOverOriginal

Documentation

The fixed-field base of the selected ray class field, regarded as an algebra over the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldBaseAlgebraOverOriginal
    (m : RayClass.Modulus K) :
    Algebra K (rayClassFieldBase K m)

abbrev

rayClassFieldBaseEquivOverOriginal

L150 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldBaseEquivOverOriginal

Documentation

The canonical fixed-field identification as an equivalence over the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldBaseEquivOverOriginal
    (m : RayClass.Modulus K) :
    K ≃ₐ[K] rayClassFieldBase K m

abbrev

rayClassFieldAlgebraOverOriginal

L159 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldAlgebraOverOriginal

Documentation

The selected ray class field as an algebra over the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldAlgebraOverOriginal
    (m : RayClass.Modulus K) :
    Algebra K (rayClassField K m)

theorem

rayClassField_algebraMap_original

L169 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField_algebraMap_original

Documentation

The scalar map into the ray class field is the canonical base equivalence followed by fixed-field inclusion.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassField_algebraMap_original
    (m : RayClass.Modulus K) (x : K) :
    algebraMap K (rayClassField K m) x =
      algebraMap
        (rayClassFieldBase K m)
        (rayClassField K m)
        (rayClassFieldBaseEquiv (K := K) m x)

def

rayClassFieldEmbedding

L184 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldEmbedding

Documentation

A chosen embedding of the finite ray-class-field realization into the fixed separable closure of its original base field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassFieldEmbedding
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) :
    rayClassField K m →ₐ[K] SeparableClosure K

def

rayClassFieldSubfield

L192 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldSubfield

Documentation

The intrinsic ray class field as an intermediate field of the fixed separable closure of K.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassFieldSubfield
    (K : Type) [Field K] [NumberField K]
    (m : RayClass.Modulus K) :
    IntermediateField K (SeparableClosure K)

theorem

rayClassFieldSubfield_eq_fieldRange

L200 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldSubfield_eq_fieldRange

Documentation

Every embedding of the chosen finite ray-class-field realization into the fixed separable closure has the intrinsic ray-class-field range.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassFieldSubfield_eq_fieldRange
    (m : RayClass.Modulus K)
    (f : rayClassField K m →ₐ[K] SeparableClosure K) :
    rayClassFieldSubfield K m = f.fieldRange

theorem

rayClassField_ideleClassNorm_range_over_original

L209 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField_ideleClassNorm_range_over_original

Documentation

Over the original number field, the determinant-norm range of the selected ray class field is exactly C_K^m.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassField_ideleClassNorm_range_over_original
    (m : RayClass.Modulus K) :
    (_root_.ideleClassNorm K (rayClassField K m)).range =
      RayClass.Modulus.congruenceSubgroup m

theorem

nonempty_algEquiv_rayClassField_iff_ideleClassNorm_range_eq

L222 ↗

GlobalClassFieldTheory.GlobalClassFields.nonempty_algEquiv_rayClassField_iff_ideleClassNorm_range_eq

Documentation

A finite abelian extension is isomorphic over K to the selected ray class field of modulus m exactly when its genuine idèle-class norm range is C_K^m. This is the actual-field uniqueness statement for ray class fields.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    nonempty_algEquiv_rayClassField_iff_ideleClassNorm_range_eq
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L]
    (m : RayClass.Modulus K) :
    Nonempty (L ≃ₐ[K] rayClassField K m) ↔
      (_root_.ideleClassNorm K L).range =
        RayClass.Modulus.congruenceSubgroup m

theorem

rayClassField_ideleClassNorm_range_antitone

L238 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField_ideleClassNorm_range_antitone

Documentation

Increasing the modulus decreases the actual determinant-norm range of the selected ray class field. This is the norm-subgroup form of the contravariant inclusion of ray class fields.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassField_ideleClassNorm_range_antitone
    {m n : RayClass.Modulus K}
    (hmn : m ≤ n) :
    (_root_.ideleClassNorm K (rayClassField K n)).range ≤
      (_root_.ideleClassNorm K (rayClassField K m)).range

theorem

rayClassField_nonempty_algHom_of_le

L259 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField_nonempty_algHom_of_le

Documentation

Divisibility of moduli produces an embedding between the selected ray-class-field types over the original number field. Literal containment inside the fixed separable closure is instead stated by rayClassFieldSubfield_mono.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassField_nonempty_algHom_of_le
    {m n : RayClass.Modulus K}
    (hmn : m ≤ n) :
    Nonempty
      (rayClassField K m →ₐ[K]
        rayClassField K n)

theorem

rayClassFieldSubfield_mono

L274 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldSubfield_mono

Documentation

Divisibility of moduli gives literal inclusion of the corresponding intrinsic ray class fields inside the fixed separable closure.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassFieldSubfield_mono
    {m n : RayClass.Modulus K}
    (hmn : m ≤ n) :
    rayClassFieldSubfield K m ≤ rayClassFieldSubfield K n

theorem

nonempty_algHom_to_rayClassField_iff_isDefiningModulus

L295 ↗

GlobalClassFieldTheory.GlobalClassFields.nonempty_algHom_to_rayClassField_iff_isDefiningModulus

Documentation

A finite abelian extension embeds in the selected ray class field of modulus m exactly when m is a defining modulus for its genuine idèle-class norm subgroup.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    nonempty_algHom_to_rayClassField_iff_isDefiningModulus
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L]
    (m : RayClass.Modulus K) :
    Nonempty (L →ₐ[K] rayClassField K m) ↔
      IsDefiningModulus
        ((_root_.ideleClassNorm K L).range) m

theorem

nonempty_algHom_to_rayClassField_narrowOfFinite_iff_narrowFiniteConductor_le

L314 ↗

GlobalClassFieldTheory.GlobalClassFields.nonempty_algHom_to_rayClassField_narrowOfFinite_iff_narrowFiniteConductor_le

Documentation

Actual containment in a narrow ray class field is equivalent to divisibility by the exact narrow finite conductor.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    nonempty_algHom_to_rayClassField_narrowOfFinite_iff_narrowFiniteConductor_le
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L]
    (n : RayClass.FiniteModulus K) :
    Nonempty
        (L →ₐ[K]
          rayClassField K (RayClass.Modulus.narrowOfFinite n)) ↔
      ideleClassNormNarrowFiniteConductor (K := K) (L := L) ≤ n

theorem

finiteAbelianExtension_nonempty_algHom_to_conductorRayClassField

L342 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtension_nonempty_algHom_to_conductorRayClassField

Documentation

The ray class field of the exact narrow finite conductor genuinely contains the given finite abelian extension.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    finiteAbelianExtension_nonempty_algHom_to_conductorRayClassField
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L] :
    Nonempty
      (L →ₐ[K]
        rayClassField K
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := L))))

theorem

finiteAbelianExtension_exists_rayClassFieldEmbedding

L363 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtension_exists_rayClassFieldEmbedding

Documentation

Every finite abelian extension is genuinely contained in a ray class field over the original base.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem finiteAbelianExtension_exists_rayClassFieldEmbedding
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L] :
    ∃ m : RayClass.Modulus K,
      Nonempty (L →ₐ[K] rayClassField K m)

theorem

ideleClassNorm_narrowFiniteConductor_is_gcd_of_rayClassField_embeddings

L378 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_is_gcd_of_rayClassField_embeddings

Documentation

The exact narrow finite conductor is the greatest common divisor of the finite parts of the moduli of the actual ray class fields containing a finite abelian extension.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    ideleClassNorm_narrowFiniteConductor_is_gcd_of_rayClassField_embeddings
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L] :
    (∀ m : RayClass.Modulus K,
        Nonempty (L →ₐ[K] rayClassField K m) →
          ideleClassNormNarrowFiniteConductor
              (K := K) (L := L) ≤ m.finitePart) ∧
      (∀ d : RayClass.FiniteModulus K,
        (∀ m : RayClass.Modulus K,
          Nonempty (L →ₐ[K] rayClassField K m) →
            d ≤ m.finitePart) →
          d ≤ ideleClassNormNarrowFiniteConductor
            (K := K) (L := L))

def

rayClassFieldGaloisContinuousMulEquivRayClassGroup

L416 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldGaloisContinuousMulEquivRayClassGroup

Documentation

Global reciprocity for the selected ray class field as a homeomorphic multiplicative equivalence

Gal(K^m / K) ≃ₜ* C_K / C_K^m.

The topology is the genuine finite Krull topology on the Galois group and the native quotient topology on the ray class group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def
    rayClassFieldGaloisContinuousMulEquivRayClassGroup
    (m : RayClass.Modulus K) :
    Gal((rayClassField K m) / K) ≃ₜ*
      RayClass.RayClassGroup m

theorem

rayClassFieldGaloisContinuousMulEquivRayClassGroup_apply

L434 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldGaloisContinuousMulEquivRayClassGroup_apply

Documentation

The underlying map of topological ray-class reciprocity is the general closed-finite-index reciprocity equivalence.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    rayClassFieldGaloisContinuousMulEquivRayClassGroup_apply
    (m : RayClass.Modulus K)
    (σ : Gal((rayClassField K m)/K)) :
    rayClassFieldGaloisContinuousMulEquivRayClassGroup
        (K := K) m σ =
      closedFiniteIndexClassFieldGaloisEquivNormQuotient
        (K := K) (RayClass.Modulus.congruenceSubgroup m)
        (RayClass.isClosed_congruenceSubgroup m) σ

theorem

rayClassFieldGaloisContinuousMulEquivRayClassGroup_globalNormResidue

L449 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldGaloisContinuousMulEquivRayClassGroup_globalNormResidue

Documentation

On an idèle-class representative, topological ray-class reciprocity sends its genuine global norm-residue symbol to its ray class modulo C_K^m.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    rayClassFieldGaloisContinuousMulEquivRayClassGroup_globalNormResidue
    (m : RayClass.Modulus K)
    (c : IdeleClassGroup K) :
    rayClassFieldGaloisContinuousMulEquivRayClassGroup
        (K := K) m
        (Reciprocity.globalNormResidueMonoidHom
          K (rayClassField K m) c) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup m) c

theorem

rayClassField_finrank_eq_rayClassGroup_card

L467 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassField_finrank_eq_rayClassGroup_card

Documentation

The degree of the selected ray class field is the order of the ray class group.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassField_finrank_eq_rayClassGroup_card
    (m : RayClass.Modulus K) :
    Module.finrank K (rayClassField K m) =
      Nat.card (RayClass.RayClassGroup m)

abbrev

rayClassFieldGaloisEquivRayClassGroup

L491 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldGaloisEquivRayClassGroup

Documentation

Global reciprocity identifies the genuine Galois group of the selected ray class field with the ray class group C_K / C_K^m.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev rayClassFieldGaloisEquivRayClassGroup
    (m : RayClass.Modulus K) :
    Gal((rayClassField K m) / K) ≃*
      RayClass.RayClassGroup m

def

rayClassSubgroupFixedField

L501 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupFixedField

Documentation

The subfield of the ray class field fixed by a prescribed ray-class subgroup, transported through the genuine reciprocity equivalence.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassSubgroupFixedField
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    IntermediateField K (rayClassField K m)

def

rayClassSubgroupSubfield

L510 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupSubfield

Documentation

The fixed field, embedded in the chosen separable closure of the original number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassSubgroupSubfield
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    IntermediateField K (SeparableClosure K)

def

rayClassSubgroupSubextension

L518 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupSubextension

Documentation

The fixed field is a finite abelian extension of the original field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassSubgroupSubextension
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    ClassFieldTheory.FiniteAbelianExtension K

def

rayClassSubgroupFixedFieldArtin

L534 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupFixedFieldArtin

Documentation

The ray class group acts on the subfield fixed by H by restricting the reciprocity action on the full ray class field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassSubgroupFixedFieldArtin
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    RayClass.RayClassGroup m →*
      (rayClassSubgroupFixedField (K := K) m H ≃ₐ[K]
        rayClassSubgroupFixedField (K := K) m H)

theorem

rayClassSubgroupFixedFieldArtin_surjective

L546 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupFixedFieldArtin_surjective

Documentation

The restricted reciprocity action reaches every automorphism of the fixed field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassSubgroupFixedFieldArtin_surjective
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    Function.Surjective (rayClassSubgroupFixedFieldArtin (K := K) m H)

theorem

rayClassSubgroupFixedFieldArtin_ker

L557 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupFixedFieldArtin_ker

Documentation

The exact kernel of the fixed-field reciprocity action is H.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassSubgroupFixedFieldArtin_ker
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    (rayClassSubgroupFixedFieldArtin (K := K) m H).ker = H

theorem

rayClassGroup_mul_comm

L575 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassGroup_mul_comm

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassGroup_mul_comm
    (m : RayClass.Modulus K)
    (x y : RayClass.RayClassGroup m) : x * y = y * x

def

rayClassGroupInvHom

L589 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassGroupInvHom

Documentation

Inversion of ray classes is a homomorphism because idèle classes commute. This form does not require a commutative-group instance on the quotient presentation.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

def rayClassGroupInvHom (m : RayClass.Modulus K) :
    RayClass.RayClassGroup m →* RayClass.RayClassGroup m where
  toFun := Inv.inv
  map_one' := inv_one
  map_mul' x y := by
    rw [mul_inv_rev]
    exact rayClassGroup_mul_comm (K := K) m y⁻¹ x⁻¹

def

rayClassSubgroupArtin

L600 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupArtin

Documentation

Arithmetic reciprocity on the fixed field, transported to the chosen subextension of the separable closure of K. The ambient ray-class equivalence is geometrically normalized, so its input is inverted.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def rayClassSubgroupArtin
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    RayClass.RayClassGroup m →*
      (rayClassSubgroupSubextension (K := K) m H ≃ₐ[K]
        rayClassSubgroupSubextension (K := K) m H)

theorem

rayClassSubgroupArtin_surjective

L614 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupArtin_surjective

Documentation

The transported reciprocity map is surjective.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassSubgroupArtin_surjective
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    Function.Surjective (rayClassSubgroupArtin (K := K) m H)

theorem

rayClassSubgroupArtin_ker

L630 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupArtin_ker

Documentation

The transported reciprocity map has exactly the prescribed kernel.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassSubgroupArtin_ker
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    (rayClassSubgroupArtin (K := K) m H).ker = H

theorem

rayClassSubgroupSubextension_norm_range

L653 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupSubextension_norm_range

Documentation

The fixed subextension has a norm subgroup containing the ray congruence subgroup. This is the defining-modulus input for its unramifiedness away from the modulus.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassSubgroupSubextension_norm_range
    (m : RayClass.Modulus K)
    (H : Subgroup (RayClass.RayClassGroup m)) :
    RayClass.Modulus.congruenceSubgroup m ≤
      (_root_.ideleClassNorm K
        (rayClassSubgroupSubextension (K := K) m H)).range

theorem

rayClassFieldGaloisEquivRayClassGroup_globalNormResidue

L680 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFieldGaloisEquivRayClassGroup_globalNormResidue

Documentation

Under ray-class reciprocity, the actual global norm-residue symbol is the ray class of its idèle-class representative.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
open CyclicCohomology
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem rayClassFieldGaloisEquivRayClassGroup_globalNormResidue
    (m : RayClass.Modulus K)
    (c : IdeleClassGroup K) :
    rayClassFieldGaloisEquivRayClassGroup
        (K := K) m
        (globalNormResidueMonoidHom K
          (rayClassField K m) c) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup m) c

Module documentation

Actual ray class fields

Declarations