Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_

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.

source
theorem Mon_Class.lift_lift_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [Mon_Class 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
source
@[simp]
theorem Mon_Class.lift_comp_one_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [Mon_Class B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f one) g) mul = g
source
@[simp]
theorem Mon_Class.lift_comp_one_left_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [Mon_Class 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
source
@[simp]
theorem Mon_Class.lift_comp_one_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [Mon_Class B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g one)) mul = f
source
@[simp]
theorem Mon_Class.lift_comp_one_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [Mon_Class 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
source
def Mon_Class.ofRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) :
Mon_Class X

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

Equations
    Instances For
      source
      @[simp]
      theorem Mon_Class.ofRepresentableBy_mul {C : Type u} [CategoryTheory.Category.{v, u} 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))
      source
      @[simp]
      theorem Mon_Class.ofRepresentableBy_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) :
      one = α.homEquiv.symm 1
      source
      @[deprecated Mon_Class.ofRepresentableBy (since := "2025-03-07")]
      def Mon_ClassOfRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) :
      Mon_Class X

      Alias of Mon_Class.ofRepresentableBy.

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

      Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Hom.monoid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [Mon_Class M] :
          Monoid (X ⟶ M)

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

          Equations
            Instances For
              source
              theorem Hom.one_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [Mon_Class M] :
              1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) Mon_Class.one
              source
              theorem Hom.mul_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [Mon_Class M] (f₁ f₂ : X ⟶ M) :
              f₁ * f₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) Mon_Class.mul
              source
              @[reducible, inline]
              abbrev Hom.commMonoid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [Mon_Class M] [CategoryTheory.BraidedCategory C] [IsCommMon M] :
              CommMonoid (X ⟶ M)

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

              Equations
                Instances For
                  source
                  def yonedaMonObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class M] :
                  CategoryTheory.Functor Cᵒᵖ MonCat

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem yonedaMonObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class 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' := ⋯ }
                      source
                      @[simp]
                      theorem yonedaMonObj_obj_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class M] (X : Cᵒᵖ) :
                      ↑((yonedaMonObj M).obj X) = (Opposite.unop X ⟶ M)
                      source
                      def yonedaMonObjIsoOfRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} 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
                        Instances For
                          source
                          @[simp]
                          theorem yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} 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✝
                          source
                          @[simp]
                          theorem yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} 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✝
                          source
                          def yonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
                          CategoryTheory.Functor (Mon_ C) (CategoryTheory.Functor Cᵒᵖ MonCat)

                          The yoneda embedding of Mon_C into presheaves of monoids.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem yonedaMon_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : Mon_ C) :
                              yonedaMon.obj M = yonedaMonObj M.X
                              source
                              @[simp]
                              theorem yonedaMon_map_app {C : Type u} [CategoryTheory.Category.{v, u} 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' := ⋯ }
                              source
                              theorem yonedaMon_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X Y : C} [Mon_Class M] [Mon_Class 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)
                              source
                              theorem yonedaMon_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X Y : C} [Mon_Class M] [Mon_Class 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)
                              source
                              def yonedaMonObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class 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
                                Instances For
                                  source
                                  theorem Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class M] :
                                  ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝
                                  source
                                  @[deprecated Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy (since := "2025-03-07")]
                                  theorem Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class M] :
                                  Mon_Class.ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

                                  Alias of Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy.

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

                                  The yoneda embedding for Mon_C is fully faithful.

                                  Equations
                                    Instances For
                                      source
                                      instance instFullMon_FunctorOppositeMonCatYonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
                                      yonedaMon.Full
                                      source
                                      instance instFaithfulMon_FunctorOppositeMonCatYonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
                                      yonedaMon.Faithful
                                      source
                                      theorem essImage_yonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
                                      yonedaMon.essImage = (fun (x : CategoryTheory.Functor Cᵒᵖ MonCat) => x.comp (CategoryTheory.forget MonCat)) ⁻¹' setOf CategoryTheory.Functor.IsRepresentable
                                      source
                                      @[simp]
                                      theorem Mon_Class.one_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [Mon_Class M] [Mon_Class N] (f : M ⟶ N) [IsMon_Hom f] :
                                      CategoryTheory.CategoryStruct.comp 1 f = 1
                                      source
                                      @[simp]
                                      theorem Mon_Class.one_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [Mon_Class M] [Mon_Class N] (f : M ⟶ N) [IsMon_Hom f] {Z : C} (h : N ⟶ Z) :
                                      CategoryTheory.CategoryStruct.comp 1 (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 1 h
                                      source
                                      theorem Mon_Class.mul_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [Mon_Class M] [Mon_Class N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsMon_Hom g] :
                                      CategoryTheory.CategoryStruct.comp (f₁ * f₂) g = CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g
                                      source
                                      theorem Mon_Class.mul_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [Mon_Class M] [Mon_Class N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsMon_Hom 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
                                      source
                                      theorem Mon_Class.pow_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [Mon_Class M] [Mon_Class N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsMon_Hom g] :
                                      CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n
                                      source
                                      theorem Mon_Class.pow_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M N X : C} [Mon_Class M] [Mon_Class N] (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsMon_Hom 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
                                      source
                                      @[simp]
                                      theorem Mon_Class.comp_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [Mon_Class M] (f : X ⟶ Y) :
                                      CategoryTheory.CategoryStruct.comp f 1 = 1
                                      source
                                      @[simp]
                                      theorem Mon_Class.comp_one_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [Mon_Class M] (f : X ⟶ Y) {Z : C} (h : M ⟶ Z) :
                                      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp 1 h) = CategoryTheory.CategoryStruct.comp 1 h
                                      source
                                      theorem Mon_Class.comp_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [Mon_Class M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) :
                                      CategoryTheory.CategoryStruct.comp f (g₁ * g₂) = CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂
                                      source
                                      theorem Mon_Class.comp_mul_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [Mon_Class 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
                                      source
                                      theorem Mon_Class.comp_pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [Mon_Class M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) :
                                      CategoryTheory.CategoryStruct.comp h (f ^ n) = CategoryTheory.CategoryStruct.comp h f ^ n
                                      source
                                      theorem Mon_Class.comp_pow_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {M X Y : C} [Mon_Class 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✝
                                      source
                                      theorem Mon_Class.one_eq_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class M] :
                                      one = 1
                                      source
                                      theorem Mon_Class.mul_eq_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [Mon_Class M] :
                                      mul = CategoryTheory.CartesianMonoidalCategory.fst M M * CategoryTheory.CartesianMonoidalCategory.snd M M