The Yoneda embedding #

The Yoneda embedding as a functor yoneda : C ⥤ (Cᵒᵖ ⥤ Type v₁), along with an instance that it is FullyFaithful.

Also the Yoneda lemma, yonedaLemma : (yoneda_pairing C) ≅ (yoneda_evaluation C).

References #

Stacks: Opposite Categories and the Yoneda Lemma

source

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

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

The Yoneda embedding, as a functor from C into presheaves on C.

Stacks Tag 001O

Equations

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

Instances For

source

@[simp]

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

(yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)

source

@[simp]

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

(yoneda.obj X).map f g = CategoryStruct.comp f.unop g

source

@[simp]

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

(yoneda.map f).app x✝ g = CategoryStruct.comp g f

source

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

Functor Cᵒᵖ (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.

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem CategoryTheory.coyoneda_map_app {C : Type u₁} [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) => CategoryStruct.comp g f, map_id := ⋯, map_comp := ⋯ }) X✝).obj x✝) :

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

source

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

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

source

@[simp]

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

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

source

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

yoneda.FullyFaithful

The Yoneda embedding is fully faithful.

Equations

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

Instances For

source

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

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

source

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

yoneda.Full

The Yoneda embedding is full.

Stacks Tag 001P

source

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

yoneda.Faithful

The Yoneda embedding is faithful.

Stacks Tag 001P

source

def CategoryTheory.Yoneda.ext {C : Type u₁} [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 (CategoryStruct.comp f g) = 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.

Instances For

source

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

IsIso f

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

source

@[simp]

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

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

source

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

coyoneda.FullyFaithful

The co-Yoneda embedding is fully faithful.

Equations

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

Instances For

source

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

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

source

def CategoryTheory.Coyoneda.preimage {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : coyoneda.obj X ⟶ 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)))

Instances For

source

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

coyoneda.Full

source

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

coyoneda.Faithful

source

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

IsIso f

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

source

def CategoryTheory.Coyoneda.punitIso :

coyoneda.obj (Opposite.op PUnit.{v₁ + 1}) ≅ 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.

Instances For

source

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

coyoneda.obj (Opposite.op (Opposite.op X)) ≅ 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) ⋯

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

structure CategoryTheory.Functor.RepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : 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 (CategoryStruct.comp f g) = F.map f.op (self.homEquiv g)

Instances For

source

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

CategoryStruct.comp f (e.homEquiv.symm x) = e.homEquiv.symm (F.map f.op x)

source

def CategoryTheory.Functor.RepresentableBy.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {F F' : 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 := ⋯ }

Instances For

source

structure CategoryTheory.Functor.CorepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : 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 (CategoryStruct.comp f g) = F.map g (self.homEquiv f)

Instances For

source

theorem CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') :

CategoryStruct.comp (e.homEquiv.symm y) g = e.homEquiv.symm (F.map g y)

source

def CategoryTheory.Functor.CorepresentableBy.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {F F' : 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 := ⋯ }

Instances For

source

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

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

source

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

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

source

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

e = e'

source

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

e = e'

source

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

F.RepresentableBy Y ≃ (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.

Instances For

source

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

yoneda.obj Y ≅ F

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

Equations

e.toIso = CategoryTheory.Functor.representableByEquiv e

Instances For

source

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

F.CorepresentableBy X ≃ (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.

Instances For

source

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

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

Instances For

source

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

Prop

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.

Stacks Tag 001Q

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

Instances

source

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

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

Prop

Alias of CategoryTheory.Functor.IsRepresentable.

Stacks Tag 001Q

Equations

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

Instances For

source

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

F.IsRepresentable

source

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

F.IsRepresentable

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

source

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

(yoneda.obj X).IsRepresentable

source

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

Prop

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

Stacks Tag 001Q

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

Instances

source

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

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

Prop

Alias of CategoryTheory.Functor.IsCorepresentable.

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

Stacks Tag 001Q

Equations

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

Instances For

source

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

F.IsCorepresentable

source

theorem CategoryTheory.Functor.IsCorepresentable.mk' {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v₁)} {X : C} (e : 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.

source

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

(coyoneda.obj X).IsCorepresentable

source

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

The representing object for the representable functor F.

Equations

F.reprX = ⋯.choose

Instances For

source

noncomputable def CategoryTheory.Functor.representableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : 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

Instances For

source

noncomputable def CategoryTheory.Functor.reprx {C : Type u₁} [Category.{v₁, u₁} C] (F : 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)

Instances For

source

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

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

Instances For

source

theorem CategoryTheory.Functor.reprW_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (F : 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

source

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

The representing object for the corepresentable functor F.

Equations

F.coreprX = ⋯.choose

Instances For

source

noncomputable def CategoryTheory.Functor.corepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : 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

Instances For

source

noncomputable def CategoryTheory.Functor.coreprx {C : Type u₁} [Category.{v₁, u₁} C] (F : 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)

Instances For

source

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

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

Instances For

source

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

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

source

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

G.IsRepresentable

source

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

G.IsCorepresentable

source

instance CategoryTheory.instIsCorepresentableIdType :

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

source

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

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

Equations

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

source

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

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

Equations

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

source

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

(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.

Instances For

source

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

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

source

@[simp]

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

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

source

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

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

See also yonedaEquiv_naturality' for a more general version.

source

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

F.map g (yonedaEquiv f) = yonedaEquiv (CategoryStruct.comp (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.

source

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

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

source

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

yonedaEquiv (yoneda.map f) = f

source

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

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

source

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

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

source

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

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

See also map_yonedaEquiv' for a more general version.

source

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

F.map g (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.

source

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

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

source

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

source

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

Functor (Cᵒᵖ × 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.26)).comp CategoryTheory.uliftFunctor.{?u.25, ?u.26}

Instances For

source

@[simp]

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

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

source

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

Functor (Cᵒᵖ × 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.

Instances For

source

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

x = y

source

@[simp]

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

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

source

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

((yoneda.obj X).comp 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.

Instances For

source

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

yonedaPairing C ≅ yonedaEvaluation 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.

Stacks Tag 001P

Equations

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

Instances For

source

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

yoneda.op.comp coyoneda ≅ 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.

Instances For

source

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

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

The curried version of the Yoneda lemma.

Equations

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

Instances For

source

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

yoneda.op.comp (yoneda.obj P) ≅ P.comp 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.

Instances For

source

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

yoneda.comp ((whiskeringLeft Cᵒᵖ (Functor Cᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj yoneda.op) ≅ Functor.id (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.

Instances For

source

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

IsIso f

source

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

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

source

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

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

source

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

(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.

Instances For

source

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

coyonedaEquiv (coyoneda.map f.op) = f

source

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

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

source

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

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

source

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

Functor (C × 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.26)).comp CategoryTheory.uliftFunctor.{?u.25, ?u.26}

Instances For

source

@[simp]

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

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

source

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

Functor (C × 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.

Instances For

source

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

x = y

source

@[simp]

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

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

source

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

((coyoneda.obj X).comp 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.

Instances For

source

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

coyonedaPairing C ≅ coyonedaEvaluation 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.

Stacks Tag 001P

Equations