English
If there is an equivalence of algebras between A1,B1 and A2,B2 compatible with the base maps, then separability transfers along the equivalence.
Русский
Если существует эквивалентность алгебр между A1,B1 и A2,B2, совместимая с базовыми отображениями, то разделимость перенесётся через эквивалентность.
LaTeX
$$$\\text{If } e_1 : A_1 \\simeq A_2,\\; e_2 : B_1 \\simeq B_2,\\; h : (algebraMap A_2 B_2) \\circ e_1 = e_2 \\circ (algebraMap A_1 B_1),\\; \\text{IsSeparable } A_1 B_1,\\; \\text{then } \\text{IsSeparable } A_2 B_2$$$
Lean4
theorem of_equiv_equiv [Algebra.IsSeparable A₁ B₁] : Algebra.IsSeparable A₂ B₂ :=
⟨fun x ↦ (e₂.apply_symm_apply x) ▸ _root_.IsSeparable.of_equiv_equiv e₁ e₂ he (Algebra.IsSeparable.isSeparable _ _)⟩
