English
IsSeparable F F⟮x⟯ ↔ IsSeparable F x, via tower/top relations.
Русский
Сепарабельность F⟮x⟯ эквивалентна сепарабельности x, через тензорные/расширенные отношения.
LaTeX
$$$ Algebra.IsSeparable F F⟮x⟯ \iff IsSeparable F x $$$
Lean4
/-- If `K / E / F` is an extension tower such that `E / F` is separable,
`x : K` is separable over `E`, then it's also separable over `F`. -/
theorem of_algebra_isSeparable_of_isSeparable [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] {x : K}
(hsep : IsSeparable E x) : IsSeparable F x :=
by
set f := minpoly E x with hf
let E' : IntermediateField F E := adjoin F f.coeffs
haveI : FiniteDimensional F E' := finiteDimensional_adjoin fun x _ ↦ Algebra.IsSeparable.isIntegral F x
let g : E'[X] := f.toSubring E'.toSubring (subset_adjoin F _)
have h : g.map (algebraMap E' E) = f := f.map_toSubring E'.toSubring (subset_adjoin F _)
clear_value g
have hx : x ∈ restrictScalars F E'⟮x⟯ := mem_adjoin_simple_self _ x
have hzero : aeval x g = 0 := by simpa only [← hf, ← h, aeval_map_algebraMap] using minpoly.aeval E x
have halg : IsIntegral E' x := isIntegral_trans (R := F) (A := E) _ (IsSeparable.isIntegral hsep) |>.tower_top
simp only [IsSeparable, ← hf, ← h, separable_map] at hsep
replace hsep := hsep.of_dvd <| minpoly.dvd E' x hzero
haveI : Algebra.IsSeparable F E' := Algebra.isSeparable_tower_bot_of_isSeparable F E' E
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
haveI := adjoin.finiteDimensional halg
haveI : FiniteDimensional F E'⟮x⟯ := FiniteDimensional.trans F E' E'⟮x⟯
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F E' E'⟮x⟯
rw [finSepDegree_eq_finrank_of_isSeparable F E', finSepDegree_eq_finrank_of_isSeparable E' E'⟮x⟯,
Module.finrank_mul_finrank F E' E'⟮x⟯, eq_comm, finSepDegree_eq_finrank_iff F E'⟮x⟯] at this
change Algebra.IsSeparable F (restrictScalars F E'⟮x⟯) at this
exact isSeparable_of_mem_isSeparable F K hx
