Module

FiniteEtaleSplittingField.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.FiniteEtaleSplittingField

1 declaration indexed from sourceView source ↗

Module documentation

A finite separable splitting field for a finite étale algebra

A maximal quotient of the actual finite faithfully flat splitting algebra is a finite separable field extension and still splits the original algebra. The construction also applies to the zero algebra.

Imports2

Mathlib.RingTheory.TotallySplit
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by2

theorem

exists_finite_separable_splittingField

L28 ↗

Algebra.IsFiniteSplit.exists_finite_separable_splittingField

Documentation

A finite étale algebra over a field splits over a finite separable field extension. No nontriviality assumption on the algebra is needed.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace Algebra.IsFiniteSplit
universe u

Lean source · statement

theorem exists_finite_separable_splittingField
    (K B : Type u) [Field K] [CommRing B] [Algebra K B]
    [Module.Finite K B] [Algebra.Etale K B] :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L)
      (_ : Module.Finite K L) (_ : Algebra.IsSeparable K L),
      Algebra.IsFiniteSplit L (L ⊗[K] B)

Module documentation

A finite separable splitting field for a finite étale algebra

Declarations

exists_finite_separable_splittingField