English
Analogous to the previous case, but with the inr leg. For A in Under R, pushout.inr A.hom (algebraMap R S) followed by the right inverse of tensorProdObjIsoPushoutObjS A yields the left-inclusion induced map from Algebra.TensorProduct.includeLeft.
Русский
Аналогично предыдущему случаю, но с правой веткой inr. Для A в Under R композиция pushout.inr A.hom (algebraMap R S) за которым следует правая часть обратного (inv) у tensorProdObjIsoPushoutObjS A даёт включение слева, порождаемое Algebra.TensorProduct.includeLeft.
LaTeX
$$$pushout.inr\\,A.hom\\ (ofHom\\ (algebraMap R S)) \\;\\gg\\; (tensorProdObjIsoPushoutObj\\ S A).inv.right = \\mathrm{ofHom}\\left(\\mathrm{Algebra.TensorProduct.includeLeftRingHom}\\right)$$$
Lean4
@[reassoc (attr := simp)]
theorem pushout_inr_tensorProdObjIsoPushoutObj_inv_right (A : Under R) :
pushout.inr A.hom (ofHom <| algebraMap R S) ≫ (tensorProdObjIsoPushoutObj S A).inv.right =
(CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom) :=
by simp [tensorProdObjIsoPushoutObj]
