English
If K is algebraically closed and L is a local ring, then L is a field iff L is separable over K.
Русский
Если K алгебраически замкнуто, L — локальное кольцо, тогда L является полем тогда и только тогда, когда L сепарабельно над K.
LaTeX
$$$[IsAlgClosed K] \Rightarrow ([\text{IsLocalRing } L] \Rightarrow ([\text{IsField } L] \Leftrightarrow [\text{IsSeparable } K L]))$$$
Lean4
theorem isReduced_of_field : IsReduced A := by
constructor
intro x hx
let f := (Algebra.TensorProduct.includeRight (R := K) (A := AlgebraicClosure K) (B := A))
have : Function.Injective f :=
by
have :
⇑f =
(LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap).comp
(Algebra.TensorProduct.lid K A).symm.toLinearMap :=
by ext x; simp [f]
rw [this]
suffices Function.Injective (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
exact this.comp (Algebra.TensorProduct.lid K A).symm.injective
apply Module.Flat.rTensor_preserves_injective_linearMap
exact (algebraMap K _).injective
apply this
rw [map_zero]
apply eq_zero_of_localization
intro M hM
have hy := (hx.map f).map (algebraMap _ (Localization.AtPrime M))
generalize algebraMap _ (Localization.AtPrime M) (f x) = y at *
have := EssFiniteType.of_isLocalization (Localization.AtPrime M) M.primeCompl
have := of_isLocalization (Rₘ := Localization.AtPrime M) M.primeCompl
have := EssFiniteType.comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
have := comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
letI := (isField_of_isAlgClosed_of_isLocalRing (AlgebraicClosure K) (A := Localization.AtPrime M)).toField
exact hy.eq_zero
