Commit 2025-04-08 16:10 0050e795

View on Github →

feat: the essential image of a finite product-preserving functor is cartesian-monoidal (#23562) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

deleted theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst

added theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst

added theorem CategoryTheory.Functor.EssImageSubcategory.NatTrans.monoidal_of_preservesFiniteProducts

added theorem CategoryTheory.Functor.EssImageSubcategory.associator_hom_def

added theorem CategoryTheory.Functor.EssImageSubcategory.associator_inv_def

added theorem CategoryTheory.Functor.EssImageSubcategory.fst_def

added theorem CategoryTheory.Functor.EssImageSubcategory.lift_def

added theorem CategoryTheory.Functor.EssImageSubcategory.snd_def

added theorem CategoryTheory.Functor.EssImageSubcategory.tensor_obj

added theorem CategoryTheory.Functor.EssImageSubcategory.toUnit_def

added theorem CategoryTheory.Functor.EssImageSubcategory.whiskerLeft_def

added theorem CategoryTheory.Functor.EssImageSubcategory.whiskerRight_def

deleted theorem CategoryTheory.NatTrans.monoidal_of_preservesFiniteProducts