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.

@[implicit_reducible]

instance CategoryTheory.Mon.uniqueHomToTrivial {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] (A : Mon D) : Unique (A ⟶ trivial D)

Equations

• A.uniqueHomToTrivial = { default := { hom := CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X, isMonHom_hom := ⋯ }, uniq := ⋯ }

@[implicit_reducible]

instance CategoryTheory.AddMon.uniqueHomToTrivial {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] (A : AddMon D) : Unique (A ⟶ trivial D)

Equations

• A.uniqueHomToTrivial = { default := { hom := CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X, isAddMonHom_hom := ⋯ }, uniq := ⋯ }

@[simp]

theorem CategoryTheory.AddMon.uniqueHomToTrivial_default_hom {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] (A : AddMon D) : default.hom = SemiCartesianMonoidalCategory.toUnit A.X

@[simp]

theorem CategoryTheory.Mon.uniqueHomToTrivial_default_hom {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] (A : Mon D) : default.hom = SemiCartesianMonoidalCategory.toUnit A.X

@[deprecated CategoryTheory.Mon.uniqueHomToTrivial (since := "2026-03-20")]

def CategoryTheory.uniqueHomToTrivial {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] (A : Mon D) : Unique (A ⟶ Mon.trivial D)

Alias of CategoryTheory.Mon.uniqueHomToTrivial.

Equations

• @CategoryTheory.uniqueHomToTrivial = @CategoryTheory.Mon.uniqueHomToTrivial

instance CategoryTheory.instHasZeroObjectMon {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] : Limits.HasZeroObject (Mon D)

instance CategoryTheory.instHasZeroObjectAddMon {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] : Limits.HasZeroObject (AddMon D)

@[implicit_reducible]

noncomputable instance CategoryTheory.instHasZeroMorphismsMon {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] : Limits.HasZeroMorphisms (Mon D)

Equations

• CategoryTheory.instHasZeroMorphismsMon = CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject

@[implicit_reducible]

noncomputable instance CategoryTheory.instHasZeroMorphismsAddMon {D : Type u_1} [Category.{v_1, u_1} D] [SemiCartesianMonoidalCategory D] : Limits.HasZeroMorphisms (AddMon D)

Equations

• CategoryTheory.instHasZeroMorphismsAddMon = CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject

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

instance CategoryTheory.AddMonObj.instIsAddMonHomToAddUnit {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] : IsAddMonHom (SemiCartesianMonoidalCategory.toUnit M)

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

instance CategoryTheory.AddMonObj.instIsAddMonHomZero {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] : IsAddMonHom zero

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.AddMonObj.lift_comp_zero_left {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {A B : C} [AddMonObj B] (f : A ⟶ MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp f zero) g) add = g

@[simp]

theorem CategoryTheory.AddMonObj.lift_comp_zero_left_assoc {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {A B : C} [AddMonObj B] (f : A ⟶ MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp f zero) g) (CategoryStruct.comp add h) = CategoryStruct.comp g h

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.AddMonObj.lift_comp_zero_right {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {A B : C} [AddMonObj B] (f : A ⟶ B) (g : A ⟶ MonoidalCategoryStruct.tensorUnit C) : CategoryStruct.comp (CartesianMonoidalCategory.lift f (CategoryStruct.comp g zero)) add = f

@[simp]

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

@[simp]

theorem CategoryTheory.AddMonObj.lift_comp_zero_right_assoc {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {A B : C} [AddMonObj B] (f : A ⟶ B) (g : A ⟶ MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift f (CategoryStruct.comp g zero)) (CategoryStruct.comp add h) = CategoryStruct.comp f h

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

instance CategoryTheory.AddMonObj.instIsAddMonHomFst {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] [BraidedCategory C] : IsAddMonHom (SemiCartesianMonoidalCategory.fst M N)

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

instance CategoryTheory.AddMonObj.instIsAddMonHomSnd {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] [BraidedCategory C] : IsAddMonHom (SemiCartesianMonoidalCategory.snd M N)

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

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

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

instance CategoryTheory.AddMonObj.instIsAddMonHomAddOfIsCommAddMonObj {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] : IsAddMonHom add

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Comm monoid objects are internal monoid objects

@[implicit_reducible]

instance CategoryTheory.Mon.instMonObjOfIsCommMonObjX {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M : Mon C} [IsCommMonObj M.X] : MonObj M

A commutative monoid object is a monoid object in the category of monoid objects.

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.instAddMonObjOfIsCommAddMonObjX {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M : AddMon C} [IsCommAddMonObj M.X] : AddMonObj M

A commutative additive monoid object is an additive monoid object in the category of additive monoid objects.

Equations

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

@[simp]

theorem CategoryTheory.Mon.hom_one {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] (M : Mon C) [IsCommMonObj M.X] : MonObj.one.hom = MonObj.one

@[simp]

theorem CategoryTheory.AddMon.hom_zero {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] (M : AddMon C) [IsCommAddMonObj M.X] : AddMonObj.zero.hom = AddMonObj.zero

@[simp]

theorem CategoryTheory.Mon.hom_mul {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] (M : Mon C) [IsCommMonObj M.X] : MonObj.mul.hom = MonObj.mul

@[simp]

theorem CategoryTheory.AddMon.hom_add {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] (M : AddMon C) [IsCommAddMonObj M.X] : AddMonObj.add.hom = AddMonObj.add

instance CategoryTheory.Mon.instIsCommMonObj {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M : Mon C} [IsCommMonObj M.X] : IsCommMonObj M

A commutative monoid object is a commutative monoid object in the category of monoid objects.

instance CategoryTheory.AddMon.instIsCommAddMonObj {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M : AddMon C} [IsCommAddMonObj M.X] : IsCommAddMonObj M

A commutative additive monoid object is a commutative additive monoid object in the category of additive monoid objects.

@[implicit_reducible]

def CategoryTheory.MonObj.ofRepresentableBy {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ MonCat) (α : (F.comp (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.

@[implicit_reducible]

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.AddMonObj.ofRepresentableBy_add {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ AddMonCat) (α : (F.comp (forget AddMonCat)).RepresentableBy X) : add = α.homEquiv.symm (α.homEquiv (SemiCartesianMonoidalCategory.fst X X) + α.homEquiv (SemiCartesianMonoidalCategory.snd X X))

@[simp]

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

@[simp]

theorem CategoryTheory.AddMonObj.ofRepresentableBy_zero {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ AddMonCat) (α : (F.comp (forget AddMonCat)).RepresentableBy X) : zero = α.homEquiv.symm 0

@[reducible, inline]

abbrev CategoryTheory.Hom.monoid {C : Type u_1} [Category.{v, u_1} C] [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.

@[reducible, inline]

abbrev CategoryTheory.Hom.addMonoid {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M X : C} [AddMonObj M] : AddMonoid (X ⟶ M)

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

Equations

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

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

theorem CategoryTheory.Hom.zero_def {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M X : C} [AddMonObj M] : 0 = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit X) AddMonObj.zero

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

theorem CategoryTheory.Hom.add_def {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M X : C} [AddMonObj M] (f₁ f₂ : X ⟶ M) : f₁ + f₂ = CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) AddMonObj.add

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

theorem CategoryTheory.Functor.map_add' {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} [AddMonObj 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

@[simp]

theorem CategoryTheory.Functor.map_zero' {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} [AddMonObj M] (F : Functor C D) [F.Monoidal] : F.map 0 = 0

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' := ⋯ }

def CategoryTheory.Functor.homAddMonoidHom {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} [AddMonObj M] (F : Functor C D) [F.Monoidal] : (X ⟶ M) →+ (F.obj X ⟶ F.obj M)

Functor.map of a monoidal functor as a AddMonoidHom.

Equations

• F.homAddMonoidHom = { toFun := F.map, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.homAddMonoidHom_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} [AddMonObj M] (F : Functor C D) [F.Monoidal] (a✝ : X ⟶ M) : F.homAddMonoidHom a✝ = F.map a✝

@[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' := ⋯ }

def CategoryTheory.Functor.FullyFaithful.homAddEquiv {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} [AddMonObj 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 AddEquiv.

Equations

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

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homAddEquiv_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} [AddMonObj M] (F : Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (a✝ : X ⟶ M) : (homAddEquiv 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

@[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.homAddEquiv_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} [AddMonObj M] (F : Functor C D) [F.Monoidal] (hF : F.FullyFaithful) (f : F.obj X ⟶ F.obj M) : (homAddEquiv F hF).symm f = hF.preimage f

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Hom.addCommMonoid {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M X : C} [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] : AddCommMonoid (X ⟶ M)

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

Equations

• CategoryTheory.Hom.addCommMonoid = { toAddMonoid := CategoryTheory.Hom.addMonoid, add_comm := ⋯ }

@[simp]

theorem CategoryTheory.Mon.Hom.hom_one {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M N : Mon C} [IsCommMonObj N.X] : hom 1 = 1

@[simp]

theorem CategoryTheory.AddMon.Hom.hom_zero {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M N : AddMon C} [IsCommAddMonObj N.X] : hom 0 = 0

@[simp]

theorem CategoryTheory.Mon.Hom.hom_mul {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M N : Mon C} [IsCommMonObj N.X] (f g : M ⟶ N) : (f * g).hom = f.hom * g.hom

@[simp]

theorem CategoryTheory.AddMon.Hom.hom_add {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M N : AddMon C} [IsCommAddMonObj N.X] (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom

@[simp]

theorem CategoryTheory.Mon.Hom.hom_pow {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M N : Mon C} [IsCommMonObj N.X] (f : M ⟶ N) (n : ℕ) : (f ^ n).hom = f.hom ^ n

@[simp]

theorem CategoryTheory.AddMon.Hom.hom_nsmul {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] [BraidedCategory C] {M N : AddMon C} [IsCommAddMonObj N.X] (f : M ⟶ N) (n : ℕ) : (n • f).hom = n • f.hom

def CategoryTheory.yonedaMonObj {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [MonObj M] : 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.

def CategoryTheory.yonedaAddMonObj {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] : Functor Cᵒᵖ AddMonCat

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.yonedaAddMonObj_map {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] {X Y₂ : Cᵒᵖ} (φ : X ⟶ Y₂) : (yonedaAddMonObj M).map φ = AddMonCat.ofHom { toFun := fun (x : Opposite.unop X ⟶ M) => CategoryStruct.comp φ.unop x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.yonedaMonObjIsoOfRepresentableBy {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ MonCat) (α : (F.comp (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

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ MonCat) (α : (F.comp (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 CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy_hom_app_hom_apply {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ AddMonCat) (α : (F.comp (forget AddMonCat)).RepresentableBy X) (X✝ : Cᵒᵖ) (a✝ : Opposite.unop X✝ ⟶ X) : ((yonedaAddMonObjIsoOfRepresentableBy X F α).hom.app X✝).hom' a✝ = α.homEquiv a✝

@[simp]

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

@[simp]

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

def CategoryTheory.yonedaMon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] : Functor (Mon C) (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.

def CategoryTheory.yonedaAddMon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] : Functor (AddMon C) (Functor Cᵒᵖ AddMonCat)

The yoneda embedding of AddMon C into presheaves of additive monoids.

Equations

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

@[simp]

theorem CategoryTheory.yonedaAddMon_obj {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : AddMon C) : yonedaAddMon.obj M = yonedaAddMonObj M.X

@[simp]

theorem CategoryTheory.yonedaAddMon_map_app {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N : AddMon C} (ψ : M ⟶ N) (Y : Cᵒᵖ) : (yonedaAddMon.map ψ).app Y = AddMonCat.ofHom { toFun := fun (x : Opposite.unop Y ⟶ M.X) => CategoryStruct.comp x ψ.hom, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

theorem CategoryTheory.yonedaMon_naturality_assoc {C : Type u_1} [Category.{v, u_1} C] [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) : CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g)) h = CategoryStruct.comp f (CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)

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

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

Equations

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

def CategoryTheory.yonedaAddMonObjRepresentableBy {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] : ((yonedaAddMonObj M).comp (forget AddMonCat)).RepresentableBy M

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

Equations

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

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

theorem CategoryTheory.AddMonObj.ofRepresentableBy_yonedaAddMonObjRepresentableBy {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] : ofRepresentableBy M (yonedaAddMonObj M) (yonedaAddMonObjRepresentableBy M) = inst✝

def CategoryTheory.yonedaMonFullyFaithful {C : Type u_1} [Category.{v, u_1} C] [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.

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

The yoneda embedding for AddMon C is fully faithful.

Equations

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

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

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

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

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

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

theorem CategoryTheory.essImage_yonedaAddMon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] : yonedaAddMon.essImage = fun (F : Functor Cᵒᵖ AddMonCat) => (F.comp (forget AddMonCat)).IsRepresentable

@[simp]

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

@[simp]

theorem CategoryTheory.AddMonObj.zero_comp {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N X : C} [AddMonObj M] [AddMonObj N] (f : M ⟶ N) [IsAddMonHom f] : CategoryStruct.comp 0 f = 0

@[simp]

theorem CategoryTheory.AddMonObj.zero_comp_assoc {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N X : C} [AddMonObj M] [AddMonObj N] (f : M ⟶ N) [IsAddMonHom f] {Z : C} (h : N ⟶ Z) : CategoryStruct.comp 0 (CategoryStruct.comp f h) = CategoryStruct.comp 0 h

@[simp]

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

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

theorem CategoryTheory.AddMonObj.add_comp {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N X : C} [AddMonObj M] [AddMonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsAddMonHom g] : CategoryStruct.comp (f₁ + f₂) g = CategoryStruct.comp f₁ g + CategoryStruct.comp f₂ g

theorem CategoryTheory.AddMonObj.add_comp_assoc {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N X : C} [AddMonObj M] [AddMonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsAddMonHom g] {Z : C} (h : N ⟶ Z) : CategoryStruct.comp (f₁ + f₂) (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f₁ g + CategoryStruct.comp f₂ g) h

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

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

theorem CategoryTheory.AddMonObj.nsmul_comp {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N X : C} [AddMonObj M] [AddMonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsAddMonHom g] : CategoryStruct.comp (n • f) g = n • CategoryStruct.comp f g

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

theorem CategoryTheory.AddMonObj.nsmul_comp_assoc {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N X : C} [AddMonObj M] [AddMonObj N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsAddMonHom g] {Z : C} (h : N ⟶ Z) : CategoryStruct.comp (n • f) (CategoryStruct.comp g h) = CategoryStruct.comp (n • CategoryStruct.comp f g) h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.AddMonObj.zero_eq_zero {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] : zero = 0

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

theorem CategoryTheory.AddMonObj.add_eq_add {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] : add = SemiCartesianMonoidalCategory.fst M M + SemiCartesianMonoidalCategory.snd M M

def CategoryTheory.Hom.mulEquivCongrRight {C : Type u_1} [Category.{v, u_1} C] [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

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

def CategoryTheory.Hom.addEquivCongrRight {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (e : M ≅ N) [IsAddMonHom e.hom] (X : C) : (X ⟶ M) ≃+ (X ⟶ N)

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

Equations

• CategoryTheory.Hom.addEquivCongrRight e X = ((CategoryTheory.yonedaAddMon.mapIso (CategoryTheory.AddMon.mkIso' e)).app (Opposite.op X)).addMonCatIsoToAddEquiv

@[simp]

theorem CategoryTheory.Hom.addEquivCongrRight_symm_apply {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (e : M ≅ N) [IsAddMonHom e.hom] (X : C) (a : ↑((yonedaAddMon.obj { X := N, addMon := inst✝ }).obj (Opposite.op X))) : (addEquivCongrRight e X).symm a = (AddMonCat.Hom.hom (AddMonCat.ofHom { toFun := fun (x : X ⟶ N) => CategoryStruct.comp x e.inv, map_zero' := ⋯, map_add' := ⋯ })) a

@[simp]

theorem CategoryTheory.Hom.addEquivCongrRight_apply {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (e : M ≅ N) [IsAddMonHom e.hom] (X : C) (a : ↑((yonedaAddMon.obj { X := M, addMon := inst✝ }).obj (Opposite.op X))) : (addEquivCongrRight e X) a = (AddMonCat.Hom.hom (AddMonCat.ofHom { toFun := fun (x : X ⟶ M) => CategoryStruct.comp x e.hom, map_zero' := ⋯, map_add' := ⋯ })) a

@[simp]

theorem CategoryTheory.Hom.mulEquivCongrRight_apply {C : Type u_1} [Category.{v, u_1} C] [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 = (MonCat.Hom.hom (MonCat.ofHom { toFun := fun (x : X ⟶ M) => CategoryStruct.comp x e.hom, map_one' := ⋯, map_mul' := ⋯ })) a

@[simp]

theorem CategoryTheory.Hom.mulEquivCongrRight_symm_apply {C : Type u_1} [Category.{v, u_1} C] [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 = (MonCat.Hom.hom (MonCat.ofHom { toFun := fun (x : X ⟶ N) => CategoryStruct.comp x e.inv, map_one' := ⋯, map_mul' := ⋯ })) a

theorem CategoryTheory.isCommMonObj_iff_isMulCommutative {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] : IsCommMonObj M ↔ ∀ (X : C), IsMulCommutative (X ⟶ M)

A monoid object M is commutative if and only if X ⟶ M is commutative for all X.

theorem CategoryTheory.isCommAddMonObj_iff_isAddCommutative {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] : IsCommAddMonObj M ↔ ∀ (X : C), IsAddCommutative (X ⟶ M)