Yoneda embeddings

This file defines a few Yoneda embeddings for the category of commutative monoids.

def CommMonCat.coyoneda : CategoryTheory.Functor CommMonCatᵒᵖ (CategoryTheory.Functor CommMonCat CommMonCat)

The CommMonCat-valued coyoneda embedding.

def AddCommMonCat.coyoneda : CategoryTheory.Functor AddCommMonCatᵒᵖ (CategoryTheory.Functor AddCommMonCat AddCommMonCat)

The AddCommMonCat-valued coyoneda embedding.

@[simp]

theorem AddCommMonCat.coyoneda_obj_map (M : AddCommMonCatᵒᵖ) {X✝ Y✝ : AddCommMonCat} (f : X✝ ⟶ Y✝) : (coyoneda.obj M).map f = ofHom (AddMonoidHom.compHom (Hom.hom f))

@[simp]

theorem AddCommMonCat.coyoneda_obj_obj_coe (M : AddCommMonCatᵒᵖ) (N : AddCommMonCat) : ↑((coyoneda.obj M).obj N) = (↑(Opposite.unop M) →+ ↑N)

@[simp]

theorem CommMonCat.coyoneda_map_app {X✝ Y✝ : CommMonCatᵒᵖ} (f : X✝ ⟶ Y✝) (N : CommMonCat) : (coyoneda.map f).app N = ofHom (Hom.hom f.unop).compHom'

@[simp]

theorem AddCommMonCat.coyoneda_map_app {X✝ Y✝ : AddCommMonCatᵒᵖ} (f : X✝ ⟶ Y✝) (N : AddCommMonCat) : (coyoneda.map f).app N = ofHom (Hom.hom f.unop).compHom'

@[simp]

theorem CommMonCat.coyoneda_obj_map (M : CommMonCatᵒᵖ) {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : (coyoneda.obj M).map f = ofHom (MonoidHom.compHom (Hom.hom f))

@[simp]

theorem CommMonCat.coyoneda_obj_obj_coe (M : CommMonCatᵒᵖ) (N : CommMonCat) : ↑((coyoneda.obj M).obj N) = (↑(Opposite.unop M) →* ↑N)

def CommMonCat.coyonedaForget : coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommMonCat CommMonCat (Type u_1)).obj (CategoryTheory.forget CommMonCat)) ≅ CategoryTheory.coyoneda

The CommMonCat-valued coyoneda embedding composed with the forgetful functor is the usual coyoneda embedding.

def AddCommMonCat.coyonedaForget : coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommMonCat AddCommMonCat (Type u_1)).obj (CategoryTheory.forget AddCommMonCat)) ≅ CategoryTheory.coyoneda

The AddCommMonCat-valued coyoneda embedding composed with the forgetful functor is the usual coyoneda embedding.

@[simp]

theorem CommMonCat.coyonedaForget_hom_app_app_hom (X : CommMonCatᵒᵖ) (X✝ : CommMonCat) (a✝ : ((coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommMonCat CommMonCat (Type u_1)).obj (CategoryTheory.forget CommMonCat))).obj X).obj X✝) : Hom.hom ((coyonedaForget.hom.app X).app X✝ a✝) = a✝

@[simp]

theorem AddCommMonCat.coyonedaForget_inv_app_app (X : AddCommMonCatᵒᵖ) (X✝ : AddCommMonCat) (a✝ : (CategoryTheory.coyoneda.obj X).obj X✝) : (coyonedaForget.inv.app X).app X✝ a✝ = Hom.hom a✝

@[simp]

theorem AddCommMonCat.coyonedaForget_hom_app_app_hom (X : AddCommMonCatᵒᵖ) (X✝ : AddCommMonCat) (a✝ : ((coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommMonCat AddCommMonCat (Type u_1)).obj (CategoryTheory.forget AddCommMonCat))).obj X).obj X✝) : Hom.hom ((coyonedaForget.hom.app X).app X✝ a✝) = a✝

@[simp]

theorem CommMonCat.coyonedaForget_inv_app_app (X : CommMonCatᵒᵖ) (X✝ : CommMonCat) (a✝ : (CategoryTheory.coyoneda.obj X).obj X✝) : (coyonedaForget.inv.app X).app X✝ a✝ = Hom.hom a✝

def CommMonCat.coyonedaType : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor CommMonCat CommMonCat)

The Hom bifunctor sending a type X and a commutative monoid M to the commutative monoid X → M with pointwise operations.

This is also the coyoneda embedding of Type into CommMonCat-valued presheaves of commutative monoids.

def AddCommMonCat.coyonedaType : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor AddCommMonCat AddCommMonCat)

The Hom bifunctor sending a type X and a commutative monoid M to the commutative monoid X → M with pointwise operations.

This is also the coyoneda embedding of Type into AddCommMonCat-valued presheaves of commutative monoids.

@[simp]

theorem CommMonCat.coyonedaType_map_app {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (N : CommMonCat) : (coyonedaType.map f).app N = ofHom (Pi.monoidHom fun (i : Opposite.unop Y✝) => Pi.evalMonoidHom (fun (a : Opposite.unop X✝) => ↑N) (f.unop i))

@[simp]

theorem CommMonCat.coyonedaType_obj_map (X : Type uᵒᵖ) {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : (coyonedaType.obj X).map f = ofHom (Pi.monoidHom fun (i : Opposite.unop X) => (Hom.hom f).comp (Pi.evalMonoidHom (fun (a : Opposite.unop X) => ↑X✝) i))

@[simp]

theorem AddCommMonCat.coyonedaType_map_app {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (N : AddCommMonCat) : (coyonedaType.map f).app N = ofHom (Pi.addMonoidHom fun (i : Opposite.unop Y✝) => Pi.evalAddMonoidHom (fun (a : Opposite.unop X✝) => ↑N) (f.unop i))

@[simp]

theorem CommMonCat.coyonedaType_obj_obj_coe (X : Type uᵒᵖ) (M : CommMonCat) : ↑((coyonedaType.obj X).obj M) = (Opposite.unop X → ↑M)

@[simp]

theorem AddCommMonCat.coyonedaType_obj_map (X : Type uᵒᵖ) {X✝ Y✝ : AddCommMonCat} (f : X✝ ⟶ Y✝) : (coyonedaType.obj X).map f = ofHom (Pi.addMonoidHom fun (i : Opposite.unop X) => (Hom.hom f).comp (Pi.evalAddMonoidHom (fun (a : Opposite.unop X) => ↑X✝) i))

@[simp]

theorem AddCommMonCat.coyonedaType_obj_obj_coe (X : Type uᵒᵖ) (M : AddCommMonCat) : ↑((coyonedaType.obj X).obj M) = (Opposite.unop X → ↑M)