Commit 2025-04-24 19:56 a23b5d5e

View on Github →

refactor(ChosenFiniteProducts): don't make finite-product-preserving functors monoidal (#24049) Instead, reprove all the theorems about finite-product-preserving functors under the appropriate LaxMonoidal/ OplaxMonoidal/Monoidal assumptions. Also take the opportunity to sort the file slightly, correct docstrings and a few names. From Toric

Estimated changes

Modified Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean

Modified Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

added theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_hom

added theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_hom

added theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_toUnit_comp_rightUnitor_hom

added theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_toUnit_comp_leftUnitor_hom

deleted theorem CategoryTheory.Functor.EssImageSubcategory.associator_hom_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.associator_inv_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.fst_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.lift_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.snd_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.tensor_obj

deleted theorem CategoryTheory.Functor.EssImageSubcategory.toUnit_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.whiskerLeft_def

deleted theorem CategoryTheory.Functor.EssImageSubcategory.whiskerRight_def

deleted theorem CategoryTheory.Functor.Monoidal.lift_δ

deleted theorem CategoryTheory.Functor.Monoidal.lift_μ

deleted theorem CategoryTheory.Functor.Monoidal.toUnit_ε

deleted theorem CategoryTheory.Functor.Monoidal.δ_fst

deleted theorem CategoryTheory.Functor.Monoidal.δ_snd

deleted theorem CategoryTheory.Functor.Monoidal.ε_of_chosenFiniteProducts

deleted theorem CategoryTheory.Functor.Monoidal.μ_comp

deleted theorem CategoryTheory.Functor.Monoidal.μ_fst

deleted theorem CategoryTheory.Functor.Monoidal.μ_of_chosenFiniteProducts

deleted theorem CategoryTheory.Functor.Monoidal.μ_snd

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.associator_hom_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.associator_inv_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.fst_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.lift_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.snd_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.tensor_obj

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.toUnit_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.whiskerLeft_def

added theorem CategoryTheory.Functor.OplaxMonoidal.EssImageSubcategory.whiskerRight_def

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.lift_δ

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.lift_μ

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.toUnit_ε

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.δ_fst

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.δ_snd

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.ε_of_chosenFiniteProducts

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.μ_comp

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.μ_fst

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.μ_of_chosenFiniteProducts

added theorem CategoryTheory.Functor.OplaxMonoidal.Monoidal.μ_snd

added def CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts

added theorem CategoryTheory.Functor.OplaxMonoidal.δ_of_chosenFiniteProducts

added theorem CategoryTheory.Functor.OplaxMonoidal.η_of_chosenFiniteProducts

deleted def CategoryTheory.Functor.oplaxMonoidalOfChosenFiniteProducts

deleted theorem CategoryTheory.Functor.δ_of_chosenFiniteProducts

deleted theorem CategoryTheory.Functor.η_of_chosenFiniteProducts

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean