Unramified algebras over fields

Main results

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

• Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_localRing: If A is K-unramified and K is alg-closed, then K = A.
• Algebra.FormallyUnramified.isReduced_of_field: If A is K-unramified then A is reduced.
• Algebra.FormallyUnramified.iff_isSeparable: L is unramified over K iff L is separable over K.

References

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

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

theorem Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_localRing (K : Type u) (A : Type u) [Field K] [CommRing A] [Algebra K A] [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] [IsAlgClosed K] [LocalRing A] : Function.Bijective ⇑(algebraMap K A)

theorem Algebra.FormallyUnramified.isField_of_isAlgClosed_of_localRing (K : Type u) (A : Type u) [Field K] [CommRing A] [Algebra K A] [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] [IsAlgClosed K] [LocalRing A] : IsField A

theorem Algebra.FormallyUnramified.isReduced_of_field (K : Type u) (A : Type u) [Field K] [CommRing A] [Algebra K A] [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] : IsReduced A

theorem Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable (K : Type u) (L : Type u) [Field K] [Field L] [Algebra K L] [Algebra.FormallyUnramified K L] [Algebra.EssFiniteType K L] [IsPurelyInseparable K L] : (algebraMap K L).range = ⊤

theorem Algebra.FormallyUnramified.isSeparable (K : Type u) (L : Type u) [Field K] [Field L] [Algebra K L] [Algebra.FormallyUnramified K L] [Algebra.EssFiniteType K L] : Algebra.IsSeparable K L

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