English
If coprodComparison F A B is an isomorphism, then inv(prodComparison F A B) ≫ coprod.map (F.map f) (F.map g) = coprod.map (F.map f) (F.map g) ≫ inv (coprodComparison F A' B').
Русский
Если coprodComparison F A B изоморфизм, то inv(prodComparison F A B) ∘ coprod.map (F.map f) (F.map g) = coprod.map (F.map f) (F.map g) ∘ inv (coprodComparison F A' B').
LaTeX
$$$ inv(\\operatorname{coprodComparison} F A B) \\circ \\operatorname{coprod.map}(F\\map f)(F\\map g) = \\operatorname{coprod.map}(F\\map f)(F\\map g) \\circ inv(\\operatorname{coprodComparison} F A' B') $$$
Lean4
/-- If the coproduct comparison morphism is an iso, its inverse is natural. -/
@[reassoc]
theorem coprodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (coprodComparison F A B)]
[IsIso (coprodComparison F A' B')] :
inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
F.map (coprod.map f g) ≫ inv (coprodComparison F A' B') :=
by rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]
