Etale algebras over fields

Main results

Let K be a field, A be a K-algebra and L be a field extension of K.

• Algebra.FormallyEtale.of_isSeparable: If L is separable over K, then L is formally etale over K.
• Algebra.FormallyEtale.iff_isSeparable: If L is (essentially) of finite type over K, then L/K is etale iff L/K is separable.

References

• B. Iversen, Generic Local Structure of the Morphisms in Commutative Algebra

theorem Algebra.FormallyEtale.of_isSeparable_aux (K L : Type u) [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] [Algebra.EssFiniteType K L] : Algebra.FormallyEtale K L

This is a weaker version of of_isSeparable that additionally assumes EssFiniteType K L. Use that instead.

This is Iversen Corollary II.5.3.

theorem Algebra.FormallyEtale.of_isSeparable (K L : Type u) [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] : Algebra.FormallyEtale K L

theorem Algebra.FormallyEtale.iff_isSeparable (K L : Type u) [Field K] [Field L] [Algebra K L] [Algebra.EssFiniteType K L] : Algebra.FormallyEtale K L ↔ Algebra.IsSeparable K L