Commit 2024-05-23 18:50 8720e506

View on Github →

feat: no interesting comonoid objects in cartesian monoidal categories (#10103)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

deleted theorem CategoryTheory.Limits.initial.hom_ext

added theorem CategoryTheory.Limits.initial.strict_hom_ext

deleted theorem CategoryTheory.Limits.terminal.hom_ext

added theorem CategoryTheory.Limits.terminal.strict_hom_ext

Modified Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

added theorem CategoryTheory.Limits.initial.hom_ext

added theorem CategoryTheory.Limits.terminal.hom_ext

Created Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean

added def cartesianComon_

added def comonEquiv

added theorem comul_eq_diag

added theorem counit_eq_from

added def iso_cartesianComon_

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_fst

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_fst

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_snd

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_snd

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_snd

added theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorUnit

added theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext

added theorem CategoryTheory.monoidalOfHasFiniteProducts.unit_ext