English
For A in Under R, the composition pushout.inl A.hom (algebraMap R S) followed by the right component of the inverse of tensorProdObjIsoPushoutObj S A equals the canonical right-inclusion map of the tensor product, i.e., the right-hand algebra inclusion.
Русский
Для A в Under R композиция pushout.inl A.hom (algebraMap R S) затем правая компонента обратного (inverse) тензорного-произведения равна каноническому правому включению в тензорном произведении.
LaTeX
$$$pushout.inl\\,A.hom\\ (ofHom\\ (algebraMap\\ R\\ S)) \\;\\gg\\; (tensorProdObjIsoPushoutObj\\ S\\ A).inv.right = \\mathrm{ofHom}\\left(\\mathrm{Algebra.TensorProduct.includeRight.toRingHom}\\right)$$$
Lean4
@[reassoc (attr := simp)]
theorem pushout_inl_tensorProdObjIsoPushoutObj_inv_right (A : Under R) :
pushout.inl A.hom (ofHom <| algebraMap R S) ≫ (tensorProdObjIsoPushoutObj S A).inv.right =
(ofHom <| Algebra.TensorProduct.includeRight.toRingHom) :=
by simp [tensorProdObjIsoPushoutObj]
