Module

RayClassGroupHomExtFinitePrime.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassGroupHomExtFinitePrime

1 declaration indexed from sourceView source ↗

Module documentation

Prime classes determine maps out of a ray class group

Finite primes away from the modulus generate enough of the ideal-theoretic ray class group to determine any homomorphism into a commutative group.

Imports3

Imported by2

theorem

rayClassGroup_hom_ext_finitePrime

L29 ↗

ClassFieldTheory.rayClassGroup_hom_ext_finitePrime

Documentation

Two homomorphisms from a ray class group agree if they have the same value on every prime class away from the modulus.

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 v

Lean source · statement

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

Module documentation

Prime classes determine maps out of a ray class group

Declarations

rayClassGroup_hom_ext_finitePrime