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 étale over K.
• Algebra.FormallyEtale.iff_isSeparable: If L is (essentially) of finite type over K, then L/K is étale iff L/K is separable.
• Algebra.FormallyEtale.iff_exists_algEquiv_prod: If A is (essentially) of finite type over K, then A/K is étale iff A is a finite product of separable field extensions.
• Algebra.Etale.iff_exists_algEquiv_prod: A/K is étale iff A is a finite product of finite separable field extensions.

References

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

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

theorem Algebra.FormallyEtale.iff_exists_algEquiv_prod (K A : Type u) [Field K] [CommRing A] [Algebra K A] [Algebra.EssFiniteType K A] : Algebra.FormallyEtale K A ↔ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 : (i : I) → Algebra K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i), ∀ (i : I), Algebra.IsSeparable K (Ai i)

If A is an essentially of finite type algebra over a field K, then A is formally étale over K if and only if A is a finite product of separable field extensions.

theorem Algebra.Etale.iff_exists_algEquiv_prod (K A : Type u) [Field K] [CommRing A] [Algebra K A] : Algebra.Etale K A ↔ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 : (i : I) → Algebra K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i), ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)

A is étale over a field K if and only if A is a finite product of finite separable field extensions.