Module

KummerAlgebraNormIffSimpleRadicalNorm.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraNormIffSimpleRadicalNorm

1 declaration indexed from sourceView source ↗

Module documentation

Norms from a Kummer algebra and a simple radical field

The canonical algebra K[X] / (X^n - a) need not be a field. When K contains the n-th roots of unity and n is nonzero in K, its norm image on units nevertheless agrees with the norm image of a field generated by an n-th root of a. One root works simultaneously for every target value.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

kummerAlgebra_norm_iff_simpleRadicalNorm

L23 ↗

ClassFieldTheory.kummerAlgebra_norm_iff_simpleRadicalNorm

Documentation

There is an n-th root of a whose simple radical extension has exactly the same norm values on units as the possibly reducible Kummer algebra.

Source context 1 command

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

namespace ClassFieldTheory

Lean source · statement

theorem kummerAlgebra_norm_iff_simpleRadicalNorm
    (K : Type) [Field K] (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    ∃ β : SeparableClosure K,
      β ^ (n : ℕ) = algebraMap K (SeparableClosure K) (a : K) ∧
      ∀ b : Kˣ,
        (∃ y : (KummerAlgebra K n a)ˣ,
          Algebra.norm K (y : KummerAlgebra K n a) = (b : K)) ↔
        ∃ z : (IntermediateField.adjoin K {β})ˣ,
          Algebra.norm K (z.val : IntermediateField.adjoin K {β}) = (b : K)

Module documentation

Norms from a Kummer algebra and a simple radical field

Declarations

kummerAlgebra_norm_iff_simpleRadicalNorm