Module

NormalClosureNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.NormalClosureNorm

1 declaration indexed from sourceView source ↗

Module documentation

Idèle-class norms from a finite normal closure

The distinguished copy of a finite extension inside its normal closure is an intermediate field. Norm transitivity therefore puts every norm from the normal closure inside the norm subgroup of that copy. Transport across the canonical algebra equivalence identifies the latter subgroup with the norm subgroup of the original extension.

Imports4

Imported by7

theorem

finiteNormalClosure_ideleClassNorm_range_le_source

L41 ↗

Documentation

Every idèle-class norm from the finite normal closure of L / K is already an idèle-class norm from L / K. This supplies a genuine finite Galois norm neighbourhood inside the norm subgroup of an arbitrary finite extension.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem finiteNormalClosure_ideleClassNorm_range_le_source :
    (_root_.ideleClassNorm K (finiteNormalClosure K L)).range ≤
      (_root_.ideleClassNorm K L).range

Module documentation

Idèle-class norms from a finite normal closure

Declarations

finiteNormalClosure_ideleClassNorm_range_le_source