Module

OrdinaryClassGroupComparison.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.OrdinaryClassGroupComparison

7 declarations indexed from sourceView source ↗

Module documentation

The ordinary ray class group and the ideal class group

The ray modulus with zero finite part and no real conditions gives precisely the ordinary ideal class group. The equivalence below also identifies their finite-prime classes.

Imports4

Imported by3

theorem

ordinary_rayClassPrimeToIdeals_eq_top

L29 ↗

ClassFieldTheory.ordinary_rayClassPrimeToIdeals_eq_top

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ordinary_rayClassPrimeToIdeals_eq_top :
    rayClassPrimeToIdeals (ordinaryRayClassModulus K) = ⊤

theorem

ordinary_rayPrincipalIdealSubgroup_eq_range

L34 ↗

ClassFieldTheory.ordinary_rayPrincipalIdealSubgroup_eq_range

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ordinary_rayPrincipalIdealSubgroup_eq_range :
    rayPrincipalIdealSubgroup (ordinaryRayClassModulus K) =
      (toPrincipalIdeal (𝓞 K) K).range

def

ordinaryRayIdealsEquiv

L51 ↗

ClassFieldTheory.ordinaryRayIdealsEquiv

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def ordinaryRayIdealsEquiv :
    rayClassPrimeToIdeals (ordinaryRayClassModulus K) ≃*
      NumberFieldFractionalIdealGroup K

theorem

ordinaryRayIdealsEquiv_apply

L57 ↗

ClassFieldTheory.ordinaryRayIdealsEquiv_apply

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ordinaryRayIdealsEquiv_apply
    (I : rayClassPrimeToIdeals (ordinaryRayClassModulus K)) :
    ordinaryRayIdealsEquiv I = I.1

theorem

ordinary_rayPrincipalIdealSubgroup_map

L61 ↗

ClassFieldTheory.ordinary_rayPrincipalIdealSubgroup_map

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ordinary_rayPrincipalIdealSubgroup_map :
    (rayPrincipalIdealSubgroupInPrimeTo
      (ordinaryRayClassModulus K)).map
        (ordinaryRayIdealsEquiv (K := K) : _ →* _) =
      (toPrincipalIdeal (𝓞 K) K).range

def

ordinaryRayClassGroupEquivClassGroup

L85 ↗

ClassFieldTheory.ordinaryRayClassGroupEquivClassGroup

Documentation

The ideal-theoretic ray class group at the trivial modulus is 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
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def ordinaryRayClassGroupEquivClassGroup :
    RayClassGroup (ordinaryRayClassModulus K) ≃* ClassGroup (𝓞 K)

theorem

ordinaryRayClassGroupEquivClassGroup_prime

L96 ↗

ClassFieldTheory.ordinaryRayClassGroupEquivClassGroup_prime

Documentation

The equivalence takes the ordinary ray class of a finite prime to the usual prime ideal class.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem ordinaryRayClassGroupEquivClassGroup_prime
    (v : HeightOneSpectrum (𝓞 K)) :
    ordinaryRayClassGroupEquivClassGroup
        (ordinaryRayClassOfFinitePrime v) =
      ClassGroup.mk K (finitePrimeFractionalIdeal v)

Module documentation

The ordinary ray class group and the ideal class group

Declarations

ordinary_rayClassPrimeToIdeals_eq_top

ordinary_rayPrincipalIdealSubgroup_eq_range

ordinaryRayIdealsEquiv

ordinaryRayIdealsEquiv_apply

ordinary_rayPrincipalIdealSubgroup_map

ordinaryRayClassGroupEquivClassGroup

ordinaryRayClassGroupEquivClassGroup_prime