English
If A1 ≃+* A2 and B1 ≃+* B2 are compatible ring isomorphisms and B1 is separable over A1, then B2 is separable over A2.
Русский
Если существуют совместимые кольцевые изоморфизмы A1 ≃+* A2 и B1 ≃+* B2 и B1 разделимо над A1, то B2 разделимо над A2.
LaTeX
$$$\\text{IsSeparable } A_1 B_1 \\Rightarrow \\text{IsSeparable } A_2 B_2$ under compatible ring equivalences $(e_1,e_2)$ with $he$ commuting$$
Lean4
theorem of_equiv_equiv {x : B₁} (h : IsSeparable A₁ x) : IsSeparable A₂ (e₂ x) :=
letI := e₁.toRingHom.toAlgebra
letI : Algebra A₂ B₁ :=
{
(algebraMap A₁ B₁).comp
e₁.symm.toRingHom with
algebraMap := (algebraMap A₁ B₁).comp e₁.symm.toRingHom
smul := fun a b ↦ ((algebraMap A₁ B₁).comp e₁.symm.toRingHom a) * b
commutes' := fun r x ↦ (Algebra.commutes) (e₁.symm.toRingHom r) x
smul_def' := fun _ _ ↦ rfl }
haveI : IsScalarTower A₁ A₂ B₁ :=
IsScalarTower.of_algebraMap_eq <| fun x ↦ (algebraMap A₁ B₁).congr_arg <| id ((e₁.symm_apply_apply x).symm)
let e : B₁ ≃ₐ[A₂] B₂ :=
{ e₂ with
commutes' := fun x ↦ by simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm x) }
(AlgEquiv.isSeparable_iff e).mpr <| IsSeparable.tower_top A₂ h
