Module

RayClassIdealModulusProjectionSurjective.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassIdealModulusProjectionSurjective

3 declarations indexed from sourceView source ↗

Module documentation

Surjectivity of the ideal-theoretic modulus projection

The direct ideal-quotient projection agrees with the natural idelic quotient projection because both preserve every prime class outside the larger modulus. The latter projection is directly surjective since both ray class groups are quotients of the same idèle class group.

Imports4

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

instance

rayClassGroupCommGroup

L30 ↗

ClassFieldTheory.rayClassGroupCommGroup

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

instance rayClassGroupCommGroup
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) : CommGroup (RayClassGroup m)

theorem

rayClassGroup_hom_ext_of_prime

L35 ↗

ClassFieldTheory.rayClassGroup_hom_ext_of_prime

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
private local instance rayClassGroupCommGroup
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) : CommGroup (RayClassGroup m) :=
  { (inferInstance : Group (RayClassGroup m)) with mul_comm := mul_comm' }

Lean source · statement

theorem rayClassGroup_hom_ext_of_prime
    (K : Type u) [Field K] [NumberField K]
    (n m : RayClassModulus K)
    (f g : RayClassGroup n →* RayClassGroup m)
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (hv : v ∉ n.finitePart.support),
        f (rayClassOfFinitePrime n v hv) =
          g (rayClassOfFinitePrime n v hv)) :
    f = g

theorem