Étale 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_formallyUnramified_of_field: If A is (essentially) of finite type over K, then A/K is formally étale iff A/K is formally unramified.
• 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 : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] [EssFiniteType K L] : 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 : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] : FormallyEtale K L

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

instance Algebra.FormallyEtale.instIsSeparableQuotientIdealOfEssFiniteTypeOfIsPrime (K : Type u_1) (A : Type u) [Field K] [CommRing A] [Algebra K A] [EssFiniteType K A] [FormallyEtale K A] (p : Ideal A) [p.IsPrime] : Algebra.IsSeparable K (A ⧸ p)

theorem Algebra.FormallyEtale.of_formallyUnramified_of_field (K : Type u_1) (A : Type u) [Field K] [CommRing A] [Algebra K A] [EssFiniteType K A] [FormallyUnramified K A] : FormallyEtale K A

theorem Algebra.FormallyEtale.iff_formallyUnramified_of_field {K : Type u_1} {A : Type u} [Field K] [CommRing A] [Algebra K A] [EssFiniteType K A] : FormallyEtale K A ↔ FormallyUnramified K A

theorem Algebra.FormallyEtale.iff_exists_algEquiv_prod (K : Type u_1) (A : Type u) [Field K] [CommRing A] [Algebra K A] [EssFiniteType K A] : 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.

noncomputable def Algebra.FormallyEtale.equivPiOfIsSepClosed (K : Type u_1) (A : Type u) [Field K] [CommRing A] [Algebra K A] [EssFiniteType K A] [FormallyEtale K A] [IsSepClosed K] : A ≃ₐ[K] PrimeSpectrum A → K

If R is an étale k-algebra over a separably closed field k, it is isomorphic to the (finite) product of copies of k indexed by the prime spectrum of R.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebra.FormallyEtale.equivPiOfIsSepClosed_self_apply {K : Type u_1} [Field K] [IsSepClosed K] (x : K) (p : PrimeSpectrum K) : (equivPiOfIsSepClosed K K) x p = x

@[simp]

theorem Algebra.FormallyEtale.equivPiOfIsSepClosed_comap {K : Type u_1} {A : Type u} [Field K] [CommRing A] [Algebra K A] {B : Type u_3} [CommRing B] [EssFiniteType K A] [FormallyEtale K A] [Algebra K B] [EssFiniteType K B] [FormallyEtale K B] [IsSepClosed K] (f : A →ₐ[K] B) (x : A) (p : PrimeSpectrum B) : (equivPiOfIsSepClosed K A) x (PrimeSpectrum.comap (↑f) p) = (equivPiOfIsSepClosed K B) (f x) p

theorem Algebra.Etale.iff_exists_algEquiv_prod (K : Type u_1) (A : Type u) [Field K] [CommRing A] [Algebra K A] : 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.