Yoneda embedding of Mon C

We show that monoid objects in Cartesian monoidal categories are exactly those whose yoneda presheaf is a presheaf of monoids, by constructing the yoneda embedding Mon C ⥤ Cᵒᵖ ⥤ MonCat.{v} and showing that it is fully faithful and its (essential) image is the representable functors.

instance MonObj.instIsMonHomToUnit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M : C} [MonObj M] : IsMonHom (CategoryTheory.CartesianMonoidalCategory.toUnit M)

instance MonObj.instIsMonHomOne {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M : C} [MonObj M] : IsMonHom one

theorem MonObj.lift_lift_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [MonObj B] (f g h : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g) mul) h) mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) mul)) mul

@[simp]

theorem MonObj.lift_comp_one_left {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [MonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f one) g) mul = g

@[simp]

theorem MonObj.lift_comp_one_left_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [MonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f one) g) (CategoryTheory.CategoryStruct.comp mul h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem MonObj.lift_comp_one_right {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [MonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g one)) mul = f

@[simp]

theorem MonObj.lift_comp_one_right_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [MonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g one)) (CategoryTheory.CategoryStruct.comp mul h) = CategoryTheory.CategoryStruct.comp f h

instance MonObj.instIsMonHomFst {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [MonObj M] [MonObj N] [CategoryTheory.BraidedCategory C] : IsMonHom (CategoryTheory.CartesianMonoidalCategory.fst M N)

instance MonObj.instIsMonHomSnd {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [MonObj M] [MonObj N] [CategoryTheory.BraidedCategory C] : IsMonHom (CategoryTheory.CartesianMonoidalCategory.snd M N)

instance MonObj.instIsMonHomLift {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N O : C} [MonObj M] [MonObj N] [MonObj O] [CategoryTheory.BraidedCategory C] {f : M ⟶ N} {g : M ⟶ O} [IsMonHom f] [IsMonHom g] : IsMonHom (CategoryTheory.CartesianMonoidalCategory.lift f g)

instance MonObj.instIsMonHomMulOfIsCommMonObj {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M : C} [MonObj M] [CategoryTheory.BraidedCategory C] [IsCommMonObj M] : IsMonHom mul

instance Mon.instCartesianMonoidalCategory {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.CartesianMonoidalCategory (Mon C)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Mon.lift_hom {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N₁ N₂ : Mon C} (f : M ⟶ N₁) (g : M ⟶ N₂) : (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom

@[simp]

theorem Mon.fst_hom {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon C) : (CategoryTheory.CartesianMonoidalCategory.fst M N).hom = CategoryTheory.CartesianMonoidalCategory.fst M.X N.X

@[simp]

theorem Mon.snd_hom {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon C) : (CategoryTheory.CartesianMonoidalCategory.snd M N).hom = CategoryTheory.CartesianMonoidalCategory.snd M.X N.X

def MonObj.ofRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : MonObj X

If X represents a presheaf of monoids, then X is a monoid object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonObj.ofRepresentableBy_mul {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : mul = α.homEquiv.symm (α.homEquiv (CategoryTheory.CartesianMonoidalCategory.fst X X) * α.homEquiv (CategoryTheory.CartesianMonoidalCategory.snd X X))

@[simp]

theorem MonObj.ofRepresentableBy_one {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : one = α.homEquiv.symm 1

@[deprecated MonObj.ofRepresentableBy (since := "2025-09-09")]

def Mon_Class.ofRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : MonObj X

Alias of MonObj.ofRepresentableBy.

---

If X represents a presheaf of monoids, then X is a monoid object.

Equations

• @Mon_Class.ofRepresentableBy = @MonObj.ofRepresentableBy

@[deprecated MonObj.ofRepresentableBy (since := "2025-03-07")]

def MonObjOfRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : MonObj X

Alias of MonObj.ofRepresentableBy.

---

If X represents a presheaf of monoids, then X is a monoid object.

Equations

• @MonObjOfRepresentableBy = @MonObj.ofRepresentableBy

@[deprecated MonObj.ofRepresentableBy (since := "2025-09-09")]

def Mon_ClassOfRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : MonObj X

Alias of MonObj.ofRepresentableBy.

---

If X represents a presheaf of monoids, then X is a monoid object.

Equations

• @Mon_ClassOfRepresentableBy = @MonObj.ofRepresentableBy

@[reducible, inline]

abbrev Hom.monoid {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [MonObj M] : Monoid (X ⟶ M)

If M is a monoid object, then Hom(X, M) has a monoid structure.

Equations

• One or more equations did not get rendered due to their size.

theorem Hom.one_def {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [MonObj M] : 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) MonObj.one

theorem Hom.mul_def {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [MonObj M] (f₁ f₂ : X ⟶ M) : f₁ * f₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) MonObj.mul

theorem CategoryTheory.Functor.map_mul {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] (f g : X ⟶ M) : F.map (f * g) = F.map f * F.map g

@[simp]

theorem CategoryTheory.Functor.map_one {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] : F.map 1 = 1

def CategoryTheory.Functor.homMonoidHom {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] : (X ⟶ M) →* (F.obj X ⟶ F.obj M)

Functor.map of a monoidal functor as a MonoidHom.

Equations

• F.homMonoidHom = { toFun := F.map, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.homMonoidHom_apply {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] (a✝ : X ⟶ M) : F.homMonoidHom a✝ = F.map a✝

def CategoryTheory.Functor.FullyFaithful.homMulEquiv {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] (hF : F.FullyFaithful) : (X ⟶ M) ≃* (F.obj X ⟶ F.obj M)

Functor.map of a fully faithful monoidal functor as a MulEquiv.

Equations

• CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF = { toEquiv := hF.homEquiv, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (a✝ : X ⟶ M) : (homMulEquiv F hF) a✝ = F.map a✝

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply {C : Type u_1} {D : Type u_2} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [Category.{w, u_2} D] [CartesianMonoidalCategory D] {M X : C} [MonObj M] (F : Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M) : (homMulEquiv F hF).symm f = hF.preimage f

@[reducible, inline]

abbrev Hom.commMonoid {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [MonObj M] [CategoryTheory.BraidedCategory C] [IsCommMonObj M] : CommMonoid (X ⟶ M)

If M is a commutative monoid object, then Hom(X, M) has a commutative monoid structure.

Equations

• Hom.commMonoid = { toMonoid := Hom.monoid, mul_comm := ⋯ }

def yonedaMonObj {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : CategoryTheory.Functor Cᵒᵖ MonCat

If M is a monoid object, then Hom(-, M) is a presheaf of monoids.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem yonedaMonObj_obj_coe {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] (X : Cᵒᵖ) : ↑((yonedaMonObj M).obj X) = (Opposite.unop X ⟶ M)

@[simp]

theorem yonedaMonObj_map {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] {X Y₂ : Cᵒᵖ} (φ : X ⟶ Y₂) : (yonedaMonObj M).map φ = MonCat.ofHom { toFun := fun (x : Opposite.unop X ⟶ M) => CategoryTheory.CategoryStruct.comp φ.unop x, map_one' := ⋯, map_mul' := ⋯ }

def yonedaMonObjIsoOfRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) : yonedaMonObj X ≅ F

If X represents a presheaf of monoids F, then Hom(-, X) is isomorphic to F as a presheaf of monoids.

Equations

• yonedaMonObjIsoOfRepresentableBy X F α = CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (let __Equiv := α.homEquiv; { toEquiv := __Equiv, map_mul' := ⋯ }).toMonCatIso) ⋯

@[simp]

theorem yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) (X✝ : Cᵒᵖ) (a✝ : ↑(F.1 X✝)) : (MonCat.Hom.hom ((yonedaMonObjIsoOfRepresentableBy X F α).inv.app X✝)) a✝ = α.homEquiv.symm a✝

@[simp]

theorem yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) (X✝ : Cᵒᵖ) (a✝ : Opposite.unop X✝ ⟶ X) : (MonCat.Hom.hom ((yonedaMonObjIsoOfRepresentableBy X F α).hom.app X✝)) a✝ = α.homEquiv a✝

def yonedaMon {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Functor (Mon C) (CategoryTheory.Functor Cᵒᵖ MonCat)

The yoneda embedding of Mon_C into presheaves of monoids.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem yonedaMon_obj {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : Mon C) : yonedaMon.obj M = yonedaMonObj M.X

@[simp]

theorem yonedaMon_map_app {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : Mon C} (ψ : M ⟶ N) (Y : Cᵒᵖ) : (yonedaMon.map ψ).app Y = MonCat.ofHom { toFun := fun (x : Opposite.unop Y ⟶ M.X) => CategoryTheory.CategoryStruct.comp x ψ.hom, map_one' := ⋯, map_mul' := ⋯ }

theorem yonedaMon_naturality {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X Y : C} [MonObj M] [MonObj N] (α : yonedaMonObj M ⟶ yonedaMonObj N) (f : X ⟶ Y) (g : Y ⟶ M) : (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g)

theorem yonedaMon_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X Y : C} [MonObj M] [MonObj N] (α : yonedaMonObj M ⟶ yonedaMonObj N) (f : X ⟶ Y) (g : Y ⟶ M) {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)

def yonedaMonObjRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : ((yonedaMonObj M).comp (CategoryTheory.forget MonCat)).RepresentableBy M

If M is a monoid object, then Hom(-, M) as a presheaf of monoids is represented by M.

Equations

• yonedaMonObjRepresentableBy M = CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj M))

theorem MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

@[deprecated MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy (since := "2025-09-09")]

theorem Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : MonObj.ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

Alias of MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy.

@[deprecated MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy (since := "2025-03-07")]

theorem MonObjOfRepresentableBy_yonedaMonObjRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : MonObj.ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

Alias of MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy.

@[deprecated MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy (since := "2025-09-09")]

theorem Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : MonObj.ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

Alias of MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy.

def yonedaMonFullyFaithful {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaMon.FullyFaithful

The yoneda embedding for Mon_C is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance instFullMonFunctorOppositeMonCatYonedaMon {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaMon.Full

instance instFaithfulMonFunctorOppositeMonCatYonedaMon {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaMon.Faithful

theorem essImage_yonedaMon {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaMon.essImage = (fun (x : CategoryTheory.Functor Cᵒᵖ MonCat) => x.comp (CategoryTheory.forget MonCat)) ⁻¹' setOf CategoryTheory.Functor.IsRepresentable

@[simp]

theorem MonObj.one_comp {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f : M ⟶ N) [IsMonHom f] : CategoryTheory.CategoryStruct.comp 1 f = 1

@[simp]

theorem MonObj.one_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f : M ⟶ N) [IsMonHom f] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp 1 (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 1 h

@[deprecated MonObj.one_comp (since := "2025-09-09")]

theorem Mon_Class.one_comp {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f : M ⟶ N) [IsMonHom f] : CategoryTheory.CategoryStruct.comp 1 f = 1

Alias of MonObj.one_comp.

theorem MonObj.mul_comp {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsMonHom g] : CategoryTheory.CategoryStruct.comp (f₁ * f₂) g = CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g

theorem MonObj.mul_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsMonHom g] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (f₁ * f₂) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g) h

@[deprecated MonObj.mul_comp (since := "2025-09-09")]

theorem Mon_Class.mul_comp {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsMonHom g] : CategoryTheory.CategoryStruct.comp (f₁ * f₂) g = CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g

Alias of MonObj.mul_comp.

theorem MonObj.pow_comp {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsMonHom g] : CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n

theorem MonObj.pow_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsMonHom g] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (f ^ n) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h

@[deprecated MonObj.pow_comp (since := "2025-09-09")]

theorem Mon_Class.pow_comp {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [MonObj M] [MonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsMonHom g] : CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n

Alias of MonObj.pow_comp.

@[simp]

theorem MonObj.comp_one {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f 1 = 1

@[simp]

theorem MonObj.comp_one_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ Y) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp 1 h) = CategoryTheory.CategoryStruct.comp 1 h

@[deprecated MonObj.comp_one (since := "2025-09-09")]

theorem Mon_Class.comp_one {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f 1 = 1

Alias of MonObj.comp_one.

theorem MonObj.comp_mul {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) : CategoryTheory.CategoryStruct.comp f (g₁ * g₂) = CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂

theorem MonObj.comp_mul_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g₁ * g₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂) h

@[deprecated MonObj.comp_mul (since := "2025-09-09")]

theorem Mon_Class.comp_mul {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) : CategoryTheory.CategoryStruct.comp f (g₁ * g₂) = CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂

Alias of MonObj.comp_mul.

theorem MonObj.comp_pow {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) : CategoryTheory.CategoryStruct.comp h (f ^ n) = CategoryTheory.CategoryStruct.comp h f ^ n

theorem MonObj.comp_pow_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) {Z : C} (h✝ : M ⟶ Z) : CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp (f ^ n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f ^ n) h✝

@[deprecated MonObj.comp_pow (since := "2025-09-09")]

theorem Mon_Class.comp_pow {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) : CategoryTheory.CategoryStruct.comp h (f ^ n) = CategoryTheory.CategoryStruct.comp h f ^ n

Alias of MonObj.comp_pow.

theorem MonObj.one_eq_one {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : one = 1

@[deprecated MonObj.one_eq_one (since := "2025-09-09")]

theorem Mon_Class.one_eq_one {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : MonObj.one = 1

Alias of MonObj.one_eq_one.

theorem MonObj.mul_eq_mul {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : mul = CategoryTheory.CartesianMonoidalCategory.fst M M * CategoryTheory.CartesianMonoidalCategory.snd M M

@[deprecated MonObj.mul_eq_mul (since := "2025-09-09")]

theorem Mon_Class.mul_eq_mul {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] : MonObj.mul = CategoryTheory.CartesianMonoidalCategory.fst M M * CategoryTheory.CartesianMonoidalCategory.snd M M

Alias of MonObj.mul_eq_mul.

def Hom.mulEquivCongrRight {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] (X : C) : (X ⟶ M) ≃* (X ⟶ N)

If M and N are isomorphic as monoid objects, then X ⟶ M and X ⟶ N are isomorphic monoids.

Equations

• Hom.mulEquivCongrRight e X = ((yonedaMon.mapIso (Mon.mkIso' e)).app (Opposite.op X)).monCatIsoToMulEquiv

@[simp]

theorem Hom.mulEquivCongrRight_symm_apply {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] (X : C) (a : ↑((yonedaMon.obj { X := N, mon := inst✝ }).obj (Opposite.op X))) : (mulEquivCongrRight e X).symm a = CategoryTheory.CategoryStruct.comp a e.inv

@[simp]

theorem Hom.mulEquivCongrRight_apply {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] (X : C) (a : ↑((yonedaMon.obj { X := M, mon := inst✝ }).obj (Opposite.op X))) : (mulEquivCongrRight e X) a = CategoryTheory.CategoryStruct.comp a e.hom