English
Let F: C → D be a functor between cartesian monoidal categories. If for every pair of objects A, B in C the morphism prodComparison F A B is an isomorphism, then F preserves the binary product A × B, i.e. F preserves the limit of the diagram consisting of A and B.
Русский
Пусть F: C → D — функтор между картинами категорических монойалий. Если для каждой пары объектов A, B в C отображение prodComparison F A B является изоморфизмом, тогда F сохраняет бинарное произведение A × B, то есть предел диаграммы, состоящей из A и B.
LaTeX
$$$IsIso(\mathrm{prodComparison}\ F\ A\ B) \Rightarrow \mathrm{PreservesLimit}(\mathrm{pair}\ A\ B)\ F$$$
Lean4
/-- If `prodComparison F A B` is an isomorphism, then `F` preserves the limit of `pair A B`. -/
theorem preservesLimit_pair_of_isIso_prodComparison (A B : C) [IsIso (prodComparison F A B)] :
PreservesLimit (pair A B) F :=
by
apply preservesLimit_of_preserves_limit_cone (tensorProductIsBinaryProduct A B)
refine
IsLimit.equivOfNatIsoOfIso (pairComp A B F) _
((BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd _ _)).extend (prodComparison F A B))
(BinaryFan.ext (by exact Iso.refl _) ?_ ?_) |>.invFun
(IsLimit.extendIso _ (tensorProductIsBinaryProduct (F.obj A) (F.obj B)))
· dsimp only [BinaryFan.fst]
simp [pairComp]
· dsimp only [BinaryFan.snd]
simp [pairComp]
