NYLL
Module

KummerAlgebraUniformFieldFactors.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraUniformFieldFactors
2 declarations indexed from sourceView source ↗

Module documentation

Uniform field factors of a Kummer algebra

If the base field contains the n-th roots of unity, every field factor of K[X] / (X ^ n - a) is a splitting field of the same polynomial. Thus all factors in the finite product decomposition are isomorphic over the base.

Imports4
Imported by2

Declarations

theorem

isSplittingField_of_root_generated

L28 ↗
ClassFieldTheory.isSplittingField_of_root_generated
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
open Polynomial
universe u
Lean source · statement
theorem isSplittingField_of_root_generated
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (a : Kˣ)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (β : L)
    (hpow : β ^ (n : ℕ) = algebraMap K L (a : K))
    (hgen : IntermediateField.adjoin K {β} = ⊤) :
    Polynomial.IsSplittingField K L
      (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K))
theorem

kummerAlgebra_exists_algEquiv_pi_isomorphicFields

L59 ↗
ClassFieldTheory.kummerAlgebra_exists_algEquiv_pi_isomorphicFields
Documentation

When K contains the n-th roots of unity, the root-generated field factors of its Kummer algebra are pairwise isomorphic over K.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
open Polynomial
universe u
Lean source · statement
theorem kummerAlgebra_exists_algEquiv_pi_isomorphicFields
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ)
    (hn : IsUnit ((n : ℕ) : K))
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ∃ (I : Type u) (_ : Finite 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) ∧
        ∃ β : E i,
          β = (e (AdjoinRoot.root
            (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)))) i ∧
          β ^ (n : ℕ) = algebraMap K (E i) (a : K) ∧
          IntermediateField.adjoin K {β} = ⊤) ∧
      ∀ i j, Nonempty (E i ≃ₐ[K] E j)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.