Module

PublicIdealNormQuotientComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicIdealNormQuotientComparison

2 declarations indexed from sourceView source ↗

Module documentation

Comparing source and public ideal-norm subgroups

The source ideal norm is defined before quotienting by principal ray ideals. The public ideal-norm image is its image in the ideal ray class group. This file records the exact comparison, including the principal-ray kernel.

Imports3

Imported by2

theorem

publicIdealNormDomain_eq_source'

L26 ↗

ClassFieldTheory.GlobalClassFieldComparison.publicIdealNormDomain_eq_source'

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison

Lean source · statement

theorem publicIdealNormDomain_eq_source'
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (m : RayClassModulus K) :
    rayClassPrimeToIdealNormDomain K L m =
      RayClass.primeToModulusIdeals
        (RayClass.idealNormLiftedModulus (K := K) (L := L)
          (rayClassModulusToOriginal K m))

theorem

publicIdealNormImage_comap_rayQuotient

L64 ↗

ClassFieldTheory.GlobalClassFieldComparison.publicIdealNormImage_comap_rayQuotient

Documentation

The preimage of the public ideal-norm image under the ray quotient is exactly the original norm subgroup, including principal ray ideals.