Module

PrimeGeneration.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.PrimeGeneration

1 declaration indexed from sourceView source ↗

Module documentation

Prime generation of ray ideal classes

The fractional ideals prime to a modulus are generated by their prime ideals away from the modulus. This is the algebraic input for comparing Frobenius-normalized ray reciprocity maps.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Ideal

Imported by6

theorem

primeToModulusIdeals_hom_ext

L31 ↗

RayClass.primeToModulusIdeals_hom_ext

Documentation

Two homomorphisms out of the prime-to-modulus fractional ideal group agree if they agree on each prime ideal away from the modulus.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
universe u v
open scoped Classical in

Lean source · statement

theorem primeToModulusIdeals_hom_ext
    {K : Type u} [Field K] [NumberField K]
    (m : RayClass.Modulus K)
    {G : Type v} [CommGroup G]
    (f g : RayClass.primeToModulusIdeals m →* G)
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (hv : v ∉ m.finitePart.support),
        f (RayClass.primeToModulusIdeal m v hv) =
          g (RayClass.primeToModulusIdeal m v hv)) :
    f = g

Module documentation

Prime generation of ray ideal classes

Declarations

primeToModulusIdeals_hom_ext