English
This is a weaker version of the main Separable criterion: if K ⊆ L is a separable extension and EssFiniteType(K,L) holds, then L is formally étale over K.
Русский
Это частный случай основной теоремы о разделимости: если K ⊆ L является раздельным расширением и essFiniteType(K,L) выполняется, то L формально étale над K.
LaTeX
$$$[\text{Algebra.IsSeparable } K L] \Rightarrow \text{FormallyEtale } K L \text{ under EssFiniteType } K L$$$
Lean4
/-- 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 of_isSeparable_aux [Algebra.IsSeparable K L] [EssFiniteType K L] : FormallyEtale K L := by
-- We already know that for field extensions
-- IsSeparable + EssFiniteType => FormallyUnramified + Finite
have := FormallyUnramified.of_isSeparable K L
have := FormallyUnramified.finite_of_free (R := K) (S := L)
constructor
-- We shall show that any `f : L → B/I` can be lifted to `L → B` if `I^2 = ⊥`
intro B _ _ I h
refine ⟨FormallyUnramified.iff_comp_injective.mp (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
intro f
let pb := Field.powerBasisOfFiniteOfSeparable K L
obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (f pb.gen)
have helper : ∀ x, IsScalarTower.toAlgHom K B (B ⧸ I) x = Ideal.Quotient.mk I x := fun _ ↦ rfl
have hx' : Ideal.Quotient.mk I (aeval x (minpoly K pb.gen)) = 0 := by
rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Since `p` is separable, `-p'(x)` is invertible in `B ⧸ I`,
obtain ⟨u, hu⟩ : ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I :=
by
have :=
(isUnit_iff_ne_zero.mpr
((Algebra.IsSeparable.isSeparable K pb.gen).aeval_derivative_ne_zero (minpoly.aeval K _))).map
f
rw [← aeval_algHom_apply, ← hx, ← helper, aeval_algHom_apply, helper] at this
obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (-this.unit⁻¹ : B ⧸ I)
use u
rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg, IsUnit.mul_val_inv, neg_add_cancel]
-- And `ε = p(x)/(-p'(x))` works.
use pb.liftEquiv.symm ⟨x + u * aeval x (minpoly K pb.gen), ?_⟩
· apply pb.algHom_ext
simp [hx, hx']
· rw [← eval_map_algebraMap, Polynomial.eval_add_of_sq_eq_zero, derivative_map, ← one_mul (eval x _),
eval_map_algebraMap, eval_map_algebraMap, ← mul_assoc, ← add_mul, ← Ideal.mem_bot, ← h, pow_two, add_comm]
· exact Ideal.mul_mem_mul hu (Ideal.Quotient.eq_zero_iff_mem.mp hx')
rw [← Ideal.mem_bot, ← h]
apply Ideal.pow_mem_pow
rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_zero]
