Module

KummerNormDescent.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.KummerNormDescent

2 declarations indexed from sourceView source ↗

Module documentation

Descent of power-local-unit idèle subgroups

For a finite extension L / K, the norm of a local n-th power is again an n-th power. At a finite place outside a prescribed support, the norm of an integral unit is an integral unit. Combining these statements over all places above a place of K shows that the ordinary idèle norm carries the power-local-unit subgroup for the full inverse-image support on L into the corresponding subgroup on K.

Passing to principal-idèle quotients gives the idèle-class norm descent needed when a Kummer extension is first constructed after a finite base extension and then viewed over the original number field.

Imports9

Imported by2

theorem

ideleNorm_mem_powerLocalUnitSubgroup_of_supports_above

L54 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleNorm_mem_powerLocalUnitSubgroup_of_supports_above

Documentation

If S' is exactly the set of finite places of L above S, the ordinary idèle norm carries the power-local-unit subgroup over L into the corresponding subgroup over K.

Source context 8 commands

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

open scoped BigOperators NumberField NumberField.LiesOver
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open AlgebraicNumberTheory.Valuations
open GlobalClassFieldTheory.ClassFieldAxiom
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem ideleNorm_mem_powerLocalUnitSubgroup_of_supports_above
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (S' : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : ∀ W : HeightOneSpectrum (𝓞 L),
      W ∈ S' ↔ _root_.finitePlaceBelow (K := K) W ∈ S)
    {a : IdeleGroup L}
    (ha :
      a ∈ idelePowerLocalUnitSubgroup (K := L) n S' ∅) :
    IdeleGroup.norm K L a ∈
      idelePowerLocalUnitSubgroup (K := K) n S ∅

theorem

ideleClassNorm_map_powerLocalUnitSubgroup_le_of_supports_above

L165 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_map_powerLocalUnitSubgroup_le_of_supports_above