Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_

Additional results about monoid objects in cartesian monoidal categories #

source
theorem Mon_.lift_lift_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A : C} {B : Mon_ C} (f g h : A ⟶ B.X) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f g) B.mul) h) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift g h) B.mul)) B.mul
source
@[simp]
theorem Mon_.lift_comp_one_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A : C} {B : Mon_ C} (f : A ⟶ 𝟙_ C) (g : A ⟶ B.X) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.comp f B.one) g) B.mul = g
source
@[simp]
theorem Mon_.lift_comp_one_left_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A : C} {B : Mon_ C} (f : A ⟶ 𝟙_ C) (g : A ⟶ B.X) {Z : C} (h : B.X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.comp f B.one) g) (CategoryTheory.CategoryStruct.comp B.mul h) = CategoryTheory.CategoryStruct.comp g h
source
@[simp]
theorem Mon_.lift_comp_one_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A : C} {B : Mon_ C} (f : A ⟶ B.X) (g : A ⟶ 𝟙_ C) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f (CategoryTheory.CategoryStruct.comp g B.one)) B.mul = f
source
@[simp]
theorem Mon_.lift_comp_one_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A : C} {B : Mon_ C} (f : A ⟶ B.X) (g : A ⟶ 𝟙_ C) {Z : C} (h : B.X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f (CategoryTheory.CategoryStruct.comp g B.one)) (CategoryTheory.CategoryStruct.comp B.mul h) = CategoryTheory.CategoryStruct.comp f h