English
Let f: A ⟶ A' and g: B ⟶ B'. If prodComparison F A B and prodComparison F A' B' are isomorphisms, then inv(prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv(prodComparison F A' B').
Русский
Пусть f: A→A' и g: B→B'. Если prodComparison F A B и prodComparison F A' B' являются изоморфизмами, то inv(prodComparison F A B) ∘ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ∘ inv(prodComparison F A' B').
LaTeX
$$$ inv(\\operatorname{prodComparison} F A B) \\circ F(\\operatorname{prod.map} f g) = \\operatorname{prod.map}(F f)(F g) \\circ inv(\\operatorname{prodComparison} F A' B') $$$
Lean4
/-- If the product comparison morphism is an iso, its inverse is natural. -/
@[reassoc]
theorem prodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A B)]
[IsIso (prodComparison F A' B')] :
inv (prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B') :=
by rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
