Theorems · Definition · category theory

CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C ≌ CategoryTheory.Mon C

Monoid objects in C are "just" lax monoidal functors from the trivial monoidal category to C.

Defined in: Mathlib.CategoryTheory.Monoidal.Mon
Cited by: 13 results in Mathlib
Foundations: Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.MonoidalCategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.MonoidalCategorystatement and proof · cited by 3,095
CategoryTheory.Discretestatement · cited by 2,447
CategoryTheory.Equivalencestatement · cited by 601
CategoryTheory.Monstatement · cited by 465
CategoryTheory.LaxMonoidalFunctorstatement · cited by 96
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMonproof · cited by 15
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalproof · cited by 15
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIsoproof · cited by 2
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoproof · cited by 2

Cited by13

Results whose statement or proof uses this declaration.

CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_appstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_εstatement · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μstatement · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_mapstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_objstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_appstatement · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_appstatement · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_homstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_homstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_map_homstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_Xstatement and proof · cited by 0
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_mulstatement · cited by 0