English
If Q is the image of P under an A-algebra isomorphism σ:B≅C (i.e., Q = map σ P), then there exists an isomorphism of A∕p-algebras between B∕P and C∕Q, induced by σ.
Русский
Если Q является образом P под A-алгебраическим изоморфизмом σ: B ≅ C (то есть Q = map σ P), то существует изоморфизм A∕p-алгебр между B∕P и C∕Q, индуцированный σ.
LaTeX
$$$\exists \phi:\,(B/P) \cong_{A/\!p} (C/Q)\quad\text{iff}\quad Q = P^{\mathrm{map},\,\sigma},$$$
Lean4
/-- An `A ⧸ p`-algebra isomorphism between `B ⧸ P` and `C ⧸ Q` induced by an `A`-algebra
isomorphism between `B` and `C`, where `Q = σ P`. -/
def algEquivOfEqMap (h : Q = P.map σ) : (B ⧸ P) ≃ₐ[A ⧸ p] (C ⧸ Q)
where
__ := quotientEquiv P Q σ h
commutes' := by
rintro ⟨x⟩
exact congrArg (Ideal.Quotient.mk Q) (AlgHomClass.commutes σ x)
