English
If L is a finite type K-algebra with FormallyUnramified K L, then L is separable over K.
Русский
Если L — конечнопредельная над K алгебра с FormallyUnramified K L, тогда L сепарабельна над K.
LaTeX
$$$[\text{FormallyUnramified } K L] \Rightarrow [\text{IsSeparable } K L]$$$
Lean4
theorem of_isSeparable [Algebra.IsSeparable K L] : FormallyUnramified K L :=
by
rw [iff_comp_injective]
intro B _ _ I hI f₁ f₂ e
ext x
have : f₁ x - f₂ x ∈ I := by simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun e x
have :=
Polynomial.eval_add_of_sq_eq_zero ((minpoly K x).map (algebraMap K B)) (f₂ x) (f₁ x - f₂ x)
(show (f₁ x - f₂ x) ^ 2 ∈ ⊥ from hI ▸ Ideal.pow_mem_pow this 2)
simp only [add_sub_cancel, eval_map_algebraMap, aeval_algHom_apply, minpoly.aeval, map_zero, derivative_map,
zero_add] at this
rwa [eq_comm,
((isUnit_iff_ne_zero.mpr ((Algebra.IsSeparable.isSeparable K x).aeval_derivative_ne_zero (minpoly.aeval K x))).map
f₂).mul_right_eq_zero,
sub_eq_zero] at this
