Module

RootQuotientChoiceIndependence.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.RootQuotientChoiceIndependence

1 declaration indexed from sourceView source ↗

Module documentation

Independence of the chosen Kummer root

When the base field contains the n-th roots of unity, the quotient σ(u) / u depends only on u ^ n. In particular, the Artin root quotient used to normalize a local Hilbert symbol does not depend on the root chosen.

Imports2

Mathlib.FieldTheory.Galois.Basic
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

rootQuotient_eq_of_pow_eq_pow

L23 ↗

ClassFieldTheory.rootQuotient_eq_of_pow_eq_pow

Documentation

Two roots with the same n-th power have the same Galois root quotient when the base field contains a primitive n-th root of unity. This also applies when σ is a local Artin automorphism.

Source context 1 command

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

namespace ClassFieldTheory

Lean source · statement

theorem rootQuotient_eq_of_pow_eq_pow
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u v : Lˣ) (huv : u ^ (n : ℕ) = v ^ (n : ℕ))
    (σ : L ≃ₐ[K] L) :
    σ • u / u = σ • v / v

Module documentation

Independence of the chosen Kummer root

Declarations

rootQuotient_eq_of_pow_eq_pow