NYLL
Module

NarrowRayClassGroupEquivNarrowClassGroup.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.NarrowRayClassGroupEquivNarrowClassGroup
8 declarations indexed from sourceView source ↗

Module documentation

The narrow ray class group and the narrow ideal class group

At the modulus with no finite part and every real place selected, the ideal-theoretic ray class group is the narrow class group. The comparison preserves the class of each finite prime.

Imports5
Imported by1

Declarations

theorem

narrow_rayClassPrimeToIdeals_eq_top

L32 ↗
ClassFieldTheory.narrow_rayClassPrimeToIdeals_eq_top
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem narrow_rayClassPrimeToIdeals_eq_top :
    rayClassPrimeToIdeals (narrowRayClassModulus K) = ⊤
theorem

narrow_rayPrincipalIdealSubgroup_eq_positive

L37 ↗
ClassFieldTheory.narrow_rayPrincipalIdealSubgroup_eq_positive
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem narrow_rayPrincipalIdealSubgroup_eq_positive :
    rayPrincipalIdealSubgroup (narrowRayClassModulus K) =
      narrowPrincipalIdealSubgroup K
def

narrowRayIdealsEquiv

L71 ↗
ClassFieldTheory.narrowRayIdealsEquiv
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def narrowRayIdealsEquiv :
    rayClassPrimeToIdeals (narrowRayClassModulus K) ≃*
      NumberFieldFractionalIdealGroup K
theorem

narrowRayIdealsEquiv_apply

L77 ↗
ClassFieldTheory.narrowRayIdealsEquiv_apply
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem narrowRayIdealsEquiv_apply
    (I : rayClassPrimeToIdeals (narrowRayClassModulus K)) :
    narrowRayIdealsEquiv I = I.1
theorem

narrow_rayPrincipalIdealSubgroup_map

L81 ↗
ClassFieldTheory.narrow_rayPrincipalIdealSubgroup_map
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem narrow_rayPrincipalIdealSubgroup_map :
    (rayPrincipalIdealSubgroupInPrimeTo
      (narrowRayClassModulus K)).map
        (narrowRayIdealsEquiv (K := K) : _ →* _) =
      narrowPrincipalIdealSubgroup K
def

narrowRayClassGroupEquivNarrowClassGroup

L105 ↗
ClassFieldTheory.narrowRayClassGroupEquivNarrowClassGroup
Documentation

The narrow ray class group is canonically isomorphic to the independent ideal-theoretic narrow class group.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def narrowRayClassGroupEquivNarrowClassGroup :
    RayClassGroup (narrowRayClassModulus K) ≃* NarrowClassGroup K
theorem

narrowRayClassGroupEquivNarrowClassGroup_prime

L114 ↗
ClassFieldTheory.narrowRayClassGroupEquivNarrowClassGroup_prime
Documentation

The comparison sends a finite-prime ray class to its narrow ideal class.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem narrowRayClassGroupEquivNarrowClassGroup_prime
    (v : HeightOneSpectrum (𝓞 K)) :
    narrowRayClassGroupEquivNarrowClassGroup
        (narrowRayClassOfFinitePrime v) =
      QuotientGroup.mk' (narrowPrincipalIdealSubgroup K)
        (finitePrimeFractionalIdeal v)
theorem

exists_narrowRayClassGroupEquivNarrowClassGroup

L127 ↗
ClassFieldTheory.exists_narrowRayClassGroupEquivNarrowClassGroup
Documentation

The public narrow class-group comparison, including its action on every finite-prime class.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem exists_narrowRayClassGroupEquivNarrowClassGroup
    (K : Type u) [Field K] [NumberField K] :
    ∃ e : RayClassGroup (narrowRayClassModulus K) ≃* NarrowClassGroup K,
      ∀ v : HeightOneSpectrum (𝓞 K),
        e (narrowRayClassOfFinitePrime v) =
          QuotientGroup.mk' (narrowPrincipalIdealSubgroup K)
            (finitePrimeFractionalIdeal v)

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