Yoneda embedding of Mon_ C

We show that monoid objects 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.

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

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

@[reducible]

def monoidOfMon_Class {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [Mon_Class X] (Y : C) : Monoid (Y ⟶ X)

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

Equations

• monoidOfMon_Class X Y = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

def yonedaMonObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [Mon_Class X] : CategoryTheory.Functor Cᵒᵖ MonCat

If X is a monoid object, then Hom(-, X) 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [Mon_Class X] (Y : Cᵒᵖ) : ↑((yonedaMonObj X).obj Y) = (Opposite.unop Y ⟶ X)

@[simp]

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

def yonedaMonObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [Mon_Class X] : ((yonedaMonObj X).comp (CategoryTheory.forget MonCat)).RepresentableBy X

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

Equations

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

theorem Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [Mon_Class X] : Mon_ClassOfRepresentableBy X (yonedaMonObj X) (yonedaMonObjRepresentableBy X) = inst✝

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

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

@[simp]

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

@[simp]

theorem yonedaMonObjMon_ClassOfRepresentableBy_hom_app_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts 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 ((yonedaMonObjMon_ClassOfRepresentableBy X F α).hom.app X✝)) a✝ = α.homEquiv a✝

def yonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts 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_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ X₂ : Mon_ C} (ψ : X₁ ⟶ X₂) (Y : Cᵒᵖ) : (yonedaMon.map ψ).app Y = MonCat.ofHom { toFun := fun (x : Opposite.unop Y ⟶ X₁.X) => CategoryTheory.CategoryStruct.comp x ψ.hom, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem yonedaMon_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : Mon_ C) : yonedaMon.obj X = yonedaMonObj X.X

theorem yonedaMon_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ X₂ : C} [Mon_Class X₁] [Mon_Class X₂] (α : yonedaMonObj X₁ ⟶ yonedaMonObj X₂) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) (g : Y₂ ⟶ X₁) : (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y₁))) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y₂))) g)

theorem yonedaMon_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ X₂ : C} [Mon_Class X₁] [Mon_Class X₂] (α : yonedaMonObj X₁ ⟶ yonedaMonObj X₂) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) (g : Y₂ ⟶ X₁) {Z : C} (h : X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y₁))) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y₂))) g) h)

def yonedaMonFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts 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 instFullMon_FunctorOppositeMonCatYonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] : yonedaMon.Full

instance instFaithfulMon_FunctorOppositeMonCatYonedaMon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] : yonedaMon.Faithful

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