NYLL
Module

Narrow.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Narrow
29 declarations indexed from sourceView source ↗

Module documentation

Narrow ideal classes

This file proves the exact sequence from global unit signs through the narrow and ordinary class groups.

Imports1
Imported by5

Declarations

theorem

finiteCongruenceSubgroup_zero

L28 ↗
RayClass.finiteCongruenceSubgroup_zero
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem finiteCongruenceSubgroup_zero :
    finiteCongruenceSubgroup (0 : FiniteModulus K) =
      FiniteIdeleGroup.integralSubgroup (K := K)
theorem

narrowIdeleCongruenceSubgroup_zero_le_integral

L36 ↗
RayClass.narrowIdeleCongruenceSubgroup_zero_le_integral
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem narrowIdeleCongruenceSubgroup_zero_le_integral :
    (Modulus.narrowOfFinite (0 : FiniteModulus K)).ideleCongruenceSubgroup ≤
      IdeleGroup.integralAtFinitePlaces (K := K)
def

narrowDenominator

L47 ↗
RayClass.narrowDenominator
Documentation

The subgroup generated by the zero-modulus congruence subgroup and the principal ideles; its quotient is the narrow class group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def narrowDenominator :
    Subgroup (IdeleGroup K)
abbrev

NarrowClassGroup

L53 ↗
RayClass.NarrowClassGroup
Documentation

The narrow class group realized as an idele quotient.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
abbrev NarrowClassGroup
    (K : Type*) [Field K] [NumberField K]
def

rayClassGroupNarrowZeroEquivNarrowClassGroup

L59 ↗
RayClass.rayClassGroupNarrowZeroEquivNarrowClassGroup
Documentation

The ray class group with zero finite part and every real place selected is the narrow class group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def rayClassGroupNarrowZeroEquivNarrowClassGroup :
    RayClassGroup (Modulus.narrowOfFinite (0 : FiniteModulus K)) ≃*
      NarrowClassGroup K
def

narrowToClassGroup

L67 ↗
RayClass.narrowToClassGroup
Documentation

The canonical map from the narrow class group to the ordinary ideal class group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def narrowToClassGroup :
    NarrowClassGroup K →* ClassGroup (𝓞 K)
theorem

narrowToClassGroup_mk

L85 ↗
RayClass.narrowToClassGroup_mk
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem narrowToClassGroup_mk (a : IdeleGroup K) :
    narrowToClassGroup
      (QuotientGroup.mk' (narrowDenominator (K := K)) a) =
      IdeleGroup.idealClass a
theorem

narrowToClassGroup_surjective

L91 ↗
RayClass.narrowToClassGroup_surjective
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem narrowToClassGroup_surjective :
    Function.Surjective
      (narrowToClassGroup (K := K))
abbrev

realSignGroup

L103 ↗
RayClass.realSignGroup
Documentation

The quotient of infinite ideles by the positive congruence subgroup.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
abbrev realSignGroup
    (K : Type*) [Field K] [NumberField K]
def

infiniteToIdele

L108 ↗
RayClass.infiniteToIdele
Documentation

Embed an infinite idele as an idele with trivial finite component.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def infiniteToIdele :
    InfiniteIdeleGroup K →* IdeleGroup K where
  toFun a := (a, 1)
  map_one' := rfl
  map_mul' _ _ := by simp
def

infiniteToNarrow

L115 ↗
RayClass.infiniteToNarrow
Documentation

Map an infinite idele to its narrow ideal class.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def infiniteToNarrow :
    InfiniteIdeleGroup K →* NarrowClassGroup K
theorem

narrowInfiniteCongruenceSubgroup_le_infiniteToNarrow_ker

L120 ↗
RayClass.narrowInfiniteCongruenceSubgroup_le_infiniteToNarrow_ker
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem narrowInfiniteCongruenceSubgroup_le_infiniteToNarrow_ker :
    narrowInfiniteCongruenceSubgroup (K := K) ≤
      (infiniteToNarrow (K := K)).ker
def

signToNarrow

L135 ↗
RayClass.signToNarrow
Documentation

The homomorphism from real sign classes to the narrow class group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def signToNarrow :
    realSignGroup K →* NarrowClassGroup K
theorem

signToNarrow_mk

L142 ↗
RayClass.signToNarrow_mk
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem signToNarrow_mk (a : InfiniteIdeleGroup K) :
    signToNarrow
        (QuotientGroup.mk'
          (narrowInfiniteCongruenceSubgroup (K := K)) a) =
      QuotientGroup.mk' (narrowDenominator (K := K))
        (infiniteToIdele (K := K) a)
theorem

signToNarrow_range_eq_narrowToClassGroup_ker

L150 ↗
RayClass.signToNarrow_range_eq_narrowToClassGroup_ker
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem signToNarrow_range_eq_narrowToClassGroup_ker :
    (signToNarrow (K := K)).range =
      (narrowToClassGroup (K := K)).ker
def

integralUnitToFieldUnit

L234 ↗
RayClass.integralUnitToFieldUnit
Documentation

The inclusion of global integral units into the field units.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def integralUnitToFieldUnit :
    (𝓞 K)ˣ →* Kˣ
theorem

toPrincipalIdeal_eq_one_iff_mem_integralUnits

L240 ↗
RayClass.toPrincipalIdeal_eq_one_iff_mem_integralUnits
Documentation

A field unit generates the unit fractional ideal exactly when it comes from a global integral unit.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem toPrincipalIdeal_eq_one_iff_mem_integralUnits
    (x : Kˣ) :
    toPrincipalIdeal (𝓞 K) K x = 1 ↔
      x ∈ (integralUnitToFieldUnit (K := K)).range
def

integralUnitToInfiniteIdele

L279 ↗
RayClass.integralUnitToInfiniteIdele
Documentation

The archimedean image of a global integral unit.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def integralUnitToInfiniteIdele :
    (𝓞 K)ˣ →* InfiniteIdeleGroup K
def

totallyPositiveUnitSubgroup

L286 ↗
RayClass.totallyPositiveUnitSubgroup
Documentation

The totally positive global units.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def totallyPositiveUnitSubgroup :
    Subgroup ((𝓞 K)ˣ)
abbrev

IntegralUnitSignGroup

L292 ↗
RayClass.IntegralUnitSignGroup
Documentation

The sign classes of global integral units.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
abbrev IntegralUnitSignGroup
def

integralUnitToRealSign

L296 ↗
RayClass.integralUnitToRealSign
Documentation

Send a global integral unit to its real sign class.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def integralUnitToRealSign :
    (𝓞 K)ˣ →* realSignGroup K
theorem

totallyPositiveUnitSubgroup_le_integralUnitToRealSign_ker

L302 ↗
RayClass.totallyPositiveUnitSubgroup_le_integralUnitToRealSign_ker
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem totallyPositiveUnitSubgroup_le_integralUnitToRealSign_ker :
    totallyPositiveUnitSubgroup (K := K) ≤
      (integralUnitToRealSign (K := K)).ker
def

integralUnitSignToRealSign

L311 ↗
RayClass.integralUnitSignToRealSign
Documentation

The induced map from integral-unit sign classes to real sign classes.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def integralUnitSignToRealSign :
    IntegralUnitSignGroup (K := K) →* realSignGroup K
theorem

integralUnitSignToRealSign_mk

L320 ↗
RayClass.integralUnitSignToRealSign_mk
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem integralUnitSignToRealSign_mk (u : (𝓞 K)ˣ) :
    integralUnitSignToRealSign
        (QuotientGroup.mk'
          (totallyPositiveUnitSubgroup (K := K)) u) =
      QuotientGroup.mk'
        (narrowInfiniteCongruenceSubgroup (K := K))
        (integralUnitToInfiniteIdele (K := K) u)
theorem

integralUnitSignToRealSign_injective

L329 ↗
RayClass.integralUnitSignToRealSign_injective
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem integralUnitSignToRealSign_injective :
    Function.Injective
      (integralUnitSignToRealSign (K := K))
theorem

principalIdele_integralUnit_finite_integral

L357 ↗
RayClass.principalIdele_integralUnit_finite_integral
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem principalIdele_integralUnit_finite_integral
    (u : (𝓞 K)ˣ) :
    (IdeleGroup.principalIdele K
        (integralUnitToFieldUnit (K := K) u)).2 ∈
      FiniteIdeleGroup.integralSubgroup (K := K)
theorem

signToNarrow_integralUnit

L373 ↗
RayClass.signToNarrow_integralUnit
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem signToNarrow_integralUnit (u : (𝓞 K)ˣ) :
    signToNarrow
        (QuotientGroup.mk'
          (narrowInfiniteCongruenceSubgroup (K := K))
          (integralUnitToInfiniteIdele (K := K) u)) = 1
theorem

integralUnitSignToRealSign_range_eq_signToNarrow_ker

L425 ↗
RayClass.integralUnitSignToRealSign_range_eq_signToNarrow_ker
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem integralUnitSignToRealSign_range_eq_signToNarrow_ker :
    (integralUnitSignToRealSign (K := K)).range =
      (signToNarrow (K := K)).ker
theorem

narrowClassGroup_exact_sequence

L530 ↗
RayClass.narrowClassGroup_exact_sequence
Documentation

The exact sequence

1 → 𝓞_Kˣ / 𝓞_{K,+}ˣ → ∏_{v real} ℝˣ / ℝ_{>0}ˣ → Cl_K¹ → Cl_K → 1.

Here complex places contribute a trivial sign quotient, so realSignGroup may uniformly be defined using all infinite places.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem narrowClassGroup_exact_sequence :
    Function.Injective
        (integralUnitSignToRealSign (K := K)) ∧
      (integralUnitSignToRealSign (K := K)).range =
        (signToNarrow (K := K)).ker ∧
      (signToNarrow (K := K)).range =
        (narrowToClassGroup (K := K)).ker ∧
      Function.Surjective (narrowToClassGroup (K := K))

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