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.

Equations

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

Instances For

source

@[simp]

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

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

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

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

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

Variant of the Yoneda embedding which allows a raise in the universe level for the category of types.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.uliftYoneda_map_app_down {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) (a✝ : uliftFunctor.{w, v₁}.obj ((yoneda.obj X✝).obj X)) :

((uliftYoneda.{w, v₁, u₁}.map f).app X a✝).down = CategoryStruct.comp a✝.down f

source

@[simp]

theorem CategoryTheory.uliftYoneda_obj_map_down {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : uliftFunctor.{w, v₁}.obj ((yoneda.obj X).obj X✝)) :

((uliftYoneda.{w, v₁, u₁}.obj X).map f a✝).down = CategoryStruct.comp f.unop a✝.down

source

@[simp]

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

(uliftYoneda.{w, v₁, u₁}.obj X).obj X✝ = ULift.{w, v₁} (Opposite.unop X✝ ⟶ X)

source

def CategoryTheory.uliftYonedaIsoYoneda {C : Type u₁} [Category.{max w v₁, u₁} C] :

uliftYoneda.{w, max v₁ w, u₁} ≅ yoneda

If C is a category with [Category.{max w v₁} C], this is the isomorphism uliftYoneda.{w} (C := C) ≅ yoneda.

Equations

CategoryTheory.uliftYonedaIsoYoneda = CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.NatIso.ofComponents (fun (x_1 : Cᵒᵖ) => Equiv.ulift.toIso) ⋯) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.uliftYonedaIsoYoneda_hom_app_app {C : Type u₁} [Category.{max w v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (uliftYoneda.{w, max v₁ w, u₁}.obj X).obj X✝) :

(uliftYonedaIsoYoneda.hom.app X).app X✝ a✝ = a✝.down

source

@[simp]

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

((uliftYonedaIsoYoneda.inv.app X).app X✝ a✝).down = a✝

source

@[reducible, inline]

abbrev 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

CategoryTheory.coyoneda = CategoryTheory.yoneda.flip

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.uliftCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] :

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

Variant of the Coyoneda embedding which allows a raise in the universe level for the category of types.

Equations

CategoryTheory.uliftCoyoneda.{?u.20, ?u.19, ?u.18} = CategoryTheory.uliftYoneda.{?u.20, ?u.19, ?u.18}.flip

Instances For

source

def CategoryTheory.uliftCoyonedaIsoCoyoneda {C : Type u₁} [Category.{max w v₁, u₁} C] :

uliftCoyoneda.{w, max v₁ w, u₁} ≅ coyoneda

If C is a category with [Category.{max w v₁} C], this is the isomorphism uliftCoyoneda.{w} (C := C) ≅ coyoneda.

Equations

CategoryTheory.uliftCoyonedaIsoCoyoneda = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => CategoryTheory.NatIso.ofComponents (fun (x_1 : C) => Equiv.ulift.toIso) ⋯) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.uliftCoyonedaIsoCoyoneda_inv_app_app_down {C : Type u₁} [Category.{max w v₁, u₁} C] (X : Cᵒᵖ) (X✝ : C) (a✝ : (coyoneda.obj X).obj X✝) :

((uliftCoyonedaIsoCoyoneda.inv.app X).app X✝ a✝).down = a✝

source

@[simp]

theorem CategoryTheory.uliftCoyonedaIsoCoyoneda_hom_app_app {C : Type u₁} [Category.{max w v₁, u₁} C] (X : Cᵒᵖ) (X✝ : C) (a✝ : (uliftCoyoneda.{w, max v₁ w, u₁}.obj X).obj X✝) :

(uliftCoyonedaIsoCoyoneda.hom.app X).app X✝ a✝ = a✝.down

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.

source

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

yoneda.Faithful

The Yoneda embedding is faithful.

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

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

uliftYoneda.{w, v₁, u₁}.FullyFaithful

When C is category such that Category.{v₁} C, then the functor uliftYoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type max w v₁ is fully faithful.

Equations

CategoryTheory.ULiftYoneda.fullyFaithful C = CategoryTheory.Yoneda.fullyFaithful.comp (CategoryTheory.fullyFaithfulULiftFunctor.whiskeringRight Cᵒᵖ)

Instances For

source

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

uliftYoneda.{w, v₁, u₁}.Full

source

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

uliftYoneda.{w, v₁, u₁}.Faithful

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

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

X ≅ Y

Extensionality via Coyoneda. The typical usage would be

-- Goal is `X ≅ Y`
apply Coyoneda.ext
-- Goals are now functions `(X ⟶ Z) → (Y ⟶ Z)`, `(Y ⟶ Z) → (X ⟶ Z)`, 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.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

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

yoneda.comp ((Functor.whiskeringLeft C Cᵒᵖ ᵒᵖ (Type v₁)).obj (opOp C)) ≅ coyoneda

Taking the unop of morphisms is a natural isomorphism.

Equations

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

Instances For

source

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

uliftCoyoneda.{w, v₁, u₁}.FullyFaithful

When C is category such that Category.{v₁} C, then the functor uliftCoyoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type max w v₁ is fully faithful.

Equations

CategoryTheory.Coyoneda.ULiftCoyoneda.fullyFaithful C = CategoryTheory.Coyoneda.fullyFaithful.comp (CategoryTheory.fullyFaithfulULiftFunctor.whiskeringRight C)

Instances For

source

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

uliftCoyoneda.{w, v₁, u₁}.Full

source

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

uliftCoyoneda.{w, v₁, u₁}.Faithful

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

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

Y ≅ Y'

Representing objects are unique up to isomorphism.

Equations

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

Instances For

source

@[simp]

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

(e.uniqueUpToIso e').hom = Yoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : Cᵒᵖ) => { hom := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, inv := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).hom

source

@[simp]

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

(e.uniqueUpToIso e').inv = Yoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : Cᵒᵖ) => { hom := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, inv := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).inv

source

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

X ≅ X'

Corepresenting objects are unique up to isomorphism.

Equations

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

Instances For

source

@[simp]

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

(e.uniqueUpToIso e').inv = (Coyoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : C) => { hom := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, inv := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).inv).unop

source

@[simp]

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

(e.uniqueUpToIso e').hom = (Coyoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : C) => { hom := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, inv := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).hom).unop

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.RepresentableBy.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor Cᵒᵖ (Type v)} {Y : C} {e e' : F.RepresentableBy Y} :

e = e' ↔ e.homEquiv (CategoryStruct.id Y) = e'.homEquiv (CategoryStruct.id Y)

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

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

e = e' ↔ e.homEquiv (CategoryStruct.id X) = e'.homEquiv (CategoryStruct.id X)

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.

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

Instances

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.

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

Instances

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.RepresentableBy.isoReprX {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] {Y : C} (e : F.RepresentableBy Y) :

Y ≅ F.reprX

Any representing object for a representable functor F is isomorphic to reprX F.

Equations

CategoryTheory.Functor.RepresentableBy.isoReprX F e = e.uniqueUpToIso F.representableBy

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.CorepresentableBy.isoCoreprX {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} [hF : F.IsCorepresentable] {Y : C} (e : F.CorepresentableBy Y) :

Y ≅ F.coreprX

Any corepresenting object for a corepresentable functor F is isomorphic to coreprX F.

Equations

e.isoCoreprX = e.uniqueUpToIso F.corepresentableBy

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.15)) 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.15))

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.19)).comp CategoryTheory.uliftFunctor.{?u.18, ?u.19}

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

theorem CategoryTheory.yonedaPairingExt_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ × Functor Cᵒᵖ (Type v₁)} {x y : (yonedaPairing C).obj X} :

x = y ↔ ∀ (Y : Cᵒᵖ), x.app Y = y.app 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.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.

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 ((Functor.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 ((Functor.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.uliftYonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor Cᵒᵖ (Type (max w v₁))} :

(uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.op X)

Yoneda's lemma as a bijection (uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X) for any presheaf of type F : Cᵒᵖ ⥤ Type (max w v₁) for some auxiliary universe w.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.uliftYonedaEquiv_symm_apply_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor Cᵒᵖ (Type (max w v₁))} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (y : (uliftYoneda.{w, v₁, u₁}.obj X).obj Y) :

(uliftYonedaEquiv.symm x).app Y y = F.map y.down.op x

source

theorem CategoryTheory.uliftYonedaEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor Cᵒᵖ (Type (max w v₁))} (τ : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) :

uliftYonedaEquiv τ = τ.app (Opposite.op X) { down := CategoryStruct.id X }

source

@[deprecated CategoryTheory.uliftYonedaEquiv (since := "2025-08-04")]

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

(uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.op X)

Alias of CategoryTheory.uliftYonedaEquiv.

Yoneda's lemma as a bijection (uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X) for any presheaf of type F : Cᵒᵖ ⥤ Type (max w v₁) for some auxiliary universe w.

Equations

@CategoryTheory.yonedaCompUliftFunctorEquiv = @CategoryTheory.uliftYonedaEquiv

Instances For

source

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

F.map g (uliftYonedaEquiv f) = uliftYonedaEquiv (CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map g.unop) f)

source

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

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

source

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

uliftYonedaEquiv.symm (F.map f t) = CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map f.unop) (uliftYonedaEquiv.symm t)

source

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

CategoryStruct.comp (uliftYonedaEquiv.symm (F.map f t)) h = CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map f.unop) (CategoryStruct.comp (uliftYonedaEquiv.symm t) h)

source

@[simp]

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

uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f) = { down := f }

source

theorem CategoryTheory.hom_ext_uliftYoneda {C : Type u₁} [Category.{v₁, u₁} C] {P Q : Functor Cᵒᵖ (Type (max w v₁))} {f g : P ⟶ Q} (h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.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 uliftYoneda.obj X ⟶ P agree.

source

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

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

A variant of the curried version of the Yoneda lemma with a raise in the universe level.

Equations

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

Instances For

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.19)).comp CategoryTheory.uliftFunctor.{?u.18, ?u.19}

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

theorem CategoryTheory.coyonedaPairingExt_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C × Functor C (Type v₁)} {x y : (coyonedaPairing C).obj X} :

x = y ↔ ∀ (Y : C), x.app Y = y.app 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.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.

Equations

CategoryTheory.coyonedaLemma C = CategoryTheory.NatIso.ofComponents (fun (x : C × CategoryTheory.Functor C (Type ?u.20)) => (CategoryTheory.coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯

Instances For

source

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

coyoneda.rightOp.comp coyoneda ≅ evaluation C (Type u₁)

The curried version of coyoneda lemma when C is small.

Equations

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

Instances For

source

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

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

The curried version of the Coyoneda lemma.

Equations

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

Instances For

source

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

coyoneda.rightOp.comp (yoneda.obj P) ≅ P.comp uliftFunctor.{u₁, v₁}

Version of the Coyoneda 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.curriedCoyonedaLemma' {C : Type u₁} [SmallCategory C] :

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

The curried version of coyoneda 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_coyoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryStruct.comp f x) :

IsIso f

source

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

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

source

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

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

source

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

(uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.unop X)

Coyoneda's lemma as a bijection (uliftCoyoneda.{w}.obj X ⟶ F) ≃ F.obj (op X) for any presheaf of type F : Cᵒᵖ ⥤ Type (max w v₁) for some auxiliary universe w.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.uliftCoyonedaEquiv_symm_apply_app {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : Functor C (Type (max w v₁))} (x : F.obj (Opposite.unop X)) (Y : C) (y : (uliftCoyoneda.{w, v₁, u₁}.obj X).obj Y) :

(uliftCoyonedaEquiv.symm x).app Y y = F.map y.down x

source

theorem CategoryTheory.uliftCoyonedaEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : Functor C (Type (max w v₁))} (τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) :

uliftCoyonedaEquiv τ = τ.app (Opposite.unop X) { down := CategoryStruct.id (Opposite.unop X) }

source

@[deprecated CategoryTheory.uliftCoyonedaEquiv (since := "2025-08-04")]

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

(uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.unop X)

Alias of CategoryTheory.uliftCoyonedaEquiv.

Coyoneda's lemma as a bijection (uliftCoyoneda.{w}.obj X ⟶ F) ≃ F.obj (op X) for any presheaf of type F : Cᵒᵖ ⥤ Type (max w v₁) for some auxiliary universe w.

Equations

@CategoryTheory.coyonedaCompUliftFunctorEquiv = @CategoryTheory.uliftCoyonedaEquiv

Instances For

source

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

F.map g (uliftCoyonedaEquiv f) = uliftCoyonedaEquiv (CategoryStruct.comp (uliftCoyoneda.{w, v₁, u₁}.map g.op) f)

source

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

uliftCoyonedaEquiv (CategoryStruct.comp α β) = β.app (Opposite.unop X) (uliftCoyonedaEquiv α)

source

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

uliftCoyonedaEquiv.symm (F.map f t) = CategoryStruct.comp (uliftCoyoneda.{w, v₁, u₁}.map f.op) (uliftCoyonedaEquiv.symm t)

source

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

CategoryStruct.comp (uliftCoyonedaEquiv.symm (F.map f t)) h = CategoryStruct.comp (uliftCoyoneda.{w, v₁, u₁}.map f.op) (CategoryStruct.comp (uliftCoyonedaEquiv.symm t) h)

source

@[simp]

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

uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f) = { down := f.unop }

source

theorem CategoryTheory.hom_ext_uliftCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] {P Q : Functor C (Type (max w v₁))} {f g : P ⟶ Q} (h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.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 uliftCoyoneda.obj X ⟶ P agree.

source

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

uliftCoyoneda.{w, v₁, u₁}.rightOp.comp coyoneda ≅ (evaluation C (Type (max v₁ w))).comp ((Functor.whiskeringRight (Functor C (Type (max v₁ w))) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj uliftFunctor.{u₁, max v₁ w})

A variant of the curried version of the Coyoneda lemma with a raise in the universe level.

Equations

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

Instances For

source

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

yoneda.obj X ⟶ F.op.comp (yoneda.obj (F.obj X))

The natural transformation yoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X) when F : C ⥤ D and X : C.

Equations

CategoryTheory.yonedaMap F X = { app := fun (x : Cᵒᵖ) (f : (CategoryTheory.yoneda.obj X).obj x) => F.map f, naturality := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.yonedaMap_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v₁, u_1} D] (F : Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X ⟶ Y) :

(yonedaMap F Y).app X f = F.map f

source

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

uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ F.op.comp (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X))

The natural transformation uliftYoneda.obj X ⟶ F.op ⋙ uliftYoneda.obj (F.obj X) when F : C ⥤ D and X : C.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.uliftYonedaMap_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X ⟶ Y) :

(uliftYonedaMap F Y).app X { down := f } = { down := F.map f }

source

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

↑F.sections ≃ ((const C).obj X ⟶ F)

A type-level equivalence between sections of a functor and morphisms from a terminal functor to it. We use the constant functor on a given singleton type here as a specific choice of terminal functor.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.sectionsEquivHom_apply_app {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type u₂)) (X : Type u₂) [Unique X] (s : ↑F.sections) (j : C) (x : ((const C).obj X).obj j) :

((F.sectionsEquivHom X) s).app j x = ↑s j

source

theorem CategoryTheory.Functor.sectionsEquivHom_naturality {C : Type u₁} [Category.{v₁, u₁} C] {F G : Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (x : ↑F.sections) :

(G.sectionsEquivHom X) ((sectionsFunctor C).map f x) = CategoryStruct.comp ((F.sectionsEquivHom X) x) f

source

theorem CategoryTheory.Functor.sectionsEquivHom_naturality_symm {C : Type u₁} [Category.{v₁, u₁} C] {F G : Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (τ : (const C).obj X ⟶ F) :

(G.sectionsEquivHom X).symm (CategoryStruct.comp τ f) = (sectionsFunctor C).map f ((F.sectionsEquivHom X).symm τ)

source

noncomputable def CategoryTheory.sectionsFunctorNatIsoCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] :

Functor.sectionsFunctor C ≅ coyoneda.obj (Opposite.op ((Functor.const C).obj X))

A natural isomorphism between the sections functor (C ⥤ Type _) ⥤ Type _ and the co-Yoneda embedding of a terminal functor, specifically a constant functor on a given singleton type X.

Equations