Module

OrdinaryRayClassGroupEquivClassGroup.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.OrdinaryRayClassGroupEquivClassGroup

1 declaration indexed from sourceView source ↗

Module documentation

The ordinary ray class group is the ideal class group

At the modulus with no finite or real conditions, the ideal-theoretic ray class group agrees with Mathlib's ideal class group. The comparison also preserves the class of each finite prime, fixing its arithmetic meaning.

Imports6

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

exists_ordinaryRayClassGroupEquivClassGroup

L31 ↗

ClassFieldTheory.exists_ordinaryRayClassGroupEquivClassGroup

Documentation

The ordinary ray class group is isomorphic to the ideal class group, and the isomorphism sends each finite-prime ray class to its ideal class.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem exists_ordinaryRayClassGroupEquivClassGroup
    (K : Type) [Field K] [NumberField K] :
    ∃ e : RayClassGroup (ordinaryRayClassModulus K) ≃* ClassGroup (𝓞 K),
      ∀ v : HeightOneSpectrum (𝓞 K),
        e (ordinaryRayClassOfFinitePrime v) =
          ClassGroup.mk K (finitePrimeFractionalIdeal v)

Module documentation

The ordinary ray class group is the ideal class group

Declarations

exists_ordinaryRayClassGroupEquivClassGroup