Documentation

def CategoryTheory.coyoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (Type v₁))

The co-Yoneda embedding, as a functor from Cᵒᵖ into co-presheaves on C.

Equations

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

@[simp]

theorem CategoryTheory.coyoneda_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) (Y : C) :

(CategoryTheory.coyoneda.obj X).obj Y = (Opposite.unop X ⟶ Y)

@[simp]

theorem CategoryTheory.coyoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (g : Opposite.unop X ⟶ X✝) :

(CategoryTheory.coyoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp g f

@[simp]

theorem CategoryTheory.coyoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (x✝ : C) (g : ((fun (X : Cᵒᵖ) => { obj := fun (Y : C) => Opposite.unop X ⟶ Y, map := fun {X_1 Y : C} (f : X_1 ⟶ Y) (g : (fun (Y : C) => Opposite.unop X ⟶ Y) X_1) => CategoryTheory.CategoryStruct.comp g f, map_id := ⋯, map_comp := ⋯ }) X✝).obj x✝) :

(CategoryTheory.coyoneda.map f).app x✝ g = CategoryTheory.CategoryStruct.comp f.unop g

theorem CategoryTheory.Yoneda.obj_map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Opposite.op X ⟶ Opposite.op Y) :

(CategoryTheory.yoneda.obj X).map f (CategoryTheory.CategoryStruct.id X) = (CategoryTheory.yoneda.map f.unop).app (Opposite.op Y) (CategoryTheory.CategoryStruct.id Y)

@[simp]

theorem CategoryTheory.Yoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) :

CategoryTheory.CategoryStruct.comp f (α.app (Opposite.op Z') h) = α.app (Opposite.op Z) (CategoryTheory.CategoryStruct.comp f h)

def CategoryTheory.Yoneda.fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.yoneda.FullyFaithful

The Yoneda embedding is fully faithful.

Equations

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

theorem CategoryTheory.Yoneda.fullyFaithful_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y) :

CategoryTheory.Yoneda.fullyFaithful.preimage f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)

instance CategoryTheory.Yoneda.yoneda_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.yoneda.Full

The Yoneda embedding is full.

instance CategoryTheory.Yoneda.yoneda_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.yoneda.Faithful

The Yoneda embedding is faithful.

def CategoryTheory.Yoneda.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (p : {Z : C} → (Z ⟶ X) → (Z ⟶ Y)) (q : {Z : C} → (Z ⟶ Y) → (Z ⟶ X)) (h₁ : ∀ {Z : C} (f : Z ⟶ X), q (p f) = f) (h₂ : ∀ {Z : C} (f : Z ⟶ Y), p (q f) = f) (n : ∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ X), p (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f (p g)) :

X ≅ Y

Extensionality via Yoneda. The typical usage would be

-- Goal is `X ≅ Y`
apply yoneda.ext,
-- Goals are now functions `(Z ⟶ X) → (Z ⟶ Y)`, `(Z ⟶ Y) → (Z ⟶ X)`, and the fact that these
-- functions are inverses and natural in `Z`.

Equations

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

theorem CategoryTheory.Yoneda.isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (CategoryTheory.yoneda.map f)] :

CategoryTheory.IsIso f

If yoneda.map f is an isomorphism, so was f.

@[simp]

theorem CategoryTheory.Coyoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (α : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z) (h : Opposite.unop X ⟶ Z') :

CategoryTheory.CategoryStruct.comp (α.app Z' h) f = α.app Z (CategoryTheory.CategoryStruct.comp h f)

def CategoryTheory.Coyoneda.fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.coyoneda.FullyFaithful

The co-Yoneda embedding is fully faithful.

Equations

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

theorem CategoryTheory.Coyoneda.fullyFaithful_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) :

CategoryTheory.Coyoneda.fullyFaithful.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))

def CategoryTheory.Coyoneda.preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) :

X ⟶ Y

The morphism X ⟶ Y corresponding to a natural transformation coyoneda.obj X ⟶ coyoneda.obj Y.

Equations

CategoryTheory.Coyoneda.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))

instance CategoryTheory.Coyoneda.coyoneda_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.coyoneda.Full

instance CategoryTheory.Coyoneda.coyoneda_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.coyoneda.Faithful

theorem CategoryTheory.Coyoneda.isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)] :

CategoryTheory.IsIso f

If coyoneda.map f is an isomorphism, so was f.

def CategoryTheory.Coyoneda.punitIso :

CategoryTheory.coyoneda.obj (Opposite.op PUnit.{v₁ + 1}) ≅ CategoryTheory.Functor.id (Type v₁)

The identity functor on Type is isomorphic to the coyoneda functor coming from PUnit.

Equations

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

def CategoryTheory.Coyoneda.objOpOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :

CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X)) ≅ CategoryTheory.yoneda.obj X

Taking the unop of morphisms is a natural isomorphism.

Equations

CategoryTheory.Coyoneda.objOpOp X = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => (CategoryTheory.opEquiv (Opposite.unop (Opposite.op (Opposite.op X))) x).toIso) ⋯

@[simp]

theorem CategoryTheory.Coyoneda.objOpOp_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (CategoryTheory.yoneda.obj X).obj X✝) :

(CategoryTheory.Coyoneda.objOpOp X).inv.app X✝ a✝ = (CategoryTheory.opEquiv (Opposite.op X) X✝).symm a✝

@[simp]

theorem CategoryTheory.Coyoneda.objOpOp_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X))).obj X✝) :

(CategoryTheory.Coyoneda.objOpOp X).hom.app X✝ a✝ = (CategoryTheory.opEquiv (Opposite.op X) X✝) a✝

structure CategoryTheory.Functor.RepresentableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (Y : C) :

Type (max (max u₁ v) v₁)

The data which expresses that a functor F : Cᵒᵖ ⥤ Type v is representable by Y : C.

homEquiv {X : C} : (X ⟶ Y) ≃ F.obj (Opposite.op X)
the natural bijection (X ⟶ Y) ≃ F.obj (op X).
homEquiv_comp {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y) : self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map f.op (self.homEquiv g)

def CategoryTheory.Functor.RepresentableBy.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F F' : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) (e' : F ≅ F') :

F'.RepresentableBy Y

If F ≅ F', and F is representable, then F' is representable.

Equations

e.ofIso e' = { homEquiv := fun {X : C} => e.homEquiv.trans (e'.app (Opposite.op X)).toEquiv, homEquiv_comp := ⋯ }

structure CategoryTheory.Functor.CorepresentableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) (X : C) :

Type (max (max u₁ v) v₁)

The data which expresses that a functor F : C ⥤ Type v is corepresentable by X : C.

homEquiv {Y : C} : (X ⟶ Y) ≃ F.obj Y
the natural bijection (X ⟶ Y) ≃ F.obj Y.
homEquiv_comp {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y) : self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map g (self.homEquiv f)

def CategoryTheory.Functor.CorepresentableBy.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F F' : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) (e' : F ≅ F') :

F'.CorepresentableBy X

If F ≅ F', and F is corepresentable, then F' is corepresentable.

Equations

e.ofIso e' = { homEquiv := fun {X_1 : C} => e.homEquiv.trans (e'.app X_1).toEquiv, homEquiv_comp := ⋯ }

theorem CategoryTheory.Functor.RepresentableBy.homEquiv_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y) :

e.homEquiv f = F.map f.op (e.homEquiv (CategoryTheory.CategoryStruct.id Y))

theorem CategoryTheory.Functor.CorepresentableBy.homEquiv_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y) :

e.homEquiv f = F.map f (e.homEquiv (CategoryTheory.CategoryStruct.id X))

theorem CategoryTheory.Functor.RepresentableBy.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {e e' : F.RepresentableBy Y} (h : e.homEquiv (CategoryTheory.CategoryStruct.id Y) = e'.homEquiv (CategoryTheory.CategoryStruct.id Y)) :

e = e'

theorem CategoryTheory.Functor.CorepresentableBy.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} {e e' : F.CorepresentableBy X} (h : e.homEquiv (CategoryTheory.CategoryStruct.id X) = e'.homEquiv (CategoryTheory.CategoryStruct.id X)) :

e = e'

def CategoryTheory.Functor.representableByEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {Y : C} :

F.RepresentableBy Y ≃ (CategoryTheory.yoneda.obj Y ≅ F)

The obvious bijection F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F) when F : Cᵒᵖ ⥤ Type v₁ and [Category.{v₁} C].

Equations

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

def CategoryTheory.Functor.RepresentableBy.toIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {Y : C} (e : F.RepresentableBy Y) :

CategoryTheory.yoneda.obj Y ≅ F

The isomorphism yoneda.obj Y ≅ F induced by e : F.RepresentableBy Y.

Equations

e.toIso = CategoryTheory.Functor.representableByEquiv e

def CategoryTheory.Functor.corepresentableByEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C} :

F.CorepresentableBy X ≃ (CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F)

The obvious bijection F.CorepresentableBy X ≃ (yoneda.obj Y ≅ F) when F : C ⥤ Type v₁ and [Category.{v₁} C].

Equations

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

def CategoryTheory.Functor.CorepresentableBy.toIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C} (e : F.CorepresentableBy X) :

CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F

The isomorphism coyoneda.obj (op X) ≅ F induced by e : F.CorepresentableBy X.

Equations

e.toIso = CategoryTheory.Functor.corepresentableByEquiv e

class CategoryTheory.Functor.IsRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) :

A functor F : Cᵒᵖ ⥤ Type v is representable if there is an object Y with a structure F.RepresentableBy Y, i.e. there is a natural bijection (X ⟶ Y) ≃ F.obj (op X), which may also be rephrased as a natural isomorphism yoneda.obj X ≅ F when Category.{v} C.

has_representation : ∃ (Y : C), Nonempty (F.RepresentableBy Y)

Instances

@[deprecated CategoryTheory.Functor.IsRepresentable (since := "2024-10-03")]

def CategoryTheory.Functor.Representable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) :

Alias of CategoryTheory.Functor.IsRepresentable.

Equations

@CategoryTheory.Functor.Representable = @CategoryTheory.Functor.IsRepresentable

theorem CategoryTheory.Functor.RepresentableBy.isRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) :

F.IsRepresentable

theorem CategoryTheory.Functor.IsRepresentable.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {X : C} (e : CategoryTheory.yoneda.obj X ≅ F) :

F.IsRepresentable

Alternative constructor for F.IsRepresentable, which takes as an input an isomorphism yoneda.obj X ≅ F.

instance CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :

(CategoryTheory.yoneda.obj X).IsRepresentable

class CategoryTheory.Functor.IsCorepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) :

A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.

has_corepresentation : ∃ (X : C), Nonempty (F.CorepresentableBy X)

Instances

@[deprecated CategoryTheory.Functor.IsCorepresentable (since := "2024-10-03")]

def CategoryTheory.Functor.Corepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) :

Alias of CategoryTheory.Functor.IsCorepresentable.

A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.

Equations

@CategoryTheory.Functor.Corepresentable = @CategoryTheory.Functor.IsCorepresentable

theorem CategoryTheory.Functor.CorepresentableBy.isCorepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) :

F.IsCorepresentable

theorem CategoryTheory.Functor.IsCorepresentable.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C} (e : CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F) :

F.IsCorepresentable

Alternative constructor for F.IsCorepresentable, which takes as an input an isomorphism coyoneda.obj (op X) ≅ F.

instance CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :

(CategoryTheory.coyoneda.obj X).IsCorepresentable

noncomputable def CategoryTheory.Functor.reprX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :

The representing object for the representable functor F.

Equations

F.reprX = ⋯.choose

noncomputable def CategoryTheory.Functor.representableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :

F.RepresentableBy F.reprX

A chosen term in F.RepresentableBy (reprX F) when F.IsRepresentable holds.

Equations

F.representableBy = ⋯.some

noncomputable def CategoryTheory.Functor.reprx {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :

F.obj (Opposite.op F.reprX)

The representing element for the representable functor F, sometimes called the universal element of the functor.

Equations

F.reprx = F.representableBy.homEquiv (CategoryTheory.CategoryStruct.id F.reprX)

noncomputable def CategoryTheory.Functor.reprW {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [F.IsRepresentable] :

CategoryTheory.yoneda.obj F.reprX ≅ F

An isomorphism between a representable F and a functor of the form C(-, F.reprX). Note the components F.reprW.app X definitionally have type (X.unop ⟶ F.reprX) ≅ F.obj X.

Equations

F.reprW = F.representableBy.toIso

theorem CategoryTheory.Functor.reprW_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [F.IsRepresentable] (X : Cᵒᵖ) (f : Opposite.unop X ⟶ F.reprX) :

F.reprW.hom.app X f = F.map f.op F.reprx

noncomputable def CategoryTheory.Functor.coreprX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) [hF : F.IsCorepresentable] :

The representing object for the corepresentable functor F.

Equations

F.coreprX = ⋯.choose

noncomputable def CategoryTheory.Functor.corepresentableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) [hF : F.IsCorepresentable] :

F.CorepresentableBy F.coreprX

A chosen term in F.CorepresentableBy (coreprX F) when F.IsCorepresentable holds.

Equations

F.corepresentableBy = ⋯.some

noncomputable def CategoryTheory.Functor.coreprx {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) [hF : F.IsCorepresentable] :

F.obj F.coreprX

The representing element for the corepresentable functor F, sometimes called the universal element of the functor.

Equations

F.coreprx = F.corepresentableBy.homEquiv (CategoryTheory.CategoryStruct.id F.coreprX)

noncomputable def CategoryTheory.Functor.coreprW {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [F.IsCorepresentable] :

CategoryTheory.coyoneda.obj (Opposite.op F.coreprX) ≅ F

An isomorphism between a corepresentable F and a functor of the form C(F.corepr X, -). Note the components F.coreprW.app X definitionally have type F.corepr_X ⟶ X ≅ F.obj X.

Equations

F.coreprW = F.corepresentableBy.toIso

theorem CategoryTheory.Functor.coreprW_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) :

F.coreprW.hom.app X f = F.map f F.coreprx

theorem CategoryTheory.isRepresentable_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (i : F ≅ G) [F.IsRepresentable] :

G.IsRepresentable

theorem CategoryTheory.corepresentable_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) {G : CategoryTheory.Functor C (Type v₁)} (i : F ≅ G) [F.IsCorepresentable] :

G.IsCorepresentable

instance CategoryTheory.instIsCorepresentableIdType :

(CategoryTheory.Functor.id (Type v₁)).IsCorepresentable

instance CategoryTheory.prodCategoryInstance1 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Category.{max u₁ v₁, max u₁ (max (v₁ + 1) u₁) v₁} (CategoryTheory.Functor Cᵒᵖ (Type v₁) × Cᵒᵖ)

Equations

CategoryTheory.prodCategoryInstance1 C = CategoryTheory.prod (CategoryTheory.Functor Cᵒᵖ (Type ?u.20)) Cᵒᵖ

instance CategoryTheory.prodCategoryInstance2 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Category.{max u₁ v₁, max (max (max (v₁ + 1) u₁) v₁) u₁} (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))

Equations

CategoryTheory.prodCategoryInstance2 C = CategoryTheory.prod Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type ?u.20))

def CategoryTheory.yonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} :

(CategoryTheory.yoneda.obj X ⟶ F) ≃ F.obj (Opposite.op X)

We have a type-level equivalence between natural transformations from the yoneda embedding and elements of F.obj X, without any universe switching.

Equations

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

theorem CategoryTheory.yonedaEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) :

CategoryTheory.yonedaEquiv f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem CategoryTheory.yonedaEquiv_symm_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) :

(CategoryTheory.yonedaEquiv.symm x).app Y f = F.map f.op x

theorem CategoryTheory.yonedaEquiv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) :

F.map g.op (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)

See also yonedaEquiv_naturality' for a more general version.

theorem CategoryTheory.yonedaEquiv_naturality' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) :

F.map g (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)

Variant of yonedaEquiv_naturality with general g. This is technically strictly more general than yonedaEquiv_naturality, but yonedaEquiv_naturality is sometimes preferable because it can avoid the "motive is not type correct" error.

theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X ⟶ F) (β : F ⟶ G) :

CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app (Opposite.op X) (CategoryTheory.yonedaEquiv α)

theorem CategoryTheory.yonedaEquiv_yoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :

CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f

theorem CategoryTheory.yonedaEquiv_symm_naturality_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (x : F.obj (Opposite.op X)) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) (CategoryTheory.yonedaEquiv.symm x) = CategoryTheory.yonedaEquiv.symm (F.map f.op x)

theorem CategoryTheory.yonedaEquiv_symm_naturality_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {F F' : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : F ⟶ F') (x : F.obj (Opposite.op X)) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yonedaEquiv.symm x) f = CategoryTheory.yonedaEquiv.symm (f.app (Opposite.op X) x)

theorem CategoryTheory.map_yonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) :

F.map g.op (CategoryTheory.yonedaEquiv f) = f.app (Opposite.op Y) g

See also map_yonedaEquiv' for a more general version.

theorem CategoryTheory.map_yonedaEquiv' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) :

F.map g (CategoryTheory.yonedaEquiv f) = f.app Y g.unop

Variant of map_yonedaEquiv with general g. This is technically strictly more general than map_yonedaEquiv, but map_yonedaEquiv is sometimes preferable because it can avoid the "motive is not type correct" error.

theorem CategoryTheory.yonedaEquiv_symm_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (t : F.obj X) :

CategoryTheory.yonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)

theorem CategoryTheory.hom_ext_yoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : P ⟶ Q} (h : ∀ (X : C) (p : CategoryTheory.yoneda.obj X ⟶ P), CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) :

f = g

Two morphisms of presheaves of types P ⟶ Q coincide if the precompositions with morphisms yoneda.obj X ⟶ P agree.

def CategoryTheory.yonedaEvaluation (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))

The "Yoneda evaluation" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type to F.obj X, functorially in both X and F.

Equations

CategoryTheory.yonedaEvaluation C = (CategoryTheory.evaluationUncurried Cᵒᵖ (Type ?u.24)).comp CategoryTheory.uliftFunctor.{?u.23, ?u.24}

@[simp]

theorem CategoryTheory.yonedaEvaluation_map_down (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (x : (CategoryTheory.yonedaEvaluation C).obj P) :

((CategoryTheory.yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)

def CategoryTheory.yonedaPairing (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))

The "Yoneda pairing" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type to yoneda.op.obj X ⟶ F, functorially in both X and F.

Equations

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

theorem CategoryTheory.yonedaPairingExt (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)} {x y : (CategoryTheory.yonedaPairing C).obj X} (w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y) :

x = y

@[simp]

theorem CategoryTheory.yonedaPairing_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.yonedaPairing C).obj P) :

(CategoryTheory.yonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.1.unop) (CategoryTheory.CategoryStruct.comp β α.2)

def CategoryTheory.yonedaCompUliftFunctorEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ w))) (X : C) :

((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} ⟶ F) ≃ F.obj (Opposite.op X)

A bijection (yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X) which is a variant of yonedaEquiv with heterogeneous universes.

Equations

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

CategoryTheory.yonedaPairing C ≅ CategoryTheory.yonedaEvaluation C

def CategoryTheory.yonedaLemma (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

The Yoneda lemma asserts that the Yoneda pairing (X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F) is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.

Equations

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

def CategoryTheory.curriedYonedaLemma {C : Type u₁} [CategoryTheory.SmallCategory C] :

CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅ CategoryTheory.evaluation Cᵒᵖ (Type u₁)

The curried version of yoneda lemma when C is small.

Equations

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

def CategoryTheory.largeCurriedYonedaLemma {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation Cᵒᵖ (Type v₁)).comp ((CategoryTheory.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj CategoryTheory.uliftFunctor.{u₁, v₁})

The curried version of the Yoneda lemma.

Equations

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

def CategoryTheory.yonedaOpCompYonedaObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) :

CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj P) ≅ P.comp CategoryTheory.uliftFunctor.{u₁, v₁}

Version of the Yoneda lemma where the presheaf is fixed but the argument varies.

Equations

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

def CategoryTheory.curriedYonedaLemma' {C : Type u₁} [CategoryTheory.SmallCategory C] :

CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj CategoryTheory.yoneda.op) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type u₁))

The curried version of yoneda lemma when C is small.

Equations

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

theorem CategoryTheory.isIso_of_yoneda_map_bijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryTheory.CategoryStruct.comp x f) :

CategoryTheory.IsIso f

theorem CategoryTheory.isIso_iff_yoneda_map_bijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :

CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryTheory.CategoryStruct.comp x f

theorem CategoryTheory.isIso_iff_isIso_yoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :

CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.yoneda.map f).app (Opposite.op c))

def CategoryTheory.coyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} :

(CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) ≃ F.obj X

We have a type-level equivalence between natural transformations from the coyoneda embedding and elements of F.obj X.unop, without any universe switching.

Equations

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

theorem CategoryTheory.coyonedaEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) :

CategoryTheory.coyonedaEquiv f = f.app X (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem CategoryTheory.coyonedaEquiv_symm_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} (x : F.obj X) (Y : C) (f : X ⟶ Y) :

(CategoryTheory.coyonedaEquiv.symm x).app Y f = F.map f x

theorem CategoryTheory.coyonedaEquiv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) :

F.map g (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)

theorem CategoryTheory.coyonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor C (Type v₁)} (α : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (β : F ⟶ G) :

CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app X (CategoryTheory.coyonedaEquiv α)

theorem CategoryTheory.coyonedaEquiv_coyoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :

CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f

theorem CategoryTheory.map_coyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) :

F.map g (CategoryTheory.coyonedaEquiv f) = f.app Y g

theorem CategoryTheory.coyonedaEquiv_symm_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type v₁)} (t : F.obj X) :

CategoryTheory.coyonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)

def CategoryTheory.coyonedaEvaluation (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))

The "Coyoneda evaluation" functor, which sends X : C and F : C ⥤ Type to F.obj X, functorially in both X and F.

Equations

CategoryTheory.coyonedaEvaluation C = (CategoryTheory.evaluationUncurried C (Type ?u.24)).comp CategoryTheory.uliftFunctor.{?u.23, ?u.24}

@[simp]

theorem CategoryTheory.coyonedaEvaluation_map_down (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q) (x : (CategoryTheory.coyonedaEvaluation C).obj P) :

((CategoryTheory.coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)

def CategoryTheory.coyonedaPairing (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))

The "Coyoneda pairing" functor, which sends X : C and F : C ⥤ Type to coyoneda.rightOp.obj X ⟶ F, functorially in both X and F.

Equations

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

theorem CategoryTheory.coyonedaPairingExt (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C × CategoryTheory.Functor C (Type v₁)} {x y : (CategoryTheory.coyonedaPairing C).obj X} (w : ∀ (Y : C), x.app Y = y.app Y) :

x = y

@[simp]

theorem CategoryTheory.coyonedaPairing_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.coyonedaPairing C).obj P) :

(CategoryTheory.coyonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)

def CategoryTheory.coyonedaCompUliftFunctorEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max v₁ w))) (X : Cᵒᵖ) :

((CategoryTheory.coyoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} ⟶ F) ≃ F.obj (Opposite.unop X)

A bijection (coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (unop X) which is a variant of coyonedaEquiv with heterogeneous universes.

Equations

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

CategoryTheory.coyonedaPairing C ≅ CategoryTheory.coyonedaEvaluation C

def CategoryTheory.coyonedaLemma (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

The Coyoneda lemma asserts that the Coyoneda pairing (X : C, F : C ⥤ Type) ↦ (coyoneda.obj X ⟶ F) is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.