Module

SimpleExtensionNorm.lean

Nyll.GaloisCohomology.Kummer.Concrete.SimpleExtensionNorm

1 declaration indexed from sourceView source ↗

Module documentation

Norm witnesses in simple Kummer extensions

This file constructs a field-generic norm witness for the pair formed by a unit and its nonzero complement. The construction uses the finite quotient of the roots of unity by the image of the simple Kummer character, so it does not require the defining power polynomial to be irreducible.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.SimpleExtension
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.NormQuotient
Mathlib.GroupTheory.Coset.Card
Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Imported by2

theorem

unit_mem_localNormSubgroup_chosenSimpleKummerExtension_one_sub

L33 ↗

KummerTheory.unit_mem_localNormSubgroup_chosenSimpleKummerExtension_one_sub

Documentation

If both a and 1 - a are nonzero, then a is a norm from the simple Kummer extension obtained by adjoining an n-th root of 1 - a.

Source context 4 commands

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

noncomputable section
namespace KummerTheory
open scoped BigOperators
variable (K : Type) [Field K]

Lean source · statement

theorem unit_mem_localNormSubgroup_chosenSimpleKummerExtension_one_sub
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (h_one_sub : 1 - (a : K) ≠ 0) :
    a ∈ LocalFieldTheory.localNormSubgroup K
      (chosenSimpleKummerExtension K n hnK
        (Units.mk0 (1 - (a : K)) h_one_sub))

Module documentation

Norm witnesses in simple Kummer extensions

Declarations

unit_mem_localNormSubgroup_chosenSimpleKummerExtension_one_sub