The Yoneda embedding for monoid objects for locally small categories

Let C be a locally w-small category. We define the Yoneda embedding shrinkYonedaMon : Mon C ⥤ Cᵒᵖ ⥤ MonCat.{w} w and its Grp analogue.

instance CategoryTheory.instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : Cᵒᵖ) : Small.{w, v} ↑((yonedaMon.obj M).obj X)

instance CategoryTheory.instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] (M : Grp C) (X : Cᵒᵖ) : Small.{w, v} ↑((yonedaGrp.obj M).obj X)

noncomputable def CategoryTheory.shrinkYonedaMon {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] : Functor (Mon C) (Functor Cᵒᵖ MonCat)

The Yoneda embedding Mon C ⥤ Cᵒᵖ ⥤ MonCat.{w} for a locally w-small category C.

Equations

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

theorem CategoryTheory.shrinkYonedaMon_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] (X : Mon C) : shrinkYonedaMon.{w, v, u}.obj X = MonCat.shrinkFunctor.{w, v, v, u} (yonedaMon.obj X)

theorem CategoryTheory.shrinkYonedaMon_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {X✝ Y✝ : Mon C} (f : X✝ ⟶ Y✝) : shrinkYonedaMon.{w, v, u}.map f = MonCat.shrinkFunctorMap (yonedaMon.map f)

noncomputable def CategoryTheory.shrinkYonedaMonObjObjEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M : Mon C} {Y : Cᵒᵖ} : ↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y) ≃* (Opposite.unop Y ⟶ M.X)

The type (shrinkYonedaMon.obj M).obj Y is equivalent to Y.unop ⟶ M.X.

Equations

• CategoryTheory.shrinkYonedaMonObjObjEquiv = Shrink.mulEquiv

theorem CategoryTheory.shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M : Mon C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Opposite.unop Y ⟶ M.X) : (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.obj M).map g)) (shrinkYonedaMonObjObjEquiv.symm f) = shrinkYonedaMonObjObjEquiv.symm (CategoryStruct.comp g.unop f)

theorem CategoryTheory.shrinkYonedaMonObjObjEquiv_symm_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M : Mon C} {Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ M.X) : shrinkYonedaMonObjObjEquiv.symm (CategoryStruct.comp g f) = (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.obj M).map g.op)) (shrinkYonedaMonObjObjEquiv.symm f)

theorem CategoryTheory.shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M M' : Mon C} {Y : Cᵒᵖ} (f : Opposite.unop Y ⟶ M.X) (g : M ⟶ M') : (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.map g).app Y)) (shrinkYonedaMonObjObjEquiv.symm f) = shrinkYonedaMonObjObjEquiv.symm (CategoryStruct.comp f g.hom)

noncomputable def CategoryTheory.shrinkYonedaGrp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] : Functor (Grp C) (Functor Cᵒᵖ GrpCat)

The Yoneda embedding Grp C ⥤ Cᵒᵖ ⥤ GrpCat.{w} for a locally w-small category C.

Equations

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

theorem CategoryTheory.shrinkYonedaGrp_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {X✝ Y✝ : Grp C} (f : X✝ ⟶ Y✝) : shrinkYonedaGrp.{w, v, u}.map f = GrpCat.shrinkFunctorMap (yonedaGrp.map f)

theorem CategoryTheory.shrinkYonedaGrp_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] (X : Grp C) : shrinkYonedaGrp.{w, v, u}.obj X = GrpCat.shrinkFunctor.{w, v, v, u} (yonedaGrp.obj X)

noncomputable def CategoryTheory.shrinkYonedaGrpObjObjEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M : Grp C} {Y : Cᵒᵖ} : ↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y) ≃* (Opposite.unop Y ⟶ M.X)

The type (shrinkYonedaGrp.obj M).obj Y is equivalent to Y.unop ⟶ M.X.

Equations

• CategoryTheory.shrinkYonedaGrpObjObjEquiv = Shrink.mulEquiv

theorem CategoryTheory.shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M : Grp C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Opposite.unop Y ⟶ M.X) : (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.obj M).map g)) (shrinkYonedaGrpObjObjEquiv.symm f) = shrinkYonedaGrpObjObjEquiv.symm (CategoryStruct.comp g.unop f)

theorem CategoryTheory.shrinkYonedaGrpObjObjEquiv_symm_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M : Grp C} {Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ M.X) : shrinkYonedaGrpObjObjEquiv.symm (CategoryStruct.comp g f) = (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.obj M).map g.op)) (shrinkYonedaGrpObjObjEquiv.symm f)

theorem CategoryTheory.shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [CartesianMonoidalCategory C] {M M' : Grp C} {Y : Cᵒᵖ} (f : Opposite.unop Y ⟶ M.X) (g : M ⟶ M') : (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.map g).app Y)) (shrinkYonedaGrpObjObjEquiv.symm f) = shrinkYonedaGrpObjObjEquiv.symm (CategoryStruct.comp f g.hom.hom)