Mathlib.CategoryTheory.Yoneda

CategoryTheory.yoneda definition

: C ⥤ Cᵒᵖ ⥤ Type v₁

Full source

/-- The Yoneda embedding, as a functor from `C` into presheaves on `C`. -/
@[simps, stacks 001O]
def yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁ where
  obj X :=
    { obj := fun Y => unop Y ⟶ X
      map := fun f g => f.unop ≫ g }
  map f :=
    { app := fun _ g => g ≫ f }

Yoneda Embedding Functor

Informal description

The Yoneda embedding is a functor from a category $C$ to the category of presheaves on $C$, which sends an object $X$ in $C$ to the contravariant functor $\mathrm{Hom}(-, X) \colon C^{\mathrm{op}} \to \mathrm{Type}$ that maps an object $Y$ in $C^{\mathrm{op}}$ to the set of morphisms $\mathrm{Hom}(Y, X)$ in $C$, and a morphism $f \colon Y \to Z$ in $C^{\mathrm{op}}$ to the precomposition map $(-) \circ f \colon \mathrm{Hom}(Z, X) \to \mathrm{Hom}(Y, X)$. The functor also maps a morphism $f \colon X \to X'$ in $C$ to the natural transformation $\mathrm{Hom}(-, X) \Rightarrow \mathrm{Hom}(-, X')$ given by postcomposition with $f$.

CategoryTheory.coyoneda definition

: Cᵒᵖ ⥤ C ⥤ Type v₁

Full source

/-- The co-Yoneda embedding, as a functor from `Cᵒᵖ` into co-presheaves on `C`.
-/
@[simps]
def coyoneda : CᵒᵖCᵒᵖ ⥤ C ⥤ Type v₁ where
  obj X :=
    { obj := fun Y => unop X ⟶ Y
      map := fun f g => g ≫ f }
  map f :=
    { app := fun _ g => f.unop ≫ g }

Co-Yoneda Embedding Functor

Informal description

The co-Yoneda embedding is a functor from the opposite category $C^{\mathrm{op}}$ to the category of copresheaves on $C$ (i.e., functors $C \to \mathrm{Type}$). For an object $X$ in $C^{\mathrm{op}}$, it sends $X$ to the covariant functor $\mathrm{Hom}(X, -) \colon C \to \mathrm{Type}$ that maps an object $Y$ in $C$ to the set of morphisms $\mathrm{Hom}(X, Y)$ in $C$, and a morphism $f \colon Y \to Y'$ in $C$ to the postcomposition map $f \circ (-) \colon \mathrm{Hom}(X, Y) \to \mathrm{Hom}(X, Y')$. For a morphism $f \colon X \to X'$ in $C^{\mathrm{op}}$, it sends $f$ to the natural transformation $\mathrm{Hom}(X', -) \Rightarrow \mathrm{Hom}(X, -)$ given by precomposition with $f$.

CategoryTheory.Yoneda.obj_map_id theorem

{X Y : C} (f : op X ⟶ op Y) : (yoneda.obj X).map f (𝟙 X) = (yoneda.map f.unop).app (op Y) (𝟙 Y)

Full source

theorem obj_map_id {X Y : C} (f : opop X ⟶ op Y) :
    (yoneda.obj X).map f (𝟙 X) = (yoneda.map f.unop).app (op Y) (𝟙 Y) := by
  dsimp
  simp

Yoneda Embedding Preserves Identity under Mapping

Informal description

For any objects $X$ and $Y$ in a category $C$ and any morphism $f \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, the application of the Yoneda embedding functor $\mathrm{y}$ satisfies: \[ (\mathrm{y}(X)).\mathrm{map}(f)(\mathrm{id}_X) = (\mathrm{y}(f^{\mathrm{unop}})).\mathrm{app}(\mathrm{op}(Y))(\mathrm{id}_Y) \] where $\mathrm{id}_X$ and $\mathrm{id}_Y$ are the identity morphisms on $X$ and $Y$ respectively, and $f^{\mathrm{unop}}$ is the morphism $f$ viewed in the original category $C$.

CategoryTheory.Yoneda.naturality theorem

 {X Y : C} (α : yoneda.obj X ⟶ yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) :
  f ≫ α.app (op Z') h = α.app (op Z) (f ≫ h)

Full source

@[simp]
theorem naturality {X Y : C} (α : yonedayoneda.obj X ⟶ yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z')
    (h : Z' ⟶ X) : f ≫ α.app (op Z') h = α.app (op Z) (f ≫ h) :=
  (FunctorToTypes.naturality _ _ α f.op h).symm

Naturality Condition for Yoneda Embedding

Informal description

For any objects $X, Y$ in a category $C$ and natural transformation $\alpha \colon \mathrm{y}(X) \Rightarrow \mathrm{y}(Y)$ between their Yoneda embeddings, and for any morphisms $f \colon Z \to Z'$ and $h \colon Z' \to X$ in $C$, the following diagram commutes: \[ f \circ \alpha_{Z'}(h) = \alpha_Z(f \circ h) \] where $\mathrm{y}(X) = \mathrm{Hom}(-, X)$ denotes the Yoneda embedding of $X$.

CategoryTheory.Yoneda.fullyFaithful definition

: (yoneda (C := C)).FullyFaithful

Full source

/-- The Yoneda embedding is fully faithful. -/
def fullyFaithful : (yoneda (C := C)).FullyFaithful where
  preimage f := f.app _ (𝟙 _)

Yoneda embedding is fully faithful

Informal description

The Yoneda embedding functor $\mathrm{y} \colon C \to C^{\mathrm{op}} \to \mathrm{Type}$ is fully faithful, meaning that for any objects $X, Y$ in $C$, the map $\mathrm{Hom}_C(X, Y) \to \mathrm{Hom}(\mathrm{y}(X), \mathrm{y}(Y))$ is bijective. Here $\mathrm{y}(X) = \mathrm{Hom}(-, X)$ is the contravariant hom-functor represented by $X$.

CategoryTheory.Yoneda.fullyFaithful_preimage theorem

{X Y : C} (f : yoneda.obj X ⟶ yoneda.obj Y) : fullyFaithful.preimage f = f.app (op X) (𝟙 X)

Full source

lemma fullyFaithful_preimage {X Y : C} (f : yonedayoneda.obj X ⟶ yoneda.obj Y) :
    fullyFaithful.preimage f = f.app (op X) (𝟙 X) := rfl

Preimage of Natural Transformation under Yoneda Embedding

Informal description

For any objects $X$ and $Y$ in a category $C$ and any natural transformation $f \colon \mathrm{Hom}(-, X) \Rightarrow \mathrm{Hom}(-, Y)$ between their Yoneda embeddings, the preimage of $f$ under the fully faithful Yoneda embedding is equal to $f_X(\mathrm{id}_X)$, where $f_X$ is the component of $f$ at $X$ and $\mathrm{id}_X$ is the identity morphism on $X$.

CategoryTheory.Yoneda.yoneda_full instance

: (yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁).Full

Full source

/-- The Yoneda embedding is full. -/
@[stacks 001P]
instance yoneda_full : (yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁).Full :=
  fullyFaithful.full

The Yoneda Embedding is Full

Informal description

The Yoneda embedding functor $\mathrm{y} \colon C \to C^{\mathrm{op}} \to \mathrm{Type}$ is full. That is, for any objects $X, Y$ in $C$, the map $\mathrm{Hom}_C(X, Y) \to \mathrm{Hom}(\mathrm{y}(X), \mathrm{y}(Y))$ is surjective, where $\mathrm{y}(X) = \mathrm{Hom}(-, X)$ is the contravariant hom-functor represented by $X$.

CategoryTheory.Yoneda.yoneda_faithful instance

: (yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁).Faithful

Full source

/-- The Yoneda embedding is faithful. -/
@[stacks 001P]
instance yoneda_faithful : (yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁).Faithful :=
  fullyFaithful.faithful

Faithfulness of the Yoneda Embedding

Informal description

The Yoneda embedding functor $\mathrm{y} \colon C \to C^{\mathrm{op}} \to \mathrm{Type}$ is faithful. That is, for any objects $X, Y$ in $C$, the map $\mathrm{Hom}_C(X, Y) \to \mathrm{Hom}(\mathrm{y}(X), \mathrm{y}(Y))$ is injective, where $\mathrm{y}(X) = \mathrm{Hom}(-, X)$ is the contravariant hom-functor represented by $X$.

CategoryTheory.Yoneda.ext definition

 (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 (f ≫ g) = f ≫ p g) : X ≅ Y

Full source

/-- 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`.
```
-/
def ext (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 (f ≫ g) = f ≫ p g) : X ≅ Y :=
  fullyFaithful.preimageIso
    (NatIso.ofComponents fun Z =>
      { hom := p
        inv := q })

Yoneda Extensionality Principle

Informal description

Given two objects $X$ and $Y$ in a category $\mathcal{C}$, and functions $p \colon \mathrm{Hom}(Z, X) \to \mathrm{Hom}(Z, Y)$ and $q \colon \mathrm{Hom}(Z, Y) \to \mathrm{Hom}(Z, X)$ for all objects $Z$ in $\mathcal{C}$, such that: 1. $q \circ p = \mathrm{id}$ on $\mathrm{Hom}(Z, X)$, 2. $p \circ q = \mathrm{id}$ on $\mathrm{Hom}(Z, Y)$, 3. $p$ is natural in $Z$ (i.e., $p(f \circ g) = f \circ p(g)$ for any morphisms $f \colon Z' \to Z$ and $g \colon Z \to X$), then $X$ and $Y$ are isomorphic in $\mathcal{C}$.

CategoryTheory.Yoneda.isIso theorem

{X Y : C} (f : X ⟶ Y) [IsIso (yoneda.map f)] : IsIso f

Full source

/-- If `yoneda.map f` is an isomorphism, so was `f`.
-/
theorem isIso {X Y : C} (f : X ⟶ Y) [IsIso (yoneda.map f)] : IsIso f :=
  isIso_of_fully_faithful yoneda f

Yoneda Embedding Reflects Isomorphisms

Informal description

Let $f \colon X \to Y$ be a morphism in a category $\mathcal{C}$. If the image of $f$ under the Yoneda embedding $\mathrm{y} \colon \mathcal{C} \to \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}$ is an isomorphism, then $f$ itself is an isomorphism in $\mathcal{C}$.

CategoryTheory.Coyoneda.naturality theorem

 {X Y : Cᵒᵖ} (α : coyoneda.obj X ⟶ coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z) (h : unop X ⟶ Z') :
  α.app Z' h ≫ f = α.app Z (h ≫ f)

Full source

@[simp]
theorem naturality {X Y : Cᵒᵖ} (α : coyonedacoyoneda.obj X ⟶ coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z)
    (h : unopunop X ⟶ Z') : α.app Z' h ≫ f = α.app Z (h ≫ f) :=
  (FunctorToTypes.naturality _ _ α f h).symm

Naturality Condition for the Co-Yoneda Embedding

Informal description

For any objects $X, Y$ in the opposite category $C^{\mathrm{op}}$ and any natural transformation $\alpha \colon \mathrm{coyoneda}(X) \to \mathrm{coyoneda}(Y)$, and for any morphisms $f \colon Z' \to Z$ in $C$ and $h \colon \mathrm{unop}(X) \to Z'$, the following diagram commutes: \[ \alpha_{Z'}(h) \circ f = \alpha_Z(h \circ f). \]

CategoryTheory.Coyoneda.fullyFaithful definition

: (coyoneda (C := C)).FullyFaithful

Full source

/-- The co-Yoneda embedding is fully faithful. -/
def fullyFaithful : (coyoneda (C := C)).FullyFaithful where
  preimage f := (f.app _ (𝟙 _)).op

Fully Faithfulness of the Co-Yoneda Embedding

Informal description

The co-Yoneda embedding functor is fully faithful, meaning it is both full and faithful. This implies that for any two objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$, the map $\mathrm{Hom}(X, Y) \to \mathrm{Hom}(\mathrm{coyoneda}(X), \mathrm{coyoneda}(Y))$ induced by the co-Yoneda embedding is bijective. In other words, the co-Yoneda embedding preserves and reflects morphisms in a one-to-one manner.

CategoryTheory.Coyoneda.fullyFaithful_preimage theorem

{X Y : Cᵒᵖ} (f : coyoneda.obj X ⟶ coyoneda.obj Y) : fullyFaithful.preimage f = (f.app X.unop (𝟙 X.unop)).op

Full source

lemma fullyFaithful_preimage {X Y : Cᵒᵖ} (f : coyonedacoyoneda.obj X ⟶ coyoneda.obj Y) :
    fullyFaithful.preimage f = (f.app X.unop (𝟙 X.unop)).op := rfl

Preimage of Natural Transformation under Co-Yoneda Embedding Equals Opposite of Identity Evaluation

Informal description

For any objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$ and any natural transformation $f \colon \mathrm{coyoneda}(X) \to \mathrm{coyoneda}(Y)$, the preimage of $f$ under the fully faithful co-Yoneda embedding is equal to the opposite of the morphism obtained by evaluating $f$ at the identity morphism on $X$ (viewed in $C$). That is, \[ \mathrm{fullyFaithful.preimage}(f) = (f_{X}(\mathrm{id}_X))^{\mathrm{op}}. \]

CategoryTheory.Coyoneda.preimage definition

{X Y : Cᵒᵖ} (f : coyoneda.obj X ⟶ coyoneda.obj Y) : X ⟶ Y

Full source

/-- The morphism `X ⟶ Y` corresponding to a natural transformation
`coyoneda.obj X ⟶ coyoneda.obj Y`. -/
def preimage {X Y : Cᵒᵖ} (f : coyonedacoyoneda.obj X ⟶ coyoneda.obj Y) : X ⟶ Y :=
  (f.app _ (𝟙 X.unop)).op

Morphism from natural transformation of co-Yoneda embeddings

Informal description

Given objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$ and a natural transformation $f$ between the co-Yoneda embeddings of $X$ and $Y$, the function returns the morphism $X \to Y$ in $C^{\mathrm{op}}$ corresponding to $f$. Specifically, it evaluates $f$ at the identity morphism on $X$ (viewed in $C$) and then takes the opposite morphism.

CategoryTheory.Coyoneda.coyoneda_full instance

: (coyoneda : Cᵒᵖ ⥤ C ⥤ Type v₁).Full

Full source

instance coyoneda_full : (coyoneda : CᵒᵖCᵒᵖ ⥤ C ⥤ Type v₁).Full :=
  fullyFaithful.full

Fullness of the Co-Yoneda Embedding

Informal description

The co-Yoneda embedding functor $\mathrm{coyoneda} \colon C^{\mathrm{op}} \to (C \to \mathrm{Type})$ is full. This means that for any two objects $X$ and $Y$ in $C^{\mathrm{op}}$, the map $\mathrm{Hom}(X, Y) \to \mathrm{Hom}(\mathrm{coyoneda}(X), \mathrm{coyoneda}(Y))$ induced by the co-Yoneda embedding is surjective. In other words, every natural transformation between the copresheaves $\mathrm{coyoneda}(X)$ and $\mathrm{coyoneda}(Y)$ arises from a morphism in $C^{\mathrm{op}}$.

CategoryTheory.Coyoneda.coyoneda_faithful instance

: (coyoneda : Cᵒᵖ ⥤ C ⥤ Type v₁).Faithful

Full source

instance coyoneda_faithful : (coyoneda : CᵒᵖCᵒᵖ ⥤ C ⥤ Type v₁).Faithful :=
  fullyFaithful.faithful

Faithfulness of the Co-Yoneda Embedding

Informal description

The co-Yoneda embedding functor $\mathrm{coyoneda} \colon C^{\mathrm{op}} \to (C \to \mathrm{Type})$ is faithful. This means that for any two objects $X$ and $Y$ in $C^{\mathrm{op}}$, the map $\mathrm{Hom}(X, Y) \to \mathrm{Hom}(\mathrm{coyoneda}(X), \mathrm{coyoneda}(Y))$ induced by the co-Yoneda embedding is injective. In other words, distinct morphisms in $C^{\mathrm{op}}$ are mapped to distinct natural transformations between the corresponding copresheaves.

CategoryTheory.Coyoneda.ext definition

 (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 (f ≫ g) = q f ≫ g) : X ≅ Y

Full source

/-- 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`.
```
-/
def ext (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 (f ≫ g) = q f ≫ g) : X ≅ Y :=
  fullyFaithful.preimageIso
    (NatIso.ofComponents (fun Z =>
      { hom := q
        inv := p })
    ) |>.unop

Extensionality via Co-Yoneda Embedding

Informal description

Given two objects $X$ and $Y$ in a category $\mathcal{C}$, and two families of functions $p_Z \colon \mathrm{Hom}(X, Z) \to \mathrm{Hom}(Y, Z)$ and $q_Z \colon \mathrm{Hom}(Y, Z) \to \mathrm{Hom}(X, Z)$ for all objects $Z$ in $\mathcal{C}$, such that: 1. $q_Z \circ p_Z = \mathrm{id}$ for all $f \in \mathrm{Hom}(X, Z)$, 2. $p_Z \circ q_Z = \mathrm{id}$ for all $f \in \mathrm{Hom}(Y, Z)$, 3. $q_Z(f \circ g) = q_Z(f) \circ g$ for all $f \in \mathrm{Hom}(Y, Z)$ and $g \in \mathrm{Hom}(Z, Z')$, then $X$ and $Y$ are isomorphic in $\mathcal{C}$.

CategoryTheory.Coyoneda.isIso theorem

{X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso (coyoneda.map f)] : IsIso f

Full source

/-- If `coyoneda.map f` is an isomorphism, so was `f`.
-/
theorem isIso {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso (coyoneda.map f)] : IsIso f :=
  isIso_of_fully_faithful coyoneda f

Reflection of Isomorphisms by the Co-Yoneda Embedding

Informal description

Let $C$ be a category and $f \colon X \to Y$ a morphism in its opposite category $C^{\mathrm{op}}$. If the induced natural transformation $\mathrm{coyoneda}(f) \colon \mathrm{coyoneda}(X) \Rightarrow \mathrm{coyoneda}(Y)$ is an isomorphism, then $f$ is an isomorphism in $C^{\mathrm{op}}$.

CategoryTheory.Coyoneda.punitIso definition

: coyoneda.obj (Opposite.op PUnit) ≅ 𝟭 (Type v₁)

Full source

/-- The identity functor on `Type` is isomorphic to the coyoneda functor coming from `PUnit`. -/
def punitIso : coyonedacoyoneda.obj (Opposite.op PUnit) ≅ 𝟭 (Type v₁) :=
  NatIso.ofComponents fun X =>
    { hom := fun f => f ⟨⟩
      inv := fun x _ => x }

Isomorphism between identity functor and co-Yoneda on PUnit

Informal description

The identity functor on the category of types is isomorphic to the co-Yoneda functor applied to the terminal object $\mathrm{PUnit}$. Specifically, for any type $X$, the isomorphism consists of: - A natural transformation $\mathrm{hom}$ that evaluates a function $f \colon \mathrm{Hom}(\mathrm{PUnit}, X)$ at the unique element $\langle \rangle \in \mathrm{PUnit}$. - An inverse natural transformation $\mathrm{inv}$ that sends any element $x \in X$ to the constant function $\mathrm{Hom}(\mathrm{PUnit}, X)$ mapping every element of $\mathrm{PUnit}$ to $x$.

CategoryTheory.Coyoneda.objOpOp definition

(X : C) : coyoneda.obj (op (op X)) ≅ yoneda.obj X

Full source

/-- Taking the `unop` of morphisms is a natural isomorphism. -/
@[simps!]
def objOpOp (X : C) : coyonedacoyoneda.obj (op (op X)) ≅ yoneda.obj X :=
  NatIso.ofComponents fun _ => (opEquiv _ _).toIso

Isomorphism between co-Yoneda on double opposite and Yoneda

Informal description

For any object $X$ in a category $\mathcal{C}$, there is a natural isomorphism between the co-Yoneda functor applied to the double opposite of $X$ (i.e., $\text{op}(\text{op}(X))$) and the Yoneda functor applied to $X$. This isomorphism is constructed using the equivalence between morphisms in the opposite category and the original category.

CategoryTheory.Coyoneda.opIso definition

: yoneda ⋙ (whiskeringLeft _ _ _).obj (opOp C) ≅ coyoneda

Full source

/-- Taking the `unop` of morphisms is a natural isomorphism. -/
def opIso : yonedayoneda ⋙ (whiskeringLeft _ _ _).obj (opOp C)yoneda ⋙ (whiskeringLeft _ _ _).obj (opOp C) ≅ coyoneda :=
  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ (opEquiv (op Y) X).toIso)
    (fun _ ↦ rfl)) (fun _ ↦ rfl)

Isomorphism between Yoneda composed with double opposite and co-Yoneda

Informal description

The natural isomorphism between the composition of the Yoneda embedding functor with the left whiskering of the double opposite functor and the co-Yoneda embedding functor. Specifically, for any object $X$ in the category $C$, this isomorphism provides a natural equivalence between the functors $\text{yoneda} \circ \text{opOp}$ and $\text{coyoneda}$.

CategoryTheory.Functor.RepresentableBy structure

(F : Cᵒᵖ ⥤ Type v) (Y : C)

Full source

/-- The data which expresses that a functor `F : Cᵒᵖ ⥤ Type v` is representable by `Y : C`. -/
structure RepresentableBy (F : CᵒᵖCᵒᵖ ⥤ Type v) (Y : C) where
  /-- the natural bijection `(X ⟶ Y) ≃ F.obj (op X)`. -/
  homEquiv {X : C} : (X ⟶ Y) ≃ F.obj (op X)
  homEquiv_comp {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y) :
    homEquiv (f ≫ g) = F.map f.op (homEquiv g)

Representable Functor

Informal description

The structure `RepresentableBy` expresses that a contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ is representable by an object $Y$ in category $C$. This means there exists a natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}_C(-, Y)$.

CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm theorem

 {F : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (op X')) (f : X ⟶ X') :
  f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x)

Full source

lemma RepresentableBy.comp_homEquiv_symm {F : CᵒᵖCᵒᵖ ⥤ Type v} {Y : C}
    (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (op X')) (f : X ⟶ X') :
    f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x) :=
  e.homEquiv.injective (by simp [homEquiv_comp])

Naturality of Representable Functor's Hom-Equivalence Inverse

Informal description

Let $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ be a contravariant functor representable by an object $Y \in C$, with a natural isomorphism $e \colon F \cong \mathrm{Hom}_C(-, Y)$. Then for any objects $X, X' \in C$, any element $x \in F(X')$, and any morphism $f \colon X \to X'$, the following diagram commutes: $$ f \circ e^{-1}_{X'}(x) = e^{-1}_X(F(f^{\mathrm{op}})(x)) $$ where $e^{-1}$ denotes the inverse of the natural isomorphism $e$.

CategoryTheory.Functor.RepresentableBy.ofIso definition

{F F' : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) (e' : F ≅ F') : F'.RepresentableBy Y

Full source

/-- If `F ≅ F'`, and `F` is representable, then `F'` is representable. -/
def RepresentableBy.ofIso {F F' : CᵒᵖCᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) (e' : F ≅ F') :
    F'.RepresentableBy Y where
  homEquiv {X} := e.homEquiv.trans (e'.app _).toEquiv
  homEquiv_comp {X X'} f g := by
    dsimp
    rw [e.homEquiv_comp]
    apply congr_fun (e'.hom.naturality f.op)

Representability preserved under natural isomorphism

Informal description

Given two contravariant functors $F, F' \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ and an object $Y$ in $C$, if $F$ is representable by $Y$ and there exists a natural isomorphism $F \cong F'$, then $F'$ is also representable by $Y$. More precisely, the representability of $F'$ is established via the composition of the natural isomorphism $F \cong F'$ with the original representability data of $F$. The hom-equivalence for $F'$ is given by the composition of the hom-equivalence for $F$ with the component of the natural isomorphism at each object $X$ in $C^{\mathrm{op}}$.

CategoryTheory.Functor.CorepresentableBy structure

(F : C ⥤ Type v) (X : C)

Full source

/-- The data which expresses that a functor `F : C ⥤ Type v` is corepresentable by `X : C`. -/
structure CorepresentableBy (F : C ⥤ Type v) (X : C) where
  /-- the natural bijection `(X ⟶ Y) ≃ F.obj Y`. -/
  homEquiv {Y : C} : (X ⟶ Y) ≃ F.obj Y
  homEquiv_comp {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y) :
    homEquiv (f ≫ g) = F.map g (homEquiv f)

Corepresentable Functor

Informal description

The structure `CorepresentableBy` expresses that a functor $F \colon C \to \mathrm{Type}_v$ is corepresentable by an object $X \in C$. This means there exists a natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}(X, -)$, providing a way to represent $F$ in terms of morphisms out of $X$.

CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp theorem

 {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') :
  e.homEquiv.symm y ≫ g = e.homEquiv.symm (F.map g y)

Full source

lemma CorepresentableBy.homEquiv_symm_comp {F : C ⥤ Type v} {X : C}
    (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') :
    e.homEquiv.symm y ≫ g = e.homEquiv.symm (F.map g y) :=
  e.homEquiv.injective (by simp [homEquiv_comp])

Naturality of Corepresentation Isomorphism Inverse

Informal description

Let $F \colon C \to \mathrm{Type}_v$ be a functor corepresentable by an object $X \in C$, with corepresentation isomorphism $e \colon F \cong \mathrm{Hom}(X, -)$. For any objects $Y, Y' \in C$, element $y \in F(Y)$, and morphism $g \colon Y \to Y'$, the following diagram commutes: $$ e^{-1}(y) \circ g = e^{-1}(F(g)(y)) $$ where $e^{-1}$ denotes the inverse of the natural isomorphism $e$.

CategoryTheory.Functor.CorepresentableBy.ofIso definition

{F F' : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) (e' : F ≅ F') : F'.CorepresentableBy X

Full source

/-- If `F ≅ F'`, and `F` is corepresentable, then `F'` is corepresentable. -/
def CorepresentableBy.ofIso {F F' : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X)
    (e' : F ≅ F') :
    F'.CorepresentableBy X where
  homEquiv {X} := e.homEquiv.trans (e'.app _).toEquiv
  homEquiv_comp {Y Y'} g f := by
    dsimp
    rw [e.homEquiv_comp]
    apply congr_fun (e'.hom.naturality g)

Corepresentability Preservation under Natural Isomorphism

Informal description

Given functors $F, F' \colon C \to \mathrm{Type}_v$ and an object $X \in C$, if $F$ is corepresentable by $X$ and there exists a natural isomorphism $F \cong F'$, then $F'$ is also corepresentable by $X$. Specifically, the hom-equivalence for $F'$ is obtained by composing the hom-equivalence for $F$ with the equivalence induced by the natural isomorphism $F \cong F'$.

CategoryTheory.Functor.RepresentableBy.homEquiv_eq theorem

 {F : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y) : e.homEquiv f = F.map f.op (e.homEquiv (𝟙 Y))

Full source

lemma RepresentableBy.homEquiv_eq {F : CᵒᵖCᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y)
    {X : C} (f : X ⟶ Y) :
    e.homEquiv f = F.map f.op (e.homEquiv (𝟙 Y)) := by
  conv_lhs => rw [← Category.comp_id f, e.homEquiv_comp]

Hom-Equivalence Property for Representable Functors

Informal description

Let $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ be a contravariant functor representable by an object $Y \in C$, with representation isomorphism $e \colon F \cong \mathrm{Hom}_C(-, Y)$. For any object $X \in C$ and morphism $f \colon X \to Y$, the hom-equivalence satisfies: $$ e(f) = F(f^{\mathrm{op}})(e(1_Y)) $$ where $f^{\mathrm{op}}$ denotes the corresponding morphism in $C^{\mathrm{op}}$ and $1_Y$ is the identity morphism on $Y$.

CategoryTheory.Functor.CorepresentableBy.homEquiv_eq theorem

 {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y) : e.homEquiv f = F.map f (e.homEquiv (𝟙 X))

Full source

lemma CorepresentableBy.homEquiv_eq {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X)
    {Y : C} (f : X ⟶ Y) :
    e.homEquiv f = F.map f (e.homEquiv (𝟙 X)) := by
  conv_lhs => rw [← Category.id_comp f, e.homEquiv_comp]

Hom-Equivalence Property for Corepresentable Functors

Informal description

Let $F \colon C \to \mathrm{Type}_v$ be a functor corepresentable by an object $X \in C$, and let $f \colon X \to Y$ be a morphism in $C$. Then the hom-equivalence $e.\mathrm{homEquiv}(f)$ is equal to the image of $f$ under $F$ applied to the hom-equivalence of the identity morphism on $X$, i.e., \[ e.\mathrm{homEquiv}(f) = F(f)(e.\mathrm{homEquiv}(1_X)). \]

CategoryTheory.Functor.RepresentableBy.uniqueUpToIso definition

{F : Cᵒᵖ ⥤ Type v} {Y Y' : C} (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y') : Y ≅ Y'

Full source

/-- Representing objects are unique up to isomorphism. -/
@[simps!]
def RepresentableBy.uniqueUpToIso {F : CᵒᵖCᵒᵖ ⥤ Type v} {Y Y' : C} (e : F.RepresentableBy Y)
    (e' : F.RepresentableBy Y') : Y ≅ Y' :=
  let ε {X} := (@e.homEquiv X).trans e'.homEquiv.symm
  Yoneda.ext _ _ ε ε.symm (by simp) (by simp)
    (by simp [ε, comp_homEquiv_symm, homEquiv_comp])

Uniqueness of representing objects up to isomorphism

Informal description

Given two objects $Y$ and $Y'$ in a category $\mathcal{C}$ that both represent the same contravariant functor $F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}_v$, there exists an isomorphism between $Y$ and $Y'$. More precisely, if $e \colon F \cong \mathrm{Hom}_{\mathcal{C}}(-, Y)$ and $e' \colon F \cong \mathrm{Hom}_{\mathcal{C}}(-, Y')$ are natural isomorphisms, then $Y$ and $Y'$ are isomorphic in $\mathcal{C}$.

CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso definition

{F : C ⥤ Type v} {X X' : C} (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X') : X ≅ X'

Full source

/-- Corepresenting objects are unique up to isomorphism. -/
@[simps!]
def CorepresentableBy.uniqueUpToIso {F : C ⥤ Type v} {X X' : C} (e : F.CorepresentableBy X)
    (e' : F.CorepresentableBy X') : X ≅ X' :=
  let ε {Y} := (@e.homEquiv Y).trans e'.homEquiv.symm
  Coyoneda.ext _ _ ε ε.symm (by simp) (by simp)
    (by simp [ε, homEquiv_symm_comp, homEquiv_comp])

Uniqueness of corepresenting objects up to isomorphism

Informal description

Given a functor $F \colon C \to \mathrm{Type}_v$ and two objects $X, X' \in C$ such that $F$ is corepresentable by both $X$ and $X'$, there exists an isomorphism $X \cong X'$ in the category $C$. This isomorphism is constructed using the natural equivalence between the hom-functors $\mathrm{Hom}(X, -)$ and $\mathrm{Hom}(X', -)$ induced by the corepresentability of $F$.

CategoryTheory.Functor.RepresentableBy.ext theorem

{F : Cᵒᵖ ⥤ Type v} {Y : C} {e e' : F.RepresentableBy Y} (h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)) : e = e'

Full source

@[ext]
lemma RepresentableBy.ext {F : CᵒᵖCᵒᵖ ⥤ Type v} {Y : C} {e e' : F.RepresentableBy Y}
    (h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)) : e = e' := by
  have : ∀ {X : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]
  obtain ⟨e, he⟩ := e
  obtain ⟨e', he'⟩ := e'
  obtain rfl : @e = @e' := by ext; apply this
  rfl

Uniqueness of Representability Witness via Identity Morphism

Informal description

Let $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ be a contravariant functor representable by an object $Y \in C$, and let $e, e' \colon F \cong \mathrm{Hom}_C(-, Y)$ be two representation isomorphisms. If $e$ and $e'$ agree on the identity morphism $1_Y$, i.e., $e(1_Y) = e'(1_Y)$, then $e = e'$.

CategoryTheory.Functor.CorepresentableBy.ext theorem

{F : C ⥤ Type v} {X : C} {e e' : F.CorepresentableBy X} (h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)) : e = e'

Full source

@[ext]
lemma CorepresentableBy.ext {F : C ⥤ Type v} {X : C} {e e' : F.CorepresentableBy X}
    (h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)) : e = e' := by
  have : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]
  obtain ⟨e, he⟩ := e
  obtain ⟨e', he'⟩ := e'
  obtain rfl : @e = @e' := by ext; apply this
  rfl

Uniqueness of Corepresentability Witness via Identity Morphism

Informal description

Let $F \colon C \to \mathrm{Type}_v$ be a functor corepresentable by an object $X \in C$, and let $e, e' \colon F \cong \mathrm{Hom}_C(X, -)$ be two corepresentation isomorphisms. If $e$ and $e'$ agree on the identity morphism $1_X$, i.e., $e(1_X) = e'(1_X)$, then $e = e'$.

CategoryTheory.Functor.representableByEquiv definition

{F : Cᵒᵖ ⥤ Type v₁} {Y : C} : F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)

Full source

/-- The obvious bijection `F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)`
when `F : Cᵒᵖ ⥤ Type v₁` and `[Category.{v₁} C]`. -/
def representableByEquiv {F : CᵒᵖCᵒᵖ ⥤ Type v₁} {Y : C} :
    F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F) where
  toFun r := NatIso.ofComponents (fun _ ↦ r.homEquiv.toIso) (fun {X X'} f ↦ by
    ext g
    simp [r.homEquiv_comp])
  invFun e :=
    { homEquiv := (e.app _).toEquiv
      homEquiv_comp := fun {X X'} f g ↦ congr_fun (e.hom.naturality f.op) g }
  left_inv _ := rfl
  right_inv _ := rfl

Bijection between representability and Yoneda isomorphism

Informal description

For any contravariant functor $ F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}_{v_1} $ and any object $ Y $ in a category $ \mathcal{C} $, there is a natural bijection between the structure $ F.\mathrm{RepresentableBy}\ Y $ (which asserts that $ F $ is representable by $ Y $) and the set of natural isomorphisms $ \mathrm{Hom}_{\mathcal{C}}(-, Y) \cong F $. Here: - $ \mathrm{Hom}_{\mathcal{C}}(-, Y) $ is the Yoneda embedding of $ Y $, i.e., the contravariant functor sending an object $ X $ to the set $ \mathrm{Hom}_{\mathcal{C}}(X, Y) $. - The bijection is constructed explicitly, mapping a representability witness $ r $ to a natural isomorphism whose components are induced by $ r.\mathrm{homEquiv} $, and vice versa.

CategoryTheory.Functor.RepresentableBy.toIso definition

{F : Cᵒᵖ ⥤ Type v₁} {Y : C} (e : F.RepresentableBy Y) : yoneda.obj Y ≅ F

Full source

/-- The isomorphism `yoneda.obj Y ≅ F` induced by `e : F.RepresentableBy Y`. -/
def RepresentableBy.toIso {F : CᵒᵖCᵒᵖ ⥤ Type v₁} {Y : C} (e : F.RepresentableBy Y) :
    yonedayoneda.obj Y ≅ F :=
  representableByEquiv e

Natural isomorphism induced by representability

Informal description

Given a contravariant functor $ F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}_{v_1} $ and an object $ Y $ in a category $ \mathcal{C} $, if $ F $ is representable by $ Y $ (i.e., there exists a natural isomorphism between $ F $ and the hom-functor $\mathrm{Hom}_{\mathcal{C}}(-, Y)$), then this definition constructs the explicit natural isomorphism $ \mathrm{Hom}_{\mathcal{C}}(-, Y) \cong F $.

CategoryTheory.Functor.corepresentableByEquiv definition

{F : C ⥤ Type v₁} {X : C} : F.CorepresentableBy X ≃ (coyoneda.obj (op X) ≅ F)

Full source

/-- The obvious bijection `F.CorepresentableBy X ≃ (yoneda.obj Y ≅ F)`
when `F : C ⥤ Type v₁` and `[Category.{v₁} C]`. -/
def corepresentableByEquiv {F : C ⥤ Type v₁} {X : C} :
    F.CorepresentableBy X ≃ (coyoneda.obj (op X) ≅ F) where
  toFun r := NatIso.ofComponents (fun _ ↦ r.homEquiv.toIso) (fun {X X'} f ↦ by
    ext g
    simp [r.homEquiv_comp])
  invFun e :=
    { homEquiv := (e.app _).toEquiv
      homEquiv_comp := fun {X X'} f g ↦ congr_fun (e.hom.naturality f) g }
  left_inv _ := rfl
  right_inv _ := rfl

Bijection between corepresentability and co-Yoneda isomorphism

Informal description

For any covariant functor $ F \colon \mathcal{C} \to \mathrm{Type}_{v_1} $ and any object $ X $ in a category $ \mathcal{C} $, there is a natural bijection between the structure $ F.\mathrm{CorepresentableBy}\ X $ (which asserts that $ F $ is corepresentable by $ X $) and the set of natural isomorphisms $ \mathrm{Hom}_{\mathcal{C}}(X, -) \cong F $. Here: - $ \mathrm{Hom}_{\mathcal{C}}(X, -) $ is the co-Yoneda embedding of $ X $, i.e., the covariant functor sending an object $ Y $ to the set $ \mathrm{Hom}_{\mathcal{C}}(X, Y) $. - The bijection is constructed explicitly, mapping a corepresentability witness $ r $ to a natural isomorphism whose components are induced by $ r.\mathrm{homEquiv} $, and vice versa.

CategoryTheory.Functor.CorepresentableBy.toIso definition

{F : C ⥤ Type v₁} {X : C} (e : F.CorepresentableBy X) : coyoneda.obj (op X) ≅ F

Full source

/-- The isomorphism `coyoneda.obj (op X) ≅ F` induced by `e : F.CorepresentableBy X`. -/
def CorepresentableBy.toIso {F : C ⥤ Type v₁} {X : C} (e : F.CorepresentableBy X) :
    coyonedacoyoneda.obj (op X) ≅ F :=
  corepresentableByEquiv e

Natural isomorphism induced by corepresentability

Informal description

Given a covariant functor $ F \colon \mathcal{C} \to \mathrm{Type}_{v_1} $ and an object $ X $ in a category $ \mathcal{C} $, if $ F $ is corepresentable by $ X $, then this definition constructs the explicit natural isomorphism $ \mathrm{Hom}_{\mathcal{C}}(X, -) \cong F $. Here: - $ \mathrm{Hom}_{\mathcal{C}}(X, -) $ is the co-Yoneda embedding of $ X $, i.e., the covariant functor sending an object $ Y $ to the set $ \mathrm{Hom}_{\mathcal{C}}(X, Y) $. - The isomorphism is constructed via the bijection between corepresentability and co-Yoneda isomorphism.

CategoryTheory.Functor.IsRepresentable structure

(F : Cᵒᵖ ⥤ Type v)

Full source

/-- 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 001Q]
class IsRepresentable (F : CᵒᵖCᵒᵖ ⥤ Type v) : Prop where
  has_representation : ∃ (Y : C), Nonempty (F.RepresentableBy Y)

Representable Functor

Informal description

A contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ is called representable if there exists an object $Y$ in $C$ and a natural isomorphism between the Yoneda embedding $\mathrm{y}(Y)$ and $F$, where $\mathrm{y}(Y)(X) = \mathrm{Hom}(X, Y)$. This means that for every object $X$ in $C$, there is a bijection $\mathrm{Hom}(X, Y) \simeq F(X)$ that is natural in $X$.

CategoryTheory.Functor.RepresentableBy.isRepresentable theorem

{F : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) : F.IsRepresentable

Full source

lemma RepresentableBy.isRepresentable {F : CᵒᵖCᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) :
    F.IsRepresentable where
  has_representation := ⟨Y, ⟨e⟩⟩

Representability of Functors Representable by an Object

Informal description

Given a contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$ and an object $Y$ in $C$, if $F$ is representable by $Y$ (i.e., there exists a natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}_C(-, Y)$), then $F$ is representable.

CategoryTheory.Functor.IsRepresentable.mk' theorem

{F : Cᵒᵖ ⥤ Type v₁} {X : C} (e : yoneda.obj X ≅ F) : F.IsRepresentable

Full source

/-- Alternative constructor for `F.IsRepresentable`, which takes as an input an
isomorphism `yoneda.obj X ≅ F`. -/
lemma IsRepresentable.mk' {F : CᵒᵖCᵒᵖ ⥤ Type v₁} {X : C} (e : yonedayoneda.obj X ≅ F) :
    F.IsRepresentable :=
  (representableByEquiv.symm e).isRepresentable

Representability via Yoneda Isomorphism

Informal description

Given a contravariant functor $F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}$ and an object $X$ in $\mathcal{C}$, if there exists a natural isomorphism between the Yoneda embedding $\mathrm{Hom}_{\mathcal{C}}(-, X)$ and $F$, then $F$ is representable.

CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda instance

{X : C} : IsRepresentable (yoneda.obj X)

Full source

instance {X : C} : IsRepresentable (yoneda.obj X) :=
  IsRepresentable.mk' (Iso.refl _)

Representability of the Yoneda Embedding

Informal description

For any object $X$ in a category $C$, the Yoneda embedding $\mathrm{y}(X) = \mathrm{Hom}_C(-, X)$ is a representable functor from $C^{\mathrm{op}}$ to $\mathrm{Type}$.

CategoryTheory.Functor.IsCorepresentable structure

(F : C ⥤ Type v)

Full source

/-- A functor `F : C ⥤ Type v₁` is corepresentable if there is object `X` so `F ≅ coyoneda.obj X`.
-/
@[stacks 001Q]
class IsCorepresentable (F : C ⥤ Type v) : Prop where
  has_corepresentation : ∃ (X : C), Nonempty (F.CorepresentableBy X)

Corepresentable Functor

Informal description

A functor $F \colon C \to \mathrm{Type}_v$ is called *corepresentable* if there exists an object $X$ in $C$ such that $F$ is naturally isomorphic to the functor $\mathrm{coyoneda}(X)$, where $\mathrm{coyoneda} \colon C \to (C^{\mathrm{op}} \to \mathrm{Type}_v)$ is the Yoneda embedding for the opposite category.

CategoryTheory.Functor.CorepresentableBy.isCorepresentable theorem

{F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) : F.IsCorepresentable

Full source

lemma CorepresentableBy.isCorepresentable {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) :
    F.IsCorepresentable where
  has_corepresentation := ⟨X, ⟨e⟩⟩

Corepresentability via Natural Isomorphism to Hom-Functor

Informal description

Given a functor $F \colon C \to \mathrm{Type}_v$ and an object $X \in C$, if there exists a natural isomorphism $e$ between $F$ and the hom-functor $\mathrm{Hom}(X, -)$, then $F$ is corepresentable.

CategoryTheory.Functor.IsCorepresentable.mk' theorem

{F : C ⥤ Type v₁} {X : C} (e : coyoneda.obj (op X) ≅ F) : F.IsCorepresentable

Full source

/-- Alternative constructor for `F.IsCorepresentable`, which takes as an input an
isomorphism `coyoneda.obj (op X) ≅ F`. -/
lemma IsCorepresentable.mk' {F : C ⥤ Type v₁} {X : C} (e : coyonedacoyoneda.obj (op X) ≅ F) :
    F.IsCorepresentable :=
  (corepresentableByEquiv.symm e).isCorepresentable

Corepresentability via Co-Yoneda Isomorphism

Informal description

Given a functor $F \colon C \to \mathrm{Type}$ and an object $X$ in $C$, if there exists a natural isomorphism between the co-Yoneda embedding $\mathrm{Hom}(X, -)$ and $F$, then $F$ is corepresentable.

CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda instance

{X : Cᵒᵖ} : IsCorepresentable (coyoneda.obj X)

Full source

instance {X : Cᵒᵖ} : IsCorepresentable (coyoneda.obj X) :=
  IsCorepresentable.mk' (Iso.refl _)

Corepresentability of the Co-Yoneda Embedding Functor

Informal description

For any object $X$ in the opposite category $C^{\mathrm{op}}$, the functor $\mathrm{coyoneda}(X) \colon C \to \mathrm{Type}$ is corepresentable. Here, $\mathrm{coyoneda}(X)$ is the functor that sends an object $Y$ in $C$ to the set of morphisms $\mathrm{Hom}_{C^{\mathrm{op}}}(X, Y) = \mathrm{Hom}_C(Y, X)$.

CategoryTheory.Functor.reprX definition

: C

Full source

/-- The representing object for the representable functor `F`. -/
noncomputable def reprX : C :=
  hF.has_representation.choose

Representing object of a representable functor

Informal description

The object $X$ in category $C$ that represents the representable functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$, meaning there exists a natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}_C(-, X)$.

CategoryTheory.Functor.representableBy definition

: F.RepresentableBy F.reprX

Full source

/-- A chosen term in `F.RepresentableBy (reprX F)` when `F.IsRepresentable` holds. -/
noncomputable def representableBy : F.RepresentableBy F.reprX :=
  hF.has_representation.choose_spec.some

Representation of a representable functor

Informal description

Given a representable contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$, this is a chosen natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}_C(-, X)$, where $X$ is the representing object of $F$.

CategoryTheory.Functor.RepresentableBy.isoReprX definition

{Y : C} (e : F.RepresentableBy Y) : Y ≅ F.reprX

Full source

/-- Any representing object for a representable functor `F` is isomorphic to `reprX F`. -/
noncomputable def RepresentableBy.isoReprX {Y : C} (e : F.RepresentableBy Y) :
    Y ≅ F.reprX :=
  RepresentableBy.uniqueUpToIso e (representableBy F)

Isomorphism between representing objects of a representable functor

Informal description

Given a representable contravariant functor $ F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}_v $ and an object $ Y $ in $ \mathcal{C} $ that represents $ F $, there exists an isomorphism between $ Y $ and the canonical representing object $ F.\mathrm{reprX} $ of $ F $.

CategoryTheory.Functor.reprx definition

: F.obj (op F.reprX)

Full source

/-- The representing element for the representable functor `F`, sometimes called the universal
element of the functor.
-/
noncomputable def reprx : F.obj (op F.reprX) :=
  F.representableBy.homEquiv (𝟙 _)

Universal element of a representable functor

Informal description

The universal element of a representable functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_v$, which is an element of $F(X)$ where $X$ is the representing object of $F$. This element corresponds to the identity morphism on $X$ via the Yoneda lemma.

CategoryTheory.Functor.reprW definition

(F : Cᵒᵖ ⥤ Type v₁) [F.IsRepresentable] : yoneda.obj F.reprX ≅ F

Full source

/-- 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`.
-/
noncomputable def reprW (F : CᵒᵖCᵒᵖ ⥤ Type v₁) [F.IsRepresentable] :
    yonedayoneda.obj F.reprX ≅ F := F.representableBy.toIso

Natural isomorphism for a representable functor

Informal description

Given a representable contravariant functor $ F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}_{v_1} $, this is the natural isomorphism between the Yoneda embedding of the representing object $ F.\mathrm{reprX} $ and the functor $ F $ itself. Specifically, it provides for each object $ X $ in $ \mathcal{C}^{\mathrm{op}} $ an isomorphism between the hom-set $ \mathrm{Hom}(X, F.\mathrm{reprX}) $ and $ F(X) $, natural in $ X $.

CategoryTheory.Functor.reprW_hom_app theorem

 (F : Cᵒᵖ ⥤ Type v₁) [F.IsRepresentable] (X : Cᵒᵖ) (f : unop X ⟶ F.reprX) : F.reprW.hom.app X f = F.map f.op F.reprx

Full source

theorem reprW_hom_app (F : CᵒᵖCᵒᵖ ⥤ Type v₁) [F.IsRepresentable]
    (X : Cᵒᵖ) (f : unopunop X ⟶ F.reprX) :
    F.reprW.hom.app X f = F.map f.op F.reprx := by
  apply RepresentableBy.homEquiv_eq

Naturality of the Yoneda Isomorphism for Representable Functors

Informal description

Let $F \colon \mathcal{C}^{\mathrm{op}} \to \mathrm{Type}_{v_1}$ be a representable functor, with representing object $Y \in \mathcal{C}$ and universal element $x \in F(Y)$. For any object $X \in \mathcal{C}^{\mathrm{op}}$ and morphism $f \colon \mathrm{unop}(X) \to Y$ in $\mathcal{C}$, the application of the natural isomorphism $F.\mathrm{reprW}.\mathrm{hom}$ at $X$ to $f$ is equal to the image of $x$ under the map $F(f^{\mathrm{op}})$, i.e., $$ F.\mathrm{reprW}.\mathrm{hom}_X(f) = F(f^{\mathrm{op}})(x). $$

CategoryTheory.Functor.coreprX definition

: C

Full source

/-- The representing object for the corepresentable functor `F`. -/
noncomputable def coreprX : C :=
  hF.has_corepresentation.choose

Representing object of a corepresentable functor

Informal description

Given a corepresentable functor $F \colon C \to \mathrm{Type}_v$, the object $\mathrm{coreprX}$ is the representing object of $F$, meaning there exists a natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}(\mathrm{coreprX}, -)$.

CategoryTheory.Functor.corepresentableBy definition

: F.CorepresentableBy F.coreprX

Full source

/-- A chosen term in `F.CorepresentableBy (coreprX F)` when `F.IsCorepresentable` holds. -/
noncomputable def corepresentableBy : F.CorepresentableBy F.coreprX :=
  hF.has_corepresentation.choose_spec.some

Corepresentation of a corepresentable functor

Informal description

Given a corepresentable functor $F \colon C \to \mathrm{Type}_v$, the term $\mathrm{corepresentableBy}$ is a chosen natural isomorphism between $F$ and the hom-functor $\mathrm{Hom}(\mathrm{coreprX}, -)$, where $\mathrm{coreprX}$ is the representing object of $F$.

CategoryTheory.Functor.CorepresentableBy.isoCoreprX definition

{Y : C} (e : F.CorepresentableBy Y) : Y ≅ F.coreprX

Full source

/-- Any corepresenting object for a corepresentable functor `F` is isomorphic to `coreprX F`. -/
noncomputable def CorepresentableBy.isoCoreprX {Y : C} (e : F.CorepresentableBy Y) :
    Y ≅ F.coreprX :=
  CorepresentableBy.uniqueUpToIso e (corepresentableBy F)

Isomorphism between corepresenting objects of a functor

Informal description

Given a functor $ F \colon \mathcal{C} \to \mathrm{Type}_v $ and an object $ Y \in \mathcal{C} $ such that $ F $ is corepresentable by $ Y $, there exists an isomorphism $ Y \cong F.\mathrm{coreprX} $ in the category $ \mathcal{C} $. Here, $ F.\mathrm{coreprX} $ is the chosen representing object of $ F $.

CategoryTheory.Functor.coreprx definition

: F.obj F.coreprX

Full source

/-- The representing element for the corepresentable functor `F`, sometimes called the universal
element of the functor.
-/
noncomputable def coreprx : F.obj F.coreprX :=
  F.corepresentableBy.homEquiv (𝟙 _)

Universal element of a corepresentable functor

Informal description

Given a corepresentable functor $F \colon C \to \mathrm{Type}_v$, the element $\mathrm{coreprx}$ is the universal element of $F$ in $F(\mathrm{coreprX})$, where $\mathrm{coreprX}$ is the representing object of $F$. This element corresponds to the identity morphism on $\mathrm{coreprX}$ via the natural isomorphism $\mathrm{corepresentableBy}$ between $F$ and the hom-functor $\mathrm{Hom}(\mathrm{coreprX}, -)$.

CategoryTheory.Functor.coreprW definition

(F : C ⥤ Type v₁) [F.IsCorepresentable] : coyoneda.obj (op F.coreprX) ≅ F

Full source

/-- 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`.
-/
noncomputable def coreprW (F : C ⥤ Type v₁) [F.IsCorepresentable] :
    coyonedacoyoneda.obj (op F.coreprX) ≅ F :=
  F.corepresentableBy.toIso

Natural isomorphism for a corepresentable functor

Informal description

Given a corepresentable functor $ F \colon \mathcal{C} \to \mathrm{Type}_{v_1} $, the natural isomorphism $ \mathrm{Hom}_{\mathcal{C}}(F.\mathrm{coreprX}, -) \cong F $ is constructed, where $ F.\mathrm{coreprX} $ is the representing object of $ F $. This isomorphism is obtained via the corepresentability data of $ F $.

CategoryTheory.Functor.coreprW_hom_app theorem

(F : C ⥤ Type v₁) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) : F.coreprW.hom.app X f = F.map f F.coreprx

Full source

theorem coreprW_hom_app (F : C ⥤ Type v₁) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) :
    F.coreprW.hom.app X f = F.map f F.coreprx := by
  apply CorepresentableBy.homEquiv_eq

Naturality of Universal Element in Corepresentable Functor

Informal description

Let $F \colon C \to \mathrm{Type}_{v_1}$ be a corepresentable functor with representing object $F.\mathrm{coreprX}$ and universal element $F.\mathrm{coreprx} \in F(F.\mathrm{coreprX})$. For any object $X \in C$ and morphism $f \colon F.\mathrm{coreprX} \to X$, the component of the natural isomorphism $F.\mathrm{coreprW}.\mathrm{hom}$ at $X$ applied to $f$ equals the image of $F.\mathrm{coreprx}$ under $F(f)$, i.e., \[ F.\mathrm{coreprW}.\mathrm{hom}.app_X(f) = F(f)(F.\mathrm{coreprx}). \]

CategoryTheory.isRepresentable_of_natIso theorem

(F : Cᵒᵖ ⥤ Type v₁) {G} (i : F ≅ G) [F.IsRepresentable] : G.IsRepresentable

Full source

theorem isRepresentable_of_natIso (F : CᵒᵖCᵒᵖ ⥤ Type v₁) {G} (i : F ≅ G) [F.IsRepresentable] :
    G.IsRepresentable :=
  (F.representableBy.ofIso i).isRepresentable

Representability Preserved under Natural Isomorphism

Informal description

Let $F, G \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$ be contravariant functors. If $F$ is representable and there exists a natural isomorphism $F \cong G$, then $G$ is also representable.

CategoryTheory.corepresentable_of_natIso theorem

(F : C ⥤ Type v₁) {G} (i : F ≅ G) [F.IsCorepresentable] : G.IsCorepresentable

Full source

theorem corepresentable_of_natIso (F : C ⥤ Type v₁) {G} (i : F ≅ G) [F.IsCorepresentable] :
    G.IsCorepresentable :=
  (F.corepresentableBy.ofIso i).isCorepresentable

Corepresentability is Preserved under Natural Isomorphism

Informal description

Let $F, G \colon C \to \mathrm{Type}_{v_1}$ be functors, and suppose there exists a natural isomorphism $i \colon F \cong G$. If $F$ is corepresentable, then $G$ is also corepresentable.

CategoryTheory.instIsCorepresentableIdType instance

: Functor.IsCorepresentable (𝟭 (Type v₁))

Full source

instance : Functor.IsCorepresentable (𝟭 (Type v₁)) :=
  corepresentable_of_natIso (coyoneda.obj (op PUnit)) Coyoneda.punitIso

Corepresentability of the Identity Functor on Types

Informal description

The identity functor on the category of types $\mathrm{Type}_{v_1}$ is corepresentable.

CategoryTheory.prodCategoryInstance1 instance

: Category ((Cᵒᵖ ⥤ Type v₁) × Cᵒᵖ)

Full source

instance prodCategoryInstance1 : Category ((Cᵒᵖ ⥤ Type v₁) × Cᵒᵖ) :=
  CategoryTheory.prod.{max u₁ v₁, v₁} (CᵒᵖCᵒᵖ ⥤ Type v₁) Cᵒᵖ

Category Structure on Pairs of Functors and Objects in Opposite Categories

Informal description

The product category $(C^{\mathrm{op}} \to \mathrm{Type}_{v_1}) \times C^{\mathrm{op}}$ has a canonical category structure, where objects are pairs $(F, X)$ with $F$ a functor from $C^{\mathrm{op}}$ to $\mathrm{Type}_{v_1}$ and $X$ an object in $C^{\mathrm{op}}$, and morphisms are pairs of morphisms in the respective categories.

CategoryTheory.prodCategoryInstance2 instance

: Category (Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁))

Full source

instance prodCategoryInstance2 : Category (CᵒᵖCᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) :=
  CategoryTheory.prod.{v₁, max u₁ v₁} Cᵒᵖ (CᵒᵖCᵒᵖ ⥤ Type v₁)

The Category Structure on $C^{\mathrm{op}} \times (C^{\mathrm{op}} \to \mathrm{Type}_{v_1})$

Informal description

The product category $C^{\mathrm{op}} \times (C^{\mathrm{op}} \to \mathrm{Type}_{v_1})$ is a category, where $C^{\mathrm{op}}$ is the opposite category of $C$ and $(C^{\mathrm{op}} \to \mathrm{Type}_{v_1})$ is the category of functors from $C^{\mathrm{op}}$ to the category of types in universe $v_1$.

CategoryTheory.yonedaEquiv definition

{X : C} {F : Cᵒᵖ ⥤ Type v₁} : (yoneda.obj X ⟶ F) ≃ F.obj (op X)

Full source

/-- We have a type-level equivalence between natural transformations from the yoneda embedding
and elements of `F.obj X`, without any universe switching.
-/
def yonedaEquiv {X : C} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} : (yoneda.obj X ⟶ F) ≃ F.obj (op X) where
  toFun η := η.app (op X) (𝟙 X)
  invFun ξ := { app := fun _ f ↦ F.map f.op ξ }
  left_inv := by
    intro η
    ext Y f
    dsimp
    rw [← FunctorToTypes.naturality]
    simp
  right_inv := by intro ξ; simp

Yoneda Lemma (Natural Transformation Form)

Informal description

For any object $X$ in a category $C$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, there is a natural equivalence between the set of natural transformations from the Yoneda embedding $\mathrm{Hom}(-, X)$ to $F$ and the set $F(X)$. Explicitly: - The forward map sends a natural transformation $\eta \colon \mathrm{Hom}(-, X) \Rightarrow F$ to $\eta_X(\mathrm{id}_X) \in F(X)$. - The inverse map sends an element $\xi \in F(X)$ to the natural transformation defined by $Y \mapsto (f \mapsto F(f)(\xi))$ for any $Y \in C$ and $f \colon Y \to X$.

CategoryTheory.yonedaEquiv_apply theorem

{X : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) : yonedaEquiv f = f.app (op X) (𝟙 X)

Full source

theorem yonedaEquiv_apply {X : C} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (f : yonedayoneda.obj X ⟶ F) :
    yonedaEquiv f = f.app (op X) (𝟙 X) :=
  rfl

Yoneda Lemma: Evaluation at Identity Morphism

Informal description

For any object $X$ in a category $C$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, the Yoneda equivalence applied to a natural transformation $f \colon \mathrm{Hom}(-, X) \Rightarrow F$ is equal to evaluating $f$ at the object $X^{\mathrm{op}}$ (the opposite of $X$) and the identity morphism $\mathrm{id}_X \in \mathrm{Hom}(X, X)$. In symbols: $$\mathrm{yonedaEquiv}(f) = f_{X^{\mathrm{op}}}(\mathrm{id}_X)$$

CategoryTheory.yonedaEquiv_symm_app_apply theorem

 {X : C} {F : Cᵒᵖ ⥤ Type v₁} (x : F.obj (op X)) (Y : Cᵒᵖ) (f : Y.unop ⟶ X) : (yonedaEquiv.symm x).app Y f = F.map f.op x

Full source

@[simp]
theorem yonedaEquiv_symm_app_apply {X : C} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (x : F.obj (op X)) (Y : Cᵒᵖ)
    (f : Y.unop ⟶ X) : (yonedaEquiv.symm x).app Y f = F.map f.op x :=
  rfl

Yoneda Lemma: Inverse Evaluation Formula

Informal description

For any object $X$ in a category $C$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, given an element $x \in F(X^{\mathrm{op}})$ and an object $Y^{\mathrm{op}}$ in $C^{\mathrm{op}}$ with a morphism $f \colon Y \to X$ in $C$, the application of the natural transformation $\mathrm{yonedaEquiv}^{-1}(x)$ to $Y^{\mathrm{op}}$ and $f$ is equal to $F(f^{\mathrm{op}})(x)$. In symbols: $$(\mathrm{yonedaEquiv}^{-1}(x))_{Y^{\mathrm{op}}}(f) = F(f^{\mathrm{op}})(x)$$

CategoryTheory.yonedaEquiv_naturality theorem

 {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) (g : Y ⟶ X) :
  F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f)

Full source

/-- See also `yonedaEquiv_naturality'` for a more general version. -/
lemma yonedaEquiv_naturality {X Y : C} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (f : yonedayoneda.obj X ⟶ F)
    (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = yonedaEquiv (yonedayoneda.map g ≫ f) := by
  change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙𝟙 Y ≫ g)
  rw [← f.naturality]
  dsimp
  simp

Naturality of the Yoneda Equivalence

Informal description

For any objects $X$ and $Y$ in a category $C$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}$, given a natural transformation $f \colon \mathrm{Hom}(-, X) \Rightarrow F$ and a morphism $g \colon Y \to X$, the following equality holds: $$ F(g^{\mathrm{op}})(\mathrm{yonedaEquiv}(f)) = \mathrm{yonedaEquiv}((\mathrm{y}(g)) \circ f) $$ where: - $\mathrm{y}(g)$ is the image of $g$ under the Yoneda embedding, - $\mathrm{yonedaEquiv}(f) = f_X(\mathrm{id}_X) \in F(X)$ is the evaluation of the natural transformation $f$ at the identity morphism, - $g^{\mathrm{op}}$ is the morphism $g$ viewed in the opposite category $C^{\mathrm{op}}$.

CategoryTheory.yonedaEquiv_naturality' theorem

 {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F) (g : X ⟶ Y) :
  F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f)

Full source

/-- 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. -/
lemma yonedaEquiv_naturality' {X Y : Cᵒᵖ} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (f : yonedayoneda.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.map g (yonedaEquiv f) = yonedaEquiv (yonedayoneda.map g.unop ≫ f) :=
  yonedaEquiv_naturality _ _

Naturality of the Yoneda Equivalence in the Opposite Category

Informal description

For any objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, given a natural transformation $f \colon \mathrm{Hom}(-, \mathrm{unop}(X)) \Rightarrow F$ and a morphism $g \colon X \to Y$ in $C^{\mathrm{op}}$, the following equality holds: $$ F(g)(\mathrm{yonedaEquiv}(f)) = \mathrm{yonedaEquiv}(\mathrm{y}(\mathrm{unop}(g)) \circ f) $$ where: - $\mathrm{y}(\mathrm{unop}(g))$ is the image of $\mathrm{unop}(g)$ under the Yoneda embedding, - $\mathrm{yonedaEquiv}(f) = f_{\mathrm{unop}(X)}(\mathrm{id}_{\mathrm{unop}(X)}) \in F(X)$ is the evaluation of the natural transformation $f$ at the identity morphism.

CategoryTheory.yonedaEquiv_comp theorem

 {X : C} {F G : Cᵒᵖ ⥤ Type v₁} (α : yoneda.obj X ⟶ F) (β : F ⟶ G) : yonedaEquiv (α ≫ β) = β.app _ (yonedaEquiv α)

Full source

lemma yonedaEquiv_comp {X : C} {F G : CᵒᵖCᵒᵖ ⥤ Type v₁} (α : yonedayoneda.obj X ⟶ F) (β : F ⟶ G) :
    yonedaEquiv (α ≫ β) = β.app _ (yonedaEquiv α) :=
  rfl

Composition Property of the Yoneda Equivalence

Informal description

For any object $X$ in a category $C$ and any pair of contravariant functors $F, G \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, given a natural transformation $\alpha \colon \mathrm{Hom}(-, X) \Rightarrow F$ and a natural transformation $\beta \colon F \Rightarrow G$, the following equality holds: $$ \mathrm{yonedaEquiv}(\alpha \circ \beta) = \beta_X(\mathrm{yonedaEquiv}(\alpha)) $$ where: - $\mathrm{yonedaEquiv}(\alpha) = \alpha_X(\mathrm{id}_X) \in F(X)$ is the evaluation of the natural transformation $\alpha$ at the identity morphism, - $\beta_X \colon F(X) \to G(X)$ is the component of $\beta$ at $X$.

CategoryTheory.yonedaEquiv_yoneda_map theorem

{X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f) = f

Full source

lemma yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f) = f := by
  rw [yonedaEquiv_apply]
  simp

Yoneda Lemma: Evaluation of Yoneda Embedding on Morphisms

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, the Yoneda equivalence applied to the image of $f$ under the Yoneda embedding is equal to $f$ itself. In symbols: $$\mathrm{yonedaEquiv}(\mathrm{yoneda.map}(f)) = f$$

CategoryTheory.yonedaEquiv_symm_naturality_left theorem

 {X X' : C} (f : X' ⟶ X) (F : Cᵒᵖ ⥤ Type v₁) (x : F.obj ⟨X⟩) :
  yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f.op) x)

Full source

lemma yonedaEquiv_symm_naturality_left {X X' : C} (f : X' ⟶ X) (F : CᵒᵖCᵒᵖ ⥤ Type v₁)
    (x : F.obj ⟨X⟩) : yonedayoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f.op) x) := by
  apply yonedaEquiv.injective
  simp only [yonedaEquiv_comp, yoneda_obj_obj, yonedaEquiv_symm_app_apply, Equiv.apply_symm_apply]
  erw [yonedaEquiv_yoneda_map]

Naturality of Yoneda Lemma Inverse with Respect to Morphisms

Informal description

For any morphism $f \colon X' \to X$ in a category $C$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, the following diagram commutes: the composition of the Yoneda embedding applied to $f$ with the inverse Yoneda equivalence of an element $x \in F(X)$ equals the inverse Yoneda equivalence of $F(f^{\mathrm{op}})(x) \in F(X')$. In symbols: $$ \mathrm{yoneda}(f) \circ \mathrm{yonedaEquiv}^{-1}(x) = \mathrm{yonedaEquiv}^{-1}(F(f^{\mathrm{op}})(x)) $$ where: - $\mathrm{yoneda}(f) \colon \mathrm{Hom}(-, X') \Rightarrow \mathrm{Hom}(-, X)$ is the natural transformation induced by $f$, - $\mathrm{yonedaEquiv}^{-1}(x) \colon \mathrm{Hom}(-, X) \Rightarrow F$ is the natural transformation corresponding to $x$ under the Yoneda lemma, - $F(f^{\mathrm{op}}) \colon F(X) \to F(X')$ is the map induced by $f^{\mathrm{op}} \colon X' \to X$ in $C^{\mathrm{op}}$.

CategoryTheory.yonedaEquiv_symm_naturality_right theorem

 (X : C) {F F' : Cᵒᵖ ⥤ Type v₁} (f : F ⟶ F') (x : F.obj ⟨X⟩) : yonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app ⟨X⟩ x)

Full source

lemma yonedaEquiv_symm_naturality_right (X : C) {F F' : CᵒᵖCᵒᵖ ⥤ Type v₁} (f : F ⟶ F')
    (x : F.obj ⟨X⟩) : yonedaEquivyonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app ⟨X⟩ x) := by
  apply yonedaEquiv.injective
  simp [yonedaEquiv_comp]

Naturality of Yoneda Lemma Inverse with Respect to Functor Transformations

Informal description

For any object $X$ in a category $C$ and any natural transformation $f \colon F \Rightarrow F'$ between contravariant functors $F, F' \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, the following diagram commutes: the composition of the natural transformation $\mathrm{yonedaEquiv.symm}(x) \colon \mathrm{Hom}(-, X) \Rightarrow F$ (where $x \in F(X)$) with $f$ equals the natural transformation $\mathrm{yonedaEquiv.symm}(f_X(x)) \colon \mathrm{Hom}(-, X) \Rightarrow F'$. In other words, for any $x \in F(X)$, we have: $$ \mathrm{yonedaEquiv.symm}(x) \circ f = \mathrm{yonedaEquiv.symm}(f_X(x)) $$ where $f_X \colon F(X) \to F'(X)$ is the component of $f$ at $X$.

CategoryTheory.map_yonedaEquiv theorem

 {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = f.app (op Y) g

Full source

/-- See also `map_yonedaEquiv'` for a more general version. -/
lemma map_yonedaEquiv {X Y : C} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (f : yonedayoneda.obj X ⟶ F)
    (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = f.app (op Y) g := by
  rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Yoneda Lemma: Naturality of Evaluation

Informal description

For any objects $X$ and $Y$ in a category $C$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}$, given a natural transformation $f \colon \mathrm{Hom}(-, X) \Rightarrow F$ and a morphism $g \colon Y \to X$, the following equality holds: $$ F(g^{\mathrm{op}})(\mathrm{yonedaEquiv}(f)) = f_Y(g) $$ where: - $\mathrm{yonedaEquiv}(f) = f_X(\mathrm{id}_X) \in F(X)$ is the evaluation of the natural transformation $f$ at the identity morphism, - $g^{\mathrm{op}}$ is the morphism $g$ viewed in the opposite category $C^{\mathrm{op}}$, - $f_Y$ is the component of $f$ at $Y$.

CategoryTheory.map_yonedaEquiv' theorem

 {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F) (g : X ⟶ Y) : F.map g (yonedaEquiv f) = f.app Y g.unop

Full source

/-- 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. -/
lemma map_yonedaEquiv' {X Y : Cᵒᵖ} {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (f : yonedayoneda.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.map g (yonedaEquiv f) = f.app Y g.unop := by
  rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Yoneda Lemma: Naturality in the Opposite Category

Informal description

For any objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$ and any contravariant functor $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, given a natural transformation $f \colon \mathrm{Hom}(-, \mathrm{unop}(X)) \Rightarrow F$ and a morphism $g \colon X \to Y$ in $C^{\mathrm{op}}$, the following equality holds: $$ F(g)(\mathrm{yonedaEquiv}(f)) = f_Y(g^{\mathrm{unop}}) $$ where: - $\mathrm{yonedaEquiv}(f) = f_X(\mathrm{id}_{\mathrm{unop}(X)}) \in F(X)$ is the evaluation of $f$ at the identity morphism, - $g^{\mathrm{unop}}$ is the corresponding morphism $\mathrm{unop}(Y) \to \mathrm{unop}(X)$ in $C$, - $f_Y$ is the component of $f$ at $Y$.

CategoryTheory.yonedaEquiv_symm_map theorem

 {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Cᵒᵖ ⥤ Type v₁} (t : F.obj X) :
  yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t

Full source

lemma yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CᵒᵖCᵒᵖ ⥤ Type v₁} (t : F.obj X) :
    yonedaEquiv.symm (F.map f t) = yonedayoneda.map f.unop ≫ yonedaEquiv.symm t := by
  obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
  rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Naturality of the Inverse Yoneda Equivalence with Respect to Functoriality

Informal description

For any objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$, any morphism $f \colon X \to Y$ in $C^{\mathrm{op}}$, and any element $t \in F(X)$, the following equality holds: $$ \mathrm{yonedaEquiv}^{-1}(F(f)(t)) = \mathrm{y}(f^{\mathrm{op}}) \circ \mathrm{yonedaEquiv}^{-1}(t) $$ where: - $\mathrm{y}(f^{\mathrm{op}})$ is the image of the morphism $f^{\mathrm{op}} \colon \mathrm{unop}(Y) \to \mathrm{unop}(X)$ under the Yoneda embedding, - $\mathrm{yonedaEquiv}^{-1}$ is the inverse of the Yoneda equivalence, which maps an element of $F(X)$ to a natural transformation $\mathrm{Hom}(-, \mathrm{unop}(X)) \Rightarrow F$.

CategoryTheory.hom_ext_yoneda theorem

{P Q : Cᵒᵖ ⥤ Type v₁} {f g : P ⟶ Q} (h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g) : f = g

Full source

/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `yoneda.obj X ⟶ P` agree. -/
lemma hom_ext_yoneda {P Q : CᵒᵖCᵒᵖ ⥤ Type v₁} {f g : P ⟶ Q}
    (h : ∀ (X : C) (p : yonedayoneda.obj X ⟶ P), p ≫ f = p ≫ g) :
    f = g := by
  ext X x
  simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
    using congr_arg (yonedaEquiv) (h _ (yonedaEquiv.symm x))

Yoneda Extensionality for Presheaf Morphisms

Informal description

Let $P$ and $Q$ be presheaves of types on a category $C$, and let $f, g \colon P \to Q$ be natural transformations between them. If for every object $X$ in $C$ and every natural transformation $p \colon \mathrm{Hom}(-, X) \to P$, the compositions $p \circ f$ and $p \circ g$ are equal, then $f = g$.

CategoryTheory.yonedaEvaluation definition

: Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type max u₁ v₁

Full source

/-- The "Yoneda evaluation" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
to `F.obj X`, functorially in both `X` and `F`.
-/
def yonedaEvaluation : CᵒᵖCᵒᵖ × (Cᵒᵖ ⥤ Type v₁)Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
  evaluationUncurriedevaluationUncurried Cᵒᵖ (Type v₁) ⋙ uliftFunctor

Yoneda evaluation functor

Informal description

The Yoneda evaluation functor is a functor that takes a pair $(X, F)$ where $X$ is an object in the opposite category $C^{\mathrm{op}}$ and $F$ is a functor from $C^{\mathrm{op}}$ to the category of types, and returns the type $F(X)$. It is constructed by composing the uncurried evaluation functor with the type lifting functor.

CategoryTheory.yonedaEvaluation_map_down theorem

 (P Q : Cᵒᵖ × (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)

Full source

@[simp]
theorem yonedaEvaluation_map_down (P Q : CᵒᵖCᵒᵖ × (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) :=
  rfl

Naturality of Yoneda Evaluation Functor's Action on Morphisms

Informal description

For any objects $P, Q$ in the product category $C^{\mathrm{op}} \times (C^{\mathrm{op}} \to \mathrm{Type}_{v_1})$, any morphism $\alpha : P \to Q$, and any element $x$ in the evaluation of the Yoneda evaluation functor at $P$, the following equality holds: $$((\text{yonedaEvaluation } C).\text{map } \alpha \ x).\text{down} = \alpha_2.\text{app } Q_1 (P_2.\text{map } \alpha_1 \ x.\text{down})$$ Here: - $P_1$ and $Q_1$ are objects in $C^{\mathrm{op}}$, - $P_2$ and $Q_2$ are functors from $C^{\mathrm{op}}$ to $\mathrm{Type}_{v_1}$, - $\alpha_1$ is the component of $\alpha$ in $C^{\mathrm{op}}$, - $\alpha_2$ is the component of $\alpha$ in the functor category, - $\text{app}$ denotes the application of a natural transformation, - $\text{map}$ denotes the action of a functor on morphisms, - $\text{down}$ projects an element from a lifted type to its underlying type.

CategoryTheory.yonedaPairing definition

: Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type max u₁ v₁

Full source

/-- The "Yoneda pairing" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
to `yoneda.op.obj X ⟶ F`, functorially in both `X` and `F`.
-/
def yonedaPairing : CᵒᵖCᵒᵖ × (Cᵒᵖ ⥤ Type v₁)Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
  Functor.prodFunctor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁)) ⋙ Functor.hom (Cᵒᵖ ⥤ Type v₁)

Yoneda Pairing Functor

Informal description

The Yoneda pairing functor is a functor that takes a pair $(X, F)$ where $X$ is an object in the opposite category $C^{\mathrm{op}}$ and $F$ is a functor from $C^{\mathrm{op}}$ to the category of types, and returns the set of natural transformations from the representable functor $\mathrm{Hom}(-, X)$ to $F$. It is constructed by composing the product of the opposite Yoneda embedding and the identity functor with the hom-functor in the presheaf category.

CategoryTheory.yonedaPairingExt theorem

{X : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)} {x y : (yonedaPairing C).obj X} (w : ∀ Y, x.app Y = y.app Y) : x = y

Full source

@[ext]
lemma yonedaPairingExt {X : CᵒᵖCᵒᵖ × (Cᵒᵖ ⥤ Type v₁)} {x y : (yonedaPairing C).obj X}
    (w : ∀ Y, x.app Y = y.app Y) : x = y :=
  NatTrans.ext (funext w)

Extensionality of Natural Transformations in Yoneda Pairing

Informal description

For any object $X$ in the product category $C^{\mathrm{op}} \times (C^{\mathrm{op}} \to \mathrm{Type}_{v_1})$ and any two natural transformations $x, y$ from the Yoneda pairing functor applied to $X$, if $x$ and $y$ agree on all objects $Y$ in $C^{\mathrm{op}}$ (i.e., $x(Y) = y(Y)$ for all $Y$), then $x = y$.

CategoryTheory.yonedaPairing_map theorem

 (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (β : (yonedaPairing C).obj P) :
  (yonedaPairing C).map α β = yoneda.map α.1.unop ≫ β ≫ α.2

Full source

@[simp]
theorem yonedaPairing_map (P Q : CᵒᵖCᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (β : (yonedaPairing C).obj P) :
    (yonedaPairing C).map α β = yonedayoneda.map α.1.unop ≫ β ≫ α.2 :=
  rfl

Functoriality of Yoneda Pairing under Morphisms

Informal description

Let $P = (X, F)$ and $Q = (Y, G)$ be objects in the product category $C^{\mathrm{op}} \times (C^{\mathrm{op}} \to \mathrm{Type}_{v_1})$, and let $\alpha \colon P \to Q$ be a morphism in this category (where $\alpha$ consists of a morphism $f \colon X \to Y$ in $C^{\mathrm{op}}$ and a natural transformation $\eta \colon F \to G$). For any natural transformation $\beta \colon \mathrm{Hom}(-, X) \to F$, the image of $\beta$ under the Yoneda pairing functor applied to $\alpha$ is given by the composition: \[ \mathrm{Hom}(-, Y) \xrightarrow{\mathrm{Hom}(-, f)} \mathrm{Hom}(-, X) \xrightarrow{\beta} F \xrightarrow{\eta} G \] where $\mathrm{Hom}(-, f)$ is the natural transformation induced by postcomposition with $f$.

CategoryTheory.yonedaCompUliftFunctorEquiv definition

(F : Cᵒᵖ ⥤ Type max v₁ w) (X : C) : (yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X)

Full source

/-- A bijection `(yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X)` which is a variant
of `yonedaEquiv` with heterogeneous universes. -/
def yonedaCompUliftFunctorEquiv (F : CᵒᵖCᵒᵖ ⥤ Type max v₁ w) (X : C) :
    (yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X) where
  toFun φ := φ.app (op X) (ULift.up (𝟙 _))
  invFun f :=
    { app := fun _ x => F.map (ULift.down x).op f }
  left_inv φ := by
    ext Y f
    dsimp
    rw [← FunctorToTypes.naturality]
    dsimp
    rw [Category.comp_id]
    rfl
  right_inv f := by simp

Yoneda Lemma with Type Lifting Bijection

Informal description

For any presheaf $ F \colon C^{\mathrm{op}} \to \mathrm{Type}_{\max(v_1, w)} $ and any object $ X $ in $ C $, there is a bijection between the set of natural transformations from the composition of the Yoneda embedding $ \mathrm{y}(X) $ with the type lifting functor $ \mathrm{ULift} $ to $ F $, and the set $ F(\mathrm{op}\, X) $. Explicitly, the bijection maps a natural transformation $ \varphi $ to $ \varphi_{\mathrm{op}\, X}(\mathrm{ULift.up}\, \mathrm{id}_X) $, and conversely, an element $ f \in F(\mathrm{op}\, X) $ is mapped to the natural transformation defined by $ Y \mapsto (x \mapsto F(x^{\mathrm{op}})(f)) $, where $ x $ is a morphism $ Y \to X $.

CategoryTheory.yonedaLemma definition

: yonedaPairing C ≅ yonedaEvaluation C

Full source

/-- 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 001P]
def yonedaLemma : yonedaPairingyonedaPairing C ≅ yonedaEvaluation C :=
  NatIso.ofComponents
    (fun _ ↦ Equiv.toIso (yonedaEquiv.trans Equiv.ulift.symm))
    (by intro (X, F) (Y, G) f
        ext (a : yonedayoneda.obj X.unop ⟶ F)
        apply ULift.ext
        dsimp [yonedaEvaluation, yonedaEquiv]
        simp [← FunctorToTypes.naturality])

Yoneda Lemma (Natural Isomorphism Form)

Informal description

The Yoneda lemma states that the Yoneda pairing functor, which maps a pair $(X, F)$ (where $X$ is an object in $C^{\mathrm{op}}$ and $F$ is a presheaf on $C$) to the set of natural transformations $\mathrm{Hom}(-, X) \Rightarrow F$, is naturally isomorphic to the Yoneda evaluation functor, which maps $(X, F)$ to the set $F(X)$. Explicitly, for any objects $X$ in $C^{\mathrm{op}}$ and $F$ in $C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$, there is a bijection between natural transformations $\eta \colon \mathrm{Hom}(-, X) \Rightarrow F$ and elements of $F(X)$, given by $\eta \mapsto \eta_X(\mathrm{id}_X)$ and $\xi \mapsto (Y \mapsto (f \mapsto F(f)(\xi)))$.

CategoryTheory.curriedYonedaLemma definition

 {C : Type u₁} [SmallCategory C] : (yoneda.op ⋙ coyoneda : Cᵒᵖ ⥤ (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) ≅ evaluation Cᵒᵖ (Type u₁)

Full source

/-- The curried version of yoneda lemma when `C` is small. -/
def curriedYonedaLemma {C : Type u₁} [SmallCategory C] :
    (yoneda.op ⋙ coyoneda : Cᵒᵖ ⥤ (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) ≅ evaluation Cᵒᵖ (Type u₁) :=
  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun _ ↦ Equiv.toIso yonedaEquiv)) (by
    intro X Y f
    ext a b
    dsimp [yonedaEquiv]
    simp [← FunctorToTypes.naturality])

Curried Yoneda Lemma for Small Categories

Informal description

For a small category $C$, there is a natural isomorphism between the composition of the opposite Yoneda embedding functor with the co-Yoneda embedding functor and the evaluation functor on the opposite category $C^{\mathrm{op}}$ with values in the category of types. Explicitly, this isomorphism relates: - The functor $\mathrm{yoneda}^{\mathrm{op}} \circ \mathrm{coyoneda} \colon C^{\mathrm{op}} \to (C^{\mathrm{op}} \to \mathrm{Type}_{u_1}) \to \mathrm{Type}_{u_1}$ - The evaluation functor $\mathrm{eval} \colon C^{\mathrm{op}} \to \mathrm{Type}_{u_1}$ where $\mathrm{yoneda}$ is the Yoneda embedding and $\mathrm{coyoneda}$ is the co-Yoneda embedding.

CategoryTheory.largeCurriedYonedaLemma definition

 {C : Type u₁} [Category.{v₁} C] :
  yoneda.op ⋙ coyoneda ≅ evaluation Cᵒᵖ (Type v₁) ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁}

Full source

/-- The curried version of the Yoneda lemma. -/
def largeCurriedYonedaLemma {C : Type u₁} [Category.{v₁} C] :
    yonedayoneda.op ⋙ coyonedayoneda.op ⋙ coyoneda ≅
      evaluation Cᵒᵖ (Type v₁) ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} :=
  NatIso.ofComponents
    (fun X => NatIso.ofComponents
      (fun _ => Equiv.toIso <| yonedaEquiv.trans Equiv.ulift.symm)
      (by
        intros Y Z f
        ext g
        rw [← ULift.down_inj]
        simpa using yonedaEquiv_comp _ _))
    (by
      intros Y Z f
      ext F g
      rw [← ULift.down_inj]
      simpa using (yonedaEquiv_naturality _ _).symm)

Large Curried Yoneda Lemma

Informal description

For a category $C$, there is a natural isomorphism between the composition of the opposite Yoneda embedding functor with the co-Yoneda embedding functor and the composition of the evaluation functor on the opposite category $C^{\mathrm{op}}$ with values in the category of types, followed by the type lifting functor. Explicitly, this isomorphism relates: - The functor $\mathrm{yoneda}^{\mathrm{op}} \circ \mathrm{coyoneda} \colon C^{\mathrm{op}} \to (C^{\mathrm{op}} \to \mathrm{Type}_{v_1}) \to \mathrm{Type}_{v_1}$ - The functor $\mathrm{eval} \circ \mathrm{uliftFunctor} \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1}$ where $\mathrm{yoneda}$ is the Yoneda embedding, $\mathrm{coyoneda}$ is the co-Yoneda embedding, $\mathrm{eval}$ is the evaluation functor, and $\mathrm{uliftFunctor}$ is the type lifting functor.

CategoryTheory.yonedaOpCompYonedaObj definition

 {C : Type u₁} [Category.{v₁} C] (P : Cᵒᵖ ⥤ Type v₁) : yoneda.op ⋙ yoneda.obj P ≅ P ⋙ uliftFunctor.{u₁}

Full source

/-- Version of the Yoneda lemma where the presheaf is fixed but the argument varies. -/
def yonedaOpCompYonedaObj {C : Type u₁} [Category.{v₁} C] (P : CᵒᵖCᵒᵖ ⥤ Type v₁) :
    yonedayoneda.op ⋙ yoneda.obj Pyoneda.op ⋙ yoneda.obj P ≅ P ⋙ uliftFunctor.{u₁} :=
  isoWhiskerRight largeCurriedYonedaLemma ((evaluation _ _).obj P)

Natural isomorphism between Yoneda composition and presheaf lifting

Informal description

For a category $ C $ and a presheaf $ P \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1} $, there is a natural isomorphism between the composition of the opposite Yoneda embedding functor with the Yoneda embedding applied to $ P $ and the composition of $ P $ with the type lifting functor. Explicitly, this isomorphism relates: - The functor $ \mathrm{yoneda}^{\mathrm{op}} \circ \mathrm{yoneda}(P) \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1} $ - The functor $ P \circ \mathrm{uliftFunctor} \colon C^{\mathrm{op}} \to \mathrm{Type}_{v_1} $ where $ \mathrm{yoneda} $ is the Yoneda embedding and $ \mathrm{uliftFunctor} $ is the type lifting functor.

CategoryTheory.curriedYonedaLemma' definition

 {C : Type u₁} [SmallCategory C] :
  yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁)

Full source

/-- The curried version of yoneda lemma when `C` is small. -/
def curriedYonedaLemma' {C : Type u₁} [SmallCategory C] :
    yonedayoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.opyoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op
      ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁) :=
  NatIso.ofComponents (fun F ↦ NatIso.ofComponents (fun _ ↦ Equiv.toIso yonedaEquiv) (by
    intro X Y f
    ext a
    dsimp [yonedaEquiv]
    simp [← FunctorToTypes.naturality]))

Curried Yoneda Lemma (Functorial Version)

Informal description

For a small category $C$, there is a natural isomorphism between the composition of the Yoneda embedding functor with the left whiskering of the opposite Yoneda embedding functor and the identity functor on the category of presheaves $C^{\mathrm{op}} \to \mathrm{Type}_{u_1}$. Explicitly, this isomorphism states that for any presheaf $F \colon C^{\mathrm{op}} \to \mathrm{Type}_{u_1}$, the functor $\mathrm{Hom}(-, -) \circ F$ is naturally isomorphic to $F$ itself, where the isomorphism is given by the Yoneda equivalence at each component.

CategoryTheory.isIso_of_yoneda_map_bijective theorem

{X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f)) : IsIso f

Full source

lemma isIso_of_yoneda_map_bijective {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f)) :
    IsIso f := by
  obtain ⟨g, hg : g ≫ f = 𝟙 Y⟩ := (hf Y).2 (𝟙 Y)
  exact ⟨g, (hf _).1 (by aesop_cat), hg⟩

Bijectivity of Yoneda Post-Composition Implies Isomorphism

Informal description

Let $C$ be a category, and let $f : X \to Y$ be a morphism in $C$. If for every object $T$ in $C$, the induced map $\Hom(T, X) \to \Hom(T, Y)$ given by post-composition with $f$ is bijective, then $f$ is an isomorphism.

CategoryTheory.isIso_iff_yoneda_map_bijective theorem

{X Y : C} (f : X ⟶ Y) : IsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f))

Full source

lemma isIso_iff_yoneda_map_bijective {X Y : C} (f : X ⟶ Y) :
    IsIsoIsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f)) := by
  refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩
  have : IsIso (yoneda.map f) := inferInstance
  intro T
  rw [← isIso_iff_bijective]
  exact inferInstanceAs (IsIso ((yoneda.map f).app _))

Yoneda Characterization of Isomorphisms: $f$ is iso iff $\Hom(-,f)$ is bijective

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, the following are equivalent: 1. $f$ is an isomorphism. 2. For every object $T$ in $C$, the induced map $\Hom(T, X) \to \Hom(T, Y)$ given by post-composition with $f$ is bijective.

CategoryTheory.isIso_iff_isIso_yoneda_map theorem

{X Y : C} (f : X ⟶ Y) : IsIso f ↔ ∀ c : C, IsIso ((yoneda.map f).app ⟨c⟩)

Full source

lemma isIso_iff_isIso_yoneda_map {X Y : C} (f : X ⟶ Y) :
    IsIsoIsIso f ↔ ∀ c : C, IsIso ((yoneda.map f).app ⟨c⟩) := by
  rw [isIso_iff_yoneda_map_bijective]
  exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm

Yoneda Characterization of Isomorphisms: $f$ is iso iff $\mathrm{Hom}(-,f)$ is pointwise iso

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, the following are equivalent: 1. $f$ is an isomorphism. 2. For every object $c$ in $C$, the induced map $\mathrm{Hom}(c, X) \to \mathrm{Hom}(c, Y)$ given by postcomposition with $f$ is an isomorphism in the category of types.

CategoryTheory.coyonedaEquiv definition

{X : C} {F : C ⥤ Type v₁} : (coyoneda.obj (op X) ⟶ F) ≃ F.obj X

Full source

/-- We have a type-level equivalence between natural transformations from the coyoneda embedding
and elements of `F.obj X.unop`, without any universe switching.
-/
def coyonedaEquiv {X : C} {F : C ⥤ Type v₁} : (coyoneda.obj (op X) ⟶ F) ≃ F.obj X where
  toFun η := η.app X (𝟙 X)
  invFun ξ := { app := fun _ x ↦ F.map x ξ }
  left_inv := fun η ↦ by
    ext Y (x : X ⟶ Y)
    dsimp
    rw [← FunctorToTypes.naturality]
    simp
  right_inv := by intro ξ; simp

Co-Yoneda Lemma

Informal description

For any object $X$ in a category $C$ and any functor $F \colon C \to \mathrm{Type}$, there is a natural equivalence between the set of natural transformations from the co-Yoneda embedding $\mathrm{Hom}(X, -)$ to $F$ and the set $F(X)$. Explicitly, the equivalence maps a natural transformation $\eta \colon \mathrm{Hom}(X, -) \Rightarrow F$ to the element $\eta_X(\mathrm{id}_X) \in F(X)$, and conversely, an element $\xi \in F(X)$ is mapped to the natural transformation that sends a morphism $f \colon X \to Y$ to $F(f)(\xi) \in F(Y)$.

CategoryTheory.coyonedaEquiv_apply theorem

{X : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F) : coyonedaEquiv f = f.app X (𝟙 X)

Full source

theorem coyonedaEquiv_apply {X : C} {F : C ⥤ Type v₁} (f : coyonedacoyoneda.obj (op X) ⟶ F) :
    coyonedaEquiv f = f.app X (𝟙 X) :=
  rfl

Co-Yoneda Evaluation: $f \mapsto f_X(\mathrm{id}_X)$

Informal description

For any object $X$ in a category $C$ and any functor $F \colon C \to \mathrm{Type}$, the co-Yoneda equivalence maps a natural transformation $f \colon \mathrm{Hom}(X, -) \Rightarrow F$ to the element $f_X(\mathrm{id}_X) \in F(X)$.

CategoryTheory.coyonedaEquiv_symm_app_apply theorem

{X : C} {F : C ⥤ Type v₁} (x : F.obj X) (Y : C) (f : X ⟶ Y) : (coyonedaEquiv.symm x).app Y f = F.map f x

Full source

@[simp]
theorem coyonedaEquiv_symm_app_apply {X : C} {F : C ⥤ Type v₁} (x : F.obj X) (Y : C)
    (f : X ⟶ Y) : (coyonedaEquiv.symm x).app Y f = F.map f x :=
  rfl

Inverse Co-Yoneda Evaluation: $\mathrm{coyonedaEquiv}^{-1}(x)_Y(f) = F(f)(x)$

Informal description

For any object $X$ in a category $C$, any functor $F \colon C \to \mathrm{Type}$, any element $x \in F(X)$, and any morphism $f \colon X \to Y$ in $C$, the natural transformation $\mathrm{coyonedaEquiv}^{-1}(x) \colon \mathrm{Hom}(X, -) \Rightarrow F$ satisfies \[ \mathrm{coyonedaEquiv}^{-1}(x)_Y(f) = F(f)(x). \] Here, $\mathrm{coyonedaEquiv}^{-1}(x)$ is the natural transformation corresponding to $x$ under the inverse of the co-Yoneda equivalence, and $F(f) \colon F(X) \to F(Y)$ is the map induced by $f$ via the functor $F$.

CategoryTheory.coyonedaEquiv_naturality theorem

 {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F) (g : X ⟶ Y) :
  F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f)

Full source

lemma coyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type v₁} (f : coyonedacoyoneda.obj (op X) ⟶ F)
    (g : X ⟶ Y) : F.map g (coyonedaEquiv f) = coyonedaEquiv (coyonedacoyoneda.map g.op ≫ f) := by
  change (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)
  rw [← f.naturality]
  dsimp
  simp

Naturality of the Co-Yoneda Lemma with Respect to Morphisms

Informal description

For any objects $X$ and $Y$ in a category $C$, any functor $F \colon C \to \mathrm{Type}$, any natural transformation $f \colon \mathrm{Hom}(X, -) \Rightarrow F$, and any morphism $g \colon X \to Y$ in $C$, the following diagram commutes: \[ F(g)(\mathrm{coyonedaEquiv}(f)) = \mathrm{coyonedaEquiv}(\mathrm{Hom}(g, -) \circ f). \] Here, $\mathrm{coyonedaEquiv}(f) \in F(X)$ is the element corresponding to $f$ under the co-Yoneda lemma, and $\mathrm{Hom}(g, -) \circ f$ denotes the composition of the natural transformation induced by $g$ with $f$.

CategoryTheory.coyonedaEquiv_comp theorem

 {X : C} {F G : C ⥤ Type v₁} (α : coyoneda.obj (op X) ⟶ F) (β : F ⟶ G) :
  coyonedaEquiv (α ≫ β) = β.app _ (coyonedaEquiv α)

Full source

lemma coyonedaEquiv_comp {X : C} {F G : C ⥤ Type v₁} (α : coyonedacoyoneda.obj (op X) ⟶ F) (β : F ⟶ G) :
    coyonedaEquiv (α ≫ β) = β.app _ (coyonedaEquiv α) := by
  rfl

Naturality of Co-Yoneda Lemma with Respect to Composition of Natural Transformations

Informal description

For any object $X$ in a category $C$ and functors $F, G \colon C \to \mathrm{Type}$, given a natural transformation $\alpha \colon \mathrm{Hom}(X, -) \Rightarrow F$ and a natural transformation $\beta \colon F \Rightarrow G$, the equivalence from the co-Yoneda lemma satisfies \[ \mathrm{coyonedaEquiv}(\alpha \circ \beta) = \beta_X(\mathrm{coyonedaEquiv}(\alpha)). \] Here, $\mathrm{coyonedaEquiv}(\alpha) \in F(X)$ is the element corresponding to $\alpha$ under the co-Yoneda lemma, and $\beta_X \colon F(X) \to G(X)$ is the component of $\beta$ at $X$.

CategoryTheory.coyonedaEquiv_coyoneda_map theorem

{X Y : C} (f : X ⟶ Y) : coyonedaEquiv (coyoneda.map f.op) = f

Full source

lemma coyonedaEquiv_coyoneda_map {X Y : C} (f : X ⟶ Y) :
    coyonedaEquiv (coyoneda.map f.op) = f := by
  rw [coyonedaEquiv_apply]
  simp

Co-Yoneda Evaluation of Morphism Yields Original Morphism

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, the co-Yoneda equivalence applied to the image of $f$ under the co-Yoneda embedding yields $f$ itself, i.e., \[ \mathrm{coyonedaEquiv}(\mathrm{coyoneda}(f^{\mathrm{op}})) = f. \]

CategoryTheory.map_coyonedaEquiv theorem

{X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F) (g : X ⟶ Y) : F.map g (coyonedaEquiv f) = f.app Y g

Full source

lemma map_coyonedaEquiv {X Y : C} {F : C ⥤ Type v₁} (f : coyonedacoyoneda.obj (op X) ⟶ F)
    (g : X ⟶ Y) : F.map g (coyonedaEquiv f) = f.app Y g := by
  rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]

Naturality of Co-Yoneda Evaluation with Respect to Morphisms

Informal description

For any objects $X$ and $Y$ in a category $C$, any functor $F \colon C \to \mathrm{Type}$, any natural transformation $f \colon \mathrm{Hom}(X, -) \Rightarrow F$, and any morphism $g \colon X \to Y$ in $C$, the following equality holds: \[ F(g)(\mathrm{coyonedaEquiv}(f)) = f_Y(g). \] Here, $\mathrm{coyonedaEquiv}(f) \in F(X)$ is the element corresponding to $f$ under the co-Yoneda lemma, and $f_Y \colon \mathrm{Hom}(X, Y) \to F(Y)$ is the component of $f$ at $Y$.

CategoryTheory.coyonedaEquiv_symm_map theorem

 {X Y : C} (f : X ⟶ Y) {F : C ⥤ Type v₁} (t : F.obj X) :
  coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t

Full source

lemma coyonedaEquiv_symm_map {X Y : C} (f : X ⟶ Y) {F : C ⥤ Type v₁} (t : F.obj X) :
    coyonedaEquiv.symm (F.map f t) = coyonedacoyoneda.map f.op ≫ coyonedaEquiv.symm t := by
  obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t
  simp [coyonedaEquiv_naturality u f]

Naturality of the Inverse Co-Yoneda Equivalence with Respect to Morphisms

Informal description

For any objects $X$ and $Y$ in a category $C$, any morphism $f \colon X \to Y$ in $C$, and any functor $F \colon C \to \mathrm{Type}_{v₁}$, the following diagram commutes: \[ \mathrm{coyonedaEquiv}^{-1}(F(f)(t)) = \mathrm{Hom}(f, -) \circ \mathrm{coyonedaEquiv}^{-1}(t), \] where $t \in F(X)$ is an element, $\mathrm{coyonedaEquiv}^{-1}$ is the inverse of the co-Yoneda equivalence, and $\mathrm{Hom}(f, -)$ denotes the natural transformation induced by precomposition with $f$.

CategoryTheory.coyonedaEvaluation definition

: C × (C ⥤ Type v₁) ⥤ Type max u₁ v₁

Full source

/-- The "Coyoneda evaluation" functor, which sends `X : C` and `F : C ⥤ Type`
to `F.obj X`, functorially in both `X` and `F`.
-/
def coyonedaEvaluation : C × (C ⥤ Type v₁)C × (C ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
  evaluationUncurriedevaluationUncurried C (Type v₁) ⋙ uliftFunctor

Coyoneda evaluation functor

Informal description

The coyoneda evaluation functor is a functor that takes a pair $(X, F)$ where $X$ is an object in a category $\mathcal{C}$ and $F$ is a functor from $\mathcal{C}$ to the category of types, and returns the type $F(X)$. It is functorial in both $X$ and $F$.

CategoryTheory.coyonedaEvaluation_map_down theorem

 (P Q : C × (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)

Full source

@[simp]
theorem coyonedaEvaluation_map_down (P Q : C × (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) :=
  rfl

Component-wise Action of Coyoneda Evaluation Functor

Informal description

For any objects $P, Q$ in the product category $\mathcal{C} \times (\mathcal{C} \to \mathrm{Type}_{v₁})$, any morphism $\alpha : P \to Q$, and any element $x$ in the evaluation of the coyoneda functor at $P$, the application of the coyoneda evaluation functor's map to $\alpha$ and $x$ satisfies: $$((\text{coyonedaEvaluation } \mathcal{C}).\text{map } \alpha \, x).\text{down} = \alpha_2.\text{app } Q_1 (P_2.\text{map } \alpha_1 \, x.\text{down})$$ where: - $\alpha_1$ is the component of $\alpha$ in $\mathcal{C}$, - $\alpha_2$ is the component of $\alpha$ in the functor category, - $P_2$ and $Q_1$ are the respective components of $P$ and $Q$, - $\text{app}$ denotes the application of a natural transformation, - $\text{map}$ denotes the functorial action on morphisms, - $\text{down}$ projects from the evaluation type.

CategoryTheory.coyonedaPairing definition

: C × (C ⥤ Type v₁) ⥤ Type max u₁ v₁

Full source

/-- The "Coyoneda pairing" functor, which sends `X : C` and `F : C ⥤ Type`
to `coyoneda.rightOp.obj X ⟶ F`, functorially in both `X` and `F`.
-/
def coyonedaPairing : C × (C ⥤ Type v₁)C × (C ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
  Functor.prodFunctor.prod coyoneda.rightOp (𝟭 (C ⥤ Type v₁)) ⋙ Functor.hom (C ⥤ Type v₁)

Coyoneda Pairing Functor

Informal description

The coyoneda pairing functor is a functor that takes a pair $(X, F)$ where $X$ is an object in a category $\mathcal{C}$ and $F$ is a functor from $\mathcal{C}$ to the category of types, and returns the set of natural transformations from the co-Yoneda embedding of $X$ to $F$. It is constructed as the composition of the right opposite of the co-Yoneda embedding functor with the identity functor on the functor category, followed by the hom functor in the functor category.

CategoryTheory.coyonedaPairingExt theorem

{X : C × (C ⥤ Type v₁)} {x y : (coyonedaPairing C).obj X} (w : ∀ Y, x.app Y = y.app Y) : x = y

Full source

@[ext]
lemma coyonedaPairingExt {X : C × (C ⥤ Type v₁)} {x y : (coyonedaPairing C).obj X}
    (w : ∀ Y, x.app Y = y.app Y) : x = y :=
  NatTrans.ext (funext w)

Natural Transformation Extensionality for Coyoneda Pairing

Informal description

For any object $X$ in the product category $\mathcal{C} \times (\mathcal{C} \to \mathrm{Type}_{v₁})$ and any two natural transformations $x, y$ from the co-Yoneda embedding of $X$ to a functor $F$, if $x$ and $y$ agree on all objects $Y$ in $\mathcal{C}$ (i.e., $x_Y = y_Y$ for all $Y$), then $x = y$.

CategoryTheory.coyonedaPairing_map theorem

 (P Q : C × (C ⥤ Type v₁)) (α : P ⟶ Q) (β : (coyonedaPairing C).obj P) :
  (coyonedaPairing C).map α β = coyoneda.map α.1.op ≫ β ≫ α.2

Full source

@[simp]
theorem coyonedaPairing_map (P Q : C × (C ⥤ Type v₁)) (α : P ⟶ Q) (β : (coyonedaPairing C).obj P) :
    (coyonedaPairing C).map α β = coyonedacoyoneda.map α.1.op ≫ β ≫ α.2 :=
  rfl

Functoriality of Coyoneda Pairing: $(F_{\text{coy}} \alpha)(\beta) = F_{\text{coy}}(\alpha_1^{\mathrm{op}}) \circ \beta \circ \alpha_2$

Informal description

For any objects $P$ and $Q$ in the product category $\mathcal{C} \times (\mathcal{C} \to \mathrm{Type}_{v₁})$, any morphism $\alpha \colon P \to Q$, and any natural transformation $\beta$ from the co-Yoneda embedding of $P$ to the second component of $P$, the image of $\beta$ under the coyoneda pairing functor applied to $\alpha$ is equal to the composition of the co-Yoneda embedding of the opposite morphism $\alpha_1^{\mathrm{op}}$, followed by $\beta$, followed by the second component $\alpha_2$ of $\alpha$.

CategoryTheory.coyonedaCompUliftFunctorEquiv definition

(F : C ⥤ Type max v₁ w) (X : Cᵒᵖ) : (coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj X.unop

Full source

/-- A bijection `(coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (unop X)` which is a variant
of `coyonedaEquiv` with heterogeneous universes. -/
def coyonedaCompUliftFunctorEquiv (F : C ⥤ Type max v₁ w) (X : Cᵒᵖ) :
    (coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj X.unop where
  toFun φ := φ.app X.unop (ULift.up (𝟙 _))
  invFun f :=
    { app := fun _ x => F.map (ULift.down x) f }
  left_inv φ := by
    ext Y f
    dsimp
    rw [← FunctorToTypes.naturality]
    dsimp
    rw [Category.id_comp]
    rfl
  right_inv f := by simp

Bijection between natural transformations and evaluations for co-Yoneda embedding with type lifting

Informal description

Given a functor $ F \colon C \to \mathrm{Type}_{\max(v_1, w)} $ and an object $ X $ in the opposite category $ C^{\mathrm{op}} $, there is a bijection between the set of natural transformations from the composition of the co-Yoneda embedding functor applied to $ X $ followed by the type lifting functor to $ F $, and the set $ F(X^{\mathrm{unop}}) $. More explicitly, the bijection maps a natural transformation $ \varphi $ to $ \varphi_{X^{\mathrm{unop}}}(\mathrm{ULift.up}(1_{X^{\mathrm{unop}}})) $, and its inverse maps an element $ f \in F(X^{\mathrm{unop}}) $ to the natural transformation defined by $ Y \mapsto (x \mapsto F(\mathrm{ULift.down}(x))(f)) $.

CategoryTheory.coyonedaLemma definition

: coyonedaPairing C ≅ coyonedaEvaluation C

Full source

/-- 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 001P]
def coyonedaLemma : coyonedaPairingcoyonedaPairing C ≅ coyonedaEvaluation C :=
  NatIso.ofComponents
    (fun _ ↦ Equiv.toIso (coyonedaEquiv.trans Equiv.ulift.symm))
    (by intro (X, F) (Y, G) f
        ext (a : coyonedacoyoneda.obj (op X) ⟶ F)
        apply ULift.ext
        dsimp [coyonedaEquiv, coyonedaEvaluation]
        simp [← FunctorToTypes.naturality])

Co-Yoneda Lemma

Informal description

The co-Yoneda lemma states that the co-Yoneda pairing functor, which maps a pair $(X, F)$ (where $X$ is an object in category $C$ and $F \colon C \to \mathrm{Type}$ is a functor) to the set of natural transformations $\mathrm{Hom}(X, -) \Rightarrow F$, is naturally isomorphic to the co-Yoneda evaluation functor that maps $(X, F)$ to $F(X)$. Explicitly, the isomorphism is given by the equivalence that sends a natural transformation $\eta \colon \mathrm{Hom}(X, -) \Rightarrow F$ to $\eta_X(\mathrm{id}_X) \in F(X)$, and conversely, an element $\xi \in F(X)$ is mapped to the natural transformation defined by $f \mapsto F(f)(\xi)$ for any morphism $f \colon X \to Y$.

CategoryTheory.curriedCoyonedaLemma definition

{C : Type u₁} [SmallCategory C] : coyoneda.rightOp ⋙ coyoneda ≅ evaluation C (Type u₁)

Full source

/-- The curried version of coyoneda lemma when `C` is small. -/
def curriedCoyonedaLemma {C : Type u₁} [SmallCategory C] :
    coyonedacoyoneda.rightOp ⋙ coyonedacoyoneda.rightOp ⋙ coyoneda ≅ evaluation C (Type u₁) :=
  NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun _ ↦ Equiv.toIso coyonedaEquiv)) (by
    intro X Y f
    ext a b
    simp [coyonedaEquiv, ← FunctorToTypes.naturality])

Curried Co-Yoneda Lemma for Small Categories

Informal description

For a small category $C$, there is a natural isomorphism between the composition of the right opposite of the co-Yoneda embedding functor followed by the co-Yoneda embedding functor, and the evaluation functor from $C$ to the category of types in universe $u_1$. Explicitly, this isomorphism states that the functor obtained by first applying the co-Yoneda embedding to the opposite category $C^{\mathrm{op}}$ and then applying the co-Yoneda embedding to $C$ is naturally isomorphic to the functor that evaluates objects of $C$ in the category of types.

CategoryTheory.largeCurriedCoyonedaLemma definition

 {C : Type u₁} [Category.{v₁} C] :
  (coyoneda.rightOp ⋙ coyoneda) ≅ evaluation C (Type v₁) ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁}

Full source

/-- The curried version of the Coyoneda lemma. -/
def largeCurriedCoyonedaLemma {C : Type u₁} [Category.{v₁} C] :
    (coyoneda.rightOp ⋙ coyoneda) ≅
      evaluation C (Type v₁) ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} :=
  NatIso.ofComponents
    (fun X => NatIso.ofComponents
      (fun _ => Equiv.toIso <| coyonedaEquiv.trans Equiv.ulift.symm)
      (by
        intros Y Z f
        ext g
        rw [← ULift.down_inj]
        simpa using coyonedaEquiv_comp _ _))
    (by
      intro Y Z f
      ext F g
      rw [← ULift.down_inj]
      simpa using (coyonedaEquiv_naturality _ _).symm)

Large Curried Co-Yoneda Lemma

Informal description

For a category $C$, there is a natural isomorphism between the composition of the right opposite of the co-Yoneda embedding functor followed by the co-Yoneda embedding functor, and the composition of the evaluation functor from $C$ to the category of types in universe $v_1$ with the type lifting functor to universe $\max(u_1, v_1)$. Explicitly, this isomorphism states that the functor obtained by first applying the co-Yoneda embedding to the opposite category $C^{\mathrm{op}}$ and then applying the co-Yoneda embedding to $C$ is naturally isomorphic to the functor that evaluates objects of $C$ in the category of types and then lifts the resulting types to a higher universe.

CategoryTheory.coyonedaCompYonedaObj definition

 {C : Type u₁} [Category.{v₁} C] (P : C ⥤ Type v₁) : coyoneda.rightOp ⋙ yoneda.obj P ≅ P ⋙ uliftFunctor.{u₁}

Full source

/-- Version of the Coyoneda lemma where the presheaf is fixed but the argument varies. -/
def coyonedaCompYonedaObj {C : Type u₁} [Category.{v₁} C] (P : C ⥤ Type v₁) :
    coyonedacoyoneda.rightOp ⋙ yoneda.obj Pcoyoneda.rightOp ⋙ yoneda.obj P ≅ P ⋙ uliftFunctor.{u₁} :=
  isoWhiskerRight largeCurriedCoyonedaLemma ((evaluation _ _).obj P)

Natural isomorphism between co-Yoneda composition and type lifting

Informal description

For a category $C$ and a functor $P \colon C \to \mathrm{Type}\, v_1$, there is a natural isomorphism between the composition of the right opposite of the co-Yoneda embedding functor followed by the Yoneda embedding applied to $P$, and the composition of $P$ with the type lifting functor to universe $\max(u_1, v_1)$. Explicitly, this isomorphism states that the functor obtained by first applying the co-Yoneda embedding to the opposite category $C^{\mathrm{op}}$ and then applying the Yoneda embedding to $P$ is naturally isomorphic to the functor obtained by applying $P$ and then lifting the resulting types to a higher universe.

CategoryTheory.curriedCoyonedaLemma' definition

 {C : Type u₁} [SmallCategory C] :
  yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp ≅ 𝟭 (C ⥤ Type u₁)

Full source

/-- The curried version of coyoneda lemma when `C` is small. -/
def curriedCoyonedaLemma' {C : Type u₁} [SmallCategory C] :
    yonedayoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOpyoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp
      ≅ 𝟭 (C ⥤ Type u₁) :=
  NatIso.ofComponents (fun F ↦ NatIso.ofComponents (fun _ ↦ Equiv.toIso coyonedaEquiv) (by
    intro X Y f
    ext a
    simp [coyonedaEquiv, ← FunctorToTypes.naturality]))

Curried Co-Yoneda Lemma for Small Categories

Informal description

For a small category $C$, there is a natural isomorphism between the composition of the Yoneda embedding functor followed by the left whiskering of the right opposite of the co-Yoneda embedding functor, and the identity functor on the category of functors from $C$ to $\mathrm{Type}\, u_1$. Explicitly, this isomorphism states that for any functor $F \colon C \to \mathrm{Type}\, u_1$, the functor obtained by first applying the Yoneda embedding to $F$ and then applying the left whiskering of the right opposite of the co-Yoneda embedding is naturally isomorphic to $F$ itself. The components of this isomorphism are given by the equivalence provided by the co-Yoneda lemma, which relates natural transformations from the co-Yoneda embedding to evaluations of $F$.

CategoryTheory.isIso_of_coyoneda_map_bijective theorem

{X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x)) : IsIso f

Full source

lemma isIso_of_coyoneda_map_bijective {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x)) :
    IsIso f := by
  obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)
  refine ⟨g, hg, (hf _).1 ?_⟩
  simp only [Category.comp_id, ← Category.assoc, hg, Category.id_comp]

Bijectivity of Post-Composition Implies Isomorphism

Informal description

Let $C$ be a category, and let $f : X \to Y$ be a morphism in $C$. If for every object $T$ in $C$, the function $(f \circ -) : \text{Hom}(Y, T) \to \text{Hom}(X, T)$ is bijective, then $f$ is an isomorphism.

CategoryTheory.isIso_iff_coyoneda_map_bijective theorem

{X Y : C} (f : X ⟶ Y) : IsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x))

Full source

lemma isIso_iff_coyoneda_map_bijective {X Y : C} (f : X ⟶ Y) :
    IsIsoIsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x)) := by
  refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩
  have : IsIso (coyoneda.map f.op) := inferInstance
  intro T
  rw [← isIso_iff_bijective]
  exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))

Characterization of Isomorphisms via Bijective Post-Composition

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, $f$ is an isomorphism if and only if for every object $T$ in $C$, the post-composition map $(f \circ -) \colon \text{Hom}(Y, T) \to \text{Hom}(X, T)$ is bijective.

CategoryTheory.isIso_iff_isIso_coyoneda_map theorem

{X Y : C} (f : X ⟶ Y) : IsIso f ↔ ∀ c : C, IsIso ((coyoneda.map f.op).app c)

Full source

lemma isIso_iff_isIso_coyoneda_map {X Y : C} (f : X ⟶ Y) :
    IsIsoIsIso f ↔ ∀ c : C, IsIso ((coyoneda.map f.op).app c) := by
  rw [isIso_iff_coyoneda_map_bijective]
  exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm

Characterization of Isomorphisms via Isomorphism of Co-Yoneda Components

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, $f$ is an isomorphism if and only if for every object $c$ in $C$, the component of the co-Yoneda embedding applied to $f^{\mathrm{op}}$ at $c$ is an isomorphism. More precisely, this means that $f$ is an isomorphism if and only if for every $c \in C$, the natural transformation $(f^{\mathrm{op}} \circ -) \colon \mathrm{Hom}(Y, c) \to \mathrm{Hom}(X, c)$ is an isomorphism in the category of types.

CategoryTheory.yonedaMap definition

(X : C) : yoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X)

Full source

/-- The natural transformation `yoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X)`
when `F : C ⥤ D` and `X : C`. -/
def yonedaMap (X : C) : yonedayoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X) where
  app _ f := F.map f

Yoneda natural transformation induced by a functor

Informal description

Given a functor $ F \colon C \to D $ and an object $ X $ in $ C $, the natural transformation $ \mathrm{y}(X) \Rightarrow F^{\mathrm{op}} \circ \mathrm{y}(F(X)) $ is defined as follows: for any object $ Y $ in $ C^{\mathrm{op}} $, the component at $ Y $ maps a morphism $ f \colon Y \to X $ in $ C $ to the morphism $ F(f) $ in $ D $. Here, $ \mathrm{y} $ denotes the Yoneda embedding functor.

CategoryTheory.yonedaMap_app_apply theorem

{Y : C} {X : Cᵒᵖ} (f : X.unop ⟶ Y) : (yonedaMap F Y).app X f = F.map f

Full source

@[simp]
lemma yonedaMap_app_apply {Y : C} {X : Cᵒᵖ} (f : X.unop ⟶ Y) :
    (yonedaMap F Y).app X f = F.map f := rfl

Yoneda Natural Transformation Component Formula

Informal description

For any objects $X$ and $Y$ in a category $C$, and any morphism $f \colon X \to Y$ in $C$, the component of the Yoneda natural transformation at $X^{\mathrm{op}}$ applied to $f$ is equal to the image of $f$ under the functor $F \colon C \to D$. More precisely, if we consider the Yoneda embedding $\mathrm{y} \colon C \to C^{\mathrm{op}} \to \mathrm{Type}$ and a functor $F \colon C \to D$, then for any $X \in C^{\mathrm{op}}$ and $f \colon X \to Y$ in $C$, we have: $$(\mathrm{y}(Y))(X)(f) = F(f)$$

CategoryTheory.Functor.sectionsEquivHom definition

(F : C ⥤ Type u₂) (X : Type u₂) [Unique X] : F.sections ≃ ((const _).obj X ⟶ F)

Full source

/-- 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. -/
@[simps apply_app]
def Functor.sectionsEquivHom (F : C ⥤ Type u₂) (X : Type u₂) [Unique X] :
    F.sections ≃ ((const _).obj X ⟶ F) where
  toFun s :=
    { app j x := s.1 j
      naturality _ _ _ := by ext x; simp }
  invFun τ := ⟨fun j ↦ τ.app _ (default : X), fun φ ↦ (congr_fun (τ.naturality φ) _).symm⟩
  left_inv s := rfl
  right_inv τ := by
    ext _ (x : X)
    rw [Unique.eq_default x]

Equivalence between sections and natural transformations from a constant functor

Informal description

Given a functor $ F : C \to \mathrm{Type}_{u_2} $ and a type $ X $ with a unique element, there is a natural equivalence between the sections of $ F $ and the natural transformations from the constant functor on $ X $ to $ F $. Explicitly: - The forward map takes a section $ s $ of $ F $ to the natural transformation defined by $ \tau_j(x) = s(j) $ for all $ j \in C $ and $ x \in X $. - The inverse map takes a natural transformation $ \tau $ to the section $ j \mapsto \tau_j(\text{default}) $, where $\text{default}$ is the unique element of $ X $. This equivalence is natural in $ F $.

CategoryTheory.Functor.sectionsEquivHom_naturality theorem

 {F G : C ⥤ Type u₂} (f : F ⟶ G) (X : Type u₂) [Unique X] (x : F.sections) :
  (G.sectionsEquivHom X) ((sectionsFunctor C).map f x) = (F.sectionsEquivHom X) x ≫ f

Full source

lemma Functor.sectionsEquivHom_naturality {F G : C ⥤ Type u₂} (f : F ⟶ G) (X : Type u₂) [Unique X]
    (x : F.sections) :
    (G.sectionsEquivHom X) ((sectionsFunctor C).map f x) = (F.sectionsEquivHom X) x ≫ f := by
  rfl

Naturality of the sections-hom equivalence for type-valued functors

Informal description

Given two functors $F, G : C \to \mathrm{Type}_{u_2}$ and a natural transformation $f : F \to G$ between them, for any type $X$ with a unique element and any section $x$ of $F$, the following diagram commutes: The image of $x$ under the sections functor composed with $f$ (i.e., $(sectionsFunctor C).map f x$) corresponds via the equivalence $(G.sectionsEquivHom X)$ to the composition of the natural transformation corresponding to $x$ (via $(F.sectionsEquivHom X)$) with $f$. In symbols: $$(G.sectionsEquivHom X)((sectionsFunctor C).map f x) = (F.sectionsEquivHom X)(x) \circ f$$

CategoryTheory.Functor.sectionsEquivHom_naturality_symm theorem

 {F G : C ⥤ Type u₂} (f : F ⟶ G) (X : Type u₂) [Unique X] (τ : (const C).obj X ⟶ F) :
  (G.sectionsEquivHom X).symm (τ ≫ f) = (sectionsFunctor C).map f ((F.sectionsEquivHom X).symm τ)

Full source

lemma Functor.sectionsEquivHom_naturality_symm {F G : C ⥤ Type u₂} (f : F ⟶ G) (X : Type u₂)
    [Unique X] (τ : (const C).obj X ⟶ F) :
    (G.sectionsEquivHom X).symm (τ ≫ f) =
      (sectionsFunctor C).map f ((F.sectionsEquivHom X).symm τ) := by
  rfl

Naturality of the Inverse Sections-Hom Equivalence for Type-Valued Functors

Informal description

Given two functors $F, G \colon C \to \mathrm{Type}_{u_2}$ and a natural transformation $f \colon F \to G$, for any type $X$ with a unique element and any natural transformation $\tau \colon (\mathrm{const}_C).obj X \to F$, the following holds: $$(G.\mathrm{sectionsEquivHom}\, X)^{-1}(\tau \circ f) = (\mathrm{sectionsFunctor}\, C).map\, f \left((F.\mathrm{sectionsEquivHom}\, X)^{-1} \tau\right).$$ Here, $\mathrm{sectionsEquivHom}$ is the equivalence between sections of a functor and natural transformations from a constant functor, and $\mathrm{sectionsFunctor}$ is the functor that maps a type-valued functor to its sections.

CategoryTheory.sectionsFunctorNatIsoCoyoneda definition

 (X : Type max u₁ u₂) [Unique X] :
  Functor.sectionsFunctor.{v₁, max u₁ u₂} C ≅ coyoneda.obj (op ((Functor.const C).obj X))

Full source

/-- 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`. -/
@[simps!]
noncomputable def sectionsFunctorNatIsoCoyoneda (X : Type max u₁ u₂) [Unique X] :
    Functor.sectionsFunctorFunctor.sectionsFunctor.{v₁, max u₁ u₂} C ≅ coyoneda.obj (op ((Functor.const C).obj X)) :=
  NatIso.ofComponents fun F ↦ (F.sectionsEquivHom X).toIso

Natural isomorphism between sections functor and co-Yoneda embedding of constant functor

Informal description

Given a type $X$ with a unique element, there is a natural isomorphism between the sections functor (which sends a type-valued functor $F \colon C \to \mathrm{Type}$ to the type of its sections) and the co-Yoneda embedding of the constant functor on $X$. Explicitly, for any functor $F \colon C \to \mathrm{Type}$, the isomorphism identifies: - The sections of $F$ (families $(u_j \in F(j))_{j \in C}$ compatible with morphisms in $C$) - The natural transformations from the constant functor on $X$ to $F$ This isomorphism is natural in $F$.

CategoryTheory.Functor.FullyFaithful.homNatIso definition

 {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) :
  F.op ⋙ yoneda.obj (F.obj X) ⋙ uliftFunctor.{v₁} ≅ yoneda.obj X ⋙ uliftFunctor.{v₂}

Full source

/-- `FullyFaithful.homEquiv` as a natural isomorphism. -/
@[simps!]
def homNatIso {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) :
    F.op ⋙ yoneda.obj (F.obj X) ⋙ uliftFunctor.{v₁}F.op ⋙ yoneda.obj (F.obj X) ⋙ uliftFunctor.{v₁} ≅ yoneda.obj X ⋙ uliftFunctor.{v₂} :=
  NatIso.ofComponents
    (fun Y => Equiv.toIso (Equiv.ulift.trans <| hF.homEquiv.symm.trans Equiv.ulift.symm))
    (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp)))

Natural isomorphism induced by a fully faithful functor on Yoneda embeddings

Informal description

Given a fully faithful functor $F \colon C \to D$ between categories $C$ and $D$, and an object $X$ in $C$, there is a natural isomorphism between the functors: 1. $F^{\mathrm{op}} \circ \mathrm{y}(F(X)) \circ \mathrm{ULift}$, where $\mathrm{y}$ is the Yoneda embedding and $\mathrm{ULift}$ is the type lifting functor. 2. $\mathrm{y}(X) \circ \mathrm{ULift}$, where $\mathrm{y}$ is the Yoneda embedding and $\mathrm{ULift}$ is the type lifting functor. This isomorphism is constructed via the equivalence of hom-sets induced by the fully faithful property of $F$, composed with the lifting and unlifting of universes.

CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight definition

 {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) :
  F.op ⋙ yoneda.obj (F.obj X) ≅ yoneda.obj X ⋙ uliftFunctor.{v₂}

Full source

/-- `FullyFaithful.homEquiv` as a natural isomorphism. -/
@[simps!]
def homNatIsoMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful)
    (X : C) : F.op ⋙ yoneda.obj (F.obj X)F.op ⋙ yoneda.obj (F.obj X) ≅ yoneda.obj X ⋙ uliftFunctor.{v₂} :=
  NatIso.ofComponents
    (fun Y => Equiv.toIso (hF.homEquiv.symm.trans Equiv.ulift.symm))
    (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp)))

Natural isomorphism between Yoneda embeddings via fully faithful functor (max universe case)

Informal description

Given a fully faithful functor $F \colon C \to D$ between categories $C$ and $D$ (where $D$ is a category in universe $\max(v₁, v₂)$), and an object $X$ in $C$, there is a natural isomorphism between the functors: 1. The composition of the opposite functor $F^{\mathrm{op}}$ with the Yoneda embedding applied to $F(X)$ 2. The composition of the Yoneda embedding applied to $X$ with the type lifting functor to universe $v₂$ This isomorphism is constructed componentwise using the equivalence of hom-sets induced by the fully faithful property of $F$, composed with universe lifting.

CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft definition

 {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) :
  F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ⋙ (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₁} ≅
    yoneda ⋙ (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₂}

Full source

/-- `FullyFaithful.homEquiv` as a natural isomorphism. -/
@[simps!]
def compYonedaCompWhiskeringLeft {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D}
    (hF : F.FullyFaithful) : F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ⋙
      (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₁}F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ⋙
      (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₁} ≅
      yoneda ⋙ (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₂} :=
  NatIso.ofComponents (fun X => hF.homNatIso _)
    (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp)))

Natural isomorphism between Yoneda compositions via fully faithful functor

Informal description

Given a fully faithful functor $ F \colon C \to D $ between categories $ C $ and $ D $, there is a natural isomorphism between the following functor compositions: 1. The composition of $ F $ with the Yoneda embedding, followed by left whiskering with the opposite functor $ F^{\mathrm{op}} $, and then right whiskering with the type lifting functor to universe $ v_1 $. 2. The Yoneda embedding followed by right whiskering with the type lifting functor to universe $ v_2 $. This isomorphism is constructed componentwise using the equivalence of hom-sets induced by the fully faithful property of $ F $.

CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight definition

 {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) :
  F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ≅ yoneda ⋙ (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₂}

Full source

/-- `FullyFaithful.homEquiv` as a natural isomorphism. -/
@[simps!]
def compYonedaCompWhiskeringLeftMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D}
    (hF : F.FullyFaithful) : F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.opF ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ≅
      yoneda ⋙ (CategoryTheory.whiskeringRight _ _ _).obj uliftFunctor.{v₂} :=
  NatIso.ofComponents (fun X => hF.homNatIsoMaxRight _)
    (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp)))

Natural isomorphism between Yoneda compositions via fully faithful functor (max universe case)

Informal description

Given a fully faithful functor $F \colon C \to D$ between categories $C$ and $D$ (where $D$ is a category in universe $\max(v₁, v₂)$), there is a natural isomorphism between the following functor compositions: 1. The composition of $F$ with the Yoneda embedding, followed by left whiskering with $F^{\mathrm{op}}$ 2. The Yoneda embedding followed by right whiskering with the type lifting functor to universe $v₂$ This isomorphism is constructed componentwise using the equivalence of hom-sets induced by the fully faithful property of $F$.

References