Module

NormLimitationCore.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.NormLimitationCore

2 declarations indexed from sourceView source ↗

Module documentation

Proof core for ideal norm limitation

This leaf proves the packaged statement using the idèle-class norm-range equality and the finite-extension ideal Artin kernel theorem.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.NormLimitationStatement

Imported by2

theorem

idealArtinKernel_congr

L29 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernel_congr

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem idealArtinKernel_congr
    (m : RayClass.Modulus K)
    {N P : Subgroup (IdeleClassGroup K)}
    (hN : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (hP : RayClass.Modulus.congruenceSubgroup m ≤ P)
    (hNP : N = P) :
    idealArtinKernel m N hN = idealArtinKernel m P hP

theorem

idealNormSubgroupMaximalAbelianStatement_proof

L40 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealNormSubgroupMaximalAbelianStatement_proof

Documentation

Core proof of the packaged ideal norm-limitation statement.