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

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

@[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

@[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)

@[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

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.

@[simp]

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

@[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

@[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)

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)

@[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)

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

The Yoneda embedding is fully faithful.

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)

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

The Yoneda embedding is full.

Stacks Tag 001P

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

The Yoneda embedding is faithful.

Stacks Tag 001P

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

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.

@[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)

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

The co-Yoneda embedding is fully faithful.

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

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.

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

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

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

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.

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.

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.

@[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✝

@[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✝

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.

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)

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)

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.

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)

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)

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.

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

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

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.

@[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

@[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

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.

@[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

@[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

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'

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)

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'

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)

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

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.

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

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.

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)

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

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.

instance CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : (yoneda.obj X).IsRepresentable

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)

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

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.

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

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

The representing object for the representable functor F.

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.

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.

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.

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.

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

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

The representing object for the corepresentable functor F.

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.

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.

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.

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.

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

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

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

instance CategoryTheory.instIsCorepresentableIdType : (Functor.id (Type v₁)).IsCorepresentable

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ᵒᵖ)

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₁))

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.

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)

@[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

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.

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.

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 α)

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

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)

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)

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.

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.

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)

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.

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.

@[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)

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.

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

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

@[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)

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.

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

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.

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.

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.

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.

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

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

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

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.

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)

@[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

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)

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 α)

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

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

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)

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.

@[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)

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.

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

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

@[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)

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.

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

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.

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.

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.

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.

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

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

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)

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.

@[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

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.

@[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

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

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 τ)

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.

@[simp]

theorem CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : Functor C (Type (max u₁ u₂))) (a✝ : (Functor.sectionsFunctor C).obj X✝) (j : C) (x : ((Functor.const C).obj X).obj j) : ((sectionsFunctorNatIsoCoyoneda X).hom.app X✝ a✝).app j x = ↑a✝ j

@[simp]

theorem CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_coe {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : Functor C (Type (max u₁ u₂))) (a✝ : (coyoneda.obj (Opposite.op ((Functor.const C).obj X))).obj X✝) (j : C) : ↑((sectionsFunctorNatIsoCoyoneda X).inv.app X✝ a✝) j = a✝.app j default

def CategoryTheory.Functor.FullyFaithful.homNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) : F.op.comp ((yoneda.obj (F.obj X)).comp uliftFunctor.{v₁, v₂}) ≅ (yoneda.obj X).comp uliftFunctor.{v₂, v₁}

FullyFaithful.homEquiv as a natural isomorphism.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp ((yoneda.obj (F.obj X)).comp uliftFunctor.{v₁, v₂})).obj X✝) : ((hF.homNatIso X).hom.app X✝ a✝).down = hF.preimage a✝.down

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝) : ((hF.homNatIso X).inv.app X✝ a✝).down = F.map a✝.down

def CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) : F.op.comp (yoneda.obj (F.obj X)) ≅ (yoneda.obj X).comp uliftFunctor.{v₂, v₁}

FullyFaithful.homEquiv as a natural isomorphism.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝) : (hF.homNatIsoMaxRight X).inv.app X✝ a✝ = F.map a✝.down

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp (yoneda.obj (F.obj X))).obj X✝) : ((hF.homNatIsoMaxRight X).hom.app X✝ a✝).down = hF.preimage a✝

def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) : F.comp (yoneda.comp (((whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₂)).obj F.op).comp ((Functor.whiskeringRight Cᵒᵖ (Type v₂) (Type (max v₂ v₁))).obj uliftFunctor.{v₁, v₂}))) ≅ yoneda.comp ((Functor.whiskeringRight Cᵒᵖ (Type v₁) (Type (max v₂ v₁))).obj uliftFunctor.{v₂, v₁})

FullyFaithful.homEquiv as a natural isomorphism.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft_inv_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝) : ((hF.compYonedaCompWhiskeringLeft.inv.app X).app X✝ a✝).down = F.map a✝.down

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft_hom_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp ((yoneda.obj (F.obj X)).comp uliftFunctor.{v₁, v₂})).obj X✝) : ((hF.compYonedaCompWhiskeringLeft.hom.app X).app X✝ a✝).down = hF.preimage a✝.down

def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) : F.comp (yoneda.comp ((whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅ yoneda.comp ((Functor.whiskeringRight Cᵒᵖ (Type v₁) (Type (max v₁ v₂))).obj uliftFunctor.{v₂, v₁})

FullyFaithful.homEquiv as a natural isomorphism.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝) : (hF.compYonedaCompWhiskeringLeftMaxRight.inv.app X).app X✝ a✝ = F.map a✝.down

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp (yoneda.obj (F.obj X))).obj X✝) : ((hF.compYonedaCompWhiskeringLeftMaxRight.hom.app X).app X✝ a✝).down = hF.preimage a✝