English
There is a canonical relation in the opposite setting between the inverse of the opProdIsoCoprod isomorphism, the unop of the right coproduct injection, and the second projection fst/snd; concretely, the inverse followed by inr unop equals prod.snd.
Русский
Пусть есть каноническая связь в противоположной обстановке между обратной стрелкой изоморфизма opProdIsoCoprod, unop инъекции правого копродукта и вторым проекционным морфизмом; конкретно, обратная стрелка после inr.unop даёт prod.snd.
LaTeX
$$$$(\operatorname{opProdIsoCoprod} A B)^{-1}.unop \;\;\circ \;\; \operatorname{coprod.inr}.unop = \operatorname{prod.snd}.$$$$
Lean4
@[reassoc (attr := simp)]
theorem opProdIsoCoprod_inv_inr : (opProdIsoCoprod A B).inv.unop ≫ coprod.inr.unop = prod.snd := by
rw [← unop_comp, inr_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
