Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraNormProduct

theorem

kummerAlgebra_exists_normProductDecomposition

ClassFieldTheory.kummerAlgebra_exists_normProductDecomposition

Documentation

For an invertible exponent, the canonical Kummer algebra has a finite separable field-product decomposition whose algebra norm is the product of the norms of its coordinates.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem kummerAlgebra_exists_normProductDecomposition
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ)
    (hn : IsUnit ((n : ℕ) : K)) :
    ∃ (I : Type u) (_ : Fintype I) (E : I → Type u)
      (_ : ∀ i, Field (E i)) (_ : ∀ i, Algebra K (E i))
      (e : KummerAlgebra K n a ≃ₐ[K] ∀ i, E i),
      (∀ i, Module.Finite K (E i) ∧ Algebra.IsSeparable K (E i)) ∧
      ∀ z : KummerAlgebra K n a,
        Algebra.norm K z = ∏ i, Algebra.norm K (e z i)

KummerAlgebraNormProduct.lean

Module documentation

Norm across the finite product of Kummer field factors

kummerAlgebra_exists_normProductDecomposition

Module documentation

Norm across the finite product of Kummer field factors

Declarations

kummerAlgebra_exists_normProductDecomposition