NYLL
Module

KummerAlgebraFiniteEtale.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraFiniteEtale
1 declaration indexed from sourceView source ↗

Module documentation

Finite étaleness of a Kummer algebra

The quotient by X ^ n - a is finite étale when the exponent is invertible in the base field. This includes reducible polynomials: the algebra need not be a field.

Imports4
Imported by3

Declarations

theorem

kummerAlgebra_finiteEtale

L28 ↗
ClassFieldTheory.kummerAlgebra_finiteEtale
Documentation

The canonical Kummer algebra is finite étale when its exponent is a unit in the base field.

Source context 3 commands

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

namespace ClassFieldTheory
open Polynomial
universe u
Lean source · statement
theorem kummerAlgebra_finiteEtale
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ)
    (hn : IsUnit ((n : ℕ) : K)) :
    Module.Finite K (KummerAlgebra K n a) ∧
      Algebra.Etale K (KummerAlgebra K n a)

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