Commit 2024-10-22 19:00 b3184a91

feat(CategoryTheory/ChosenFiniteProducts): prodComparison and terminalComparison for ChosenFiniteProducts (#17701) Given a functor F : C ⥤ D between categories with chosen finite products and A B : C, introduce terminalComparison F : F (𝟙_ C) ⟶ 𝟙_ D and prodComparison F A B : F (A ⊗ B) ⟶ F A ⊗ F B the canonical maps.

• Show that terminalComparison is an isomorphism if and only if F preserves terminal objects.
• Show that the canonical map prodComparison F A B is natural in A and B and compatible with composition.
• Show that F preserves binary products if and only if prodComparison F A B is an isomorphism for all A B.