English
If P = Q.comap σ for some A-algebra isomorphism σ:B≃C, then there is an induced A∕p-algebra isomorphism between B∕P and C∕Q, again given by an appropriate quotient equivalence.
Русский
Если P = Q.comap σ для некоторого A-алгебрического изоморфизма σ: B ≃ C, то существует индуцированный изоморфизм A∕p-алгебр между B∕P и C∕Q, задаваемый соответствующим эквивалентом частот.
LaTeX
$$$P = Q^{\mathrm{comap},\,\sigma} \Rightarrow (B/P) \cong_{A/\!p} (C/Q)$$
Lean4
/-- An `A ⧸ p`-algebra isomorphism between `B ⧸ P` and `C ⧸ Q` induced by an `A`-algebra
isomorphism between `B` and `C`, where `P = σ⁻¹ Q`. -/
def algEquivOfEqComap (h : P = Q.comap σ) : (B ⧸ P) ≃ₐ[A ⧸ p] (C ⧸ Q) :=
algEquivOfEqMap p σ ((congrArg (map σ) h).trans (Q.map_comap_eq_self_of_equiv σ)).symm
