# The Yoneda embedding #

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

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

## References #

- Stacks: Opposite Categories and the Yoneda Lemma

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

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.yoneda_map_app {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : C ᵒᵖ) (g : { obj := fun (Y : C ᵒᵖ) => Opposite.unop Y ⟶ X✝, map := fun {X Y : C ᵒᵖ} (f : X ⟶ Y) (g : Opposite.unop X ⟶ X✝) => CategoryStruct.comp f.unop g, map_id := ⋯, map_comp := ⋯ }.obj x✝) :
(yoneda.map f).app x✝ g = CategoryStruct.comp g f
source
@[simp]
theorem CategoryTheory.yoneda_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (Y : C ᵒᵖ) :
(yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)
source
@[simp]
theorem CategoryTheory.yoneda_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : C ᵒᵖ} (f : X✝ ⟶ Y✝) (g : Opposite.unop X✝ ⟶ X) :
(yoneda.obj X).map f g = CategoryStruct.comp f.unop g
source
def CategoryTheory.uliftYoneda {C : Type u₁} [Category.{v₁, u₁} C] :
Functor C (Functor C ᵒᵖ (Type (max w v₁)))

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.uliftYoneda_map_app_down {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : C ᵒᵖ) (a✝ : uliftFunctor.{w, v₁}.obj ((yoneda.obj X✝).obj X)) :
((uliftYoneda.{w, v₁, u₁}.map f).app X a✝).down = CategoryStruct.comp a✝.down f
source
@[simp]
theorem CategoryTheory.uliftYoneda_obj_map_down {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : C ᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : uliftFunctor.{w, v₁}.obj ((yoneda.obj X).obj X✝)) :
((uliftYoneda.{w, v₁, u₁}.obj X).map f a✝).down = CategoryStruct.comp f.unop a✝.down
source
@[simp]
theorem CategoryTheory.uliftYoneda_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X✝ : C ᵒᵖ) :
(uliftYoneda.{w, v₁, u₁}.obj X).obj X✝ = ULift.{w, v₁} (Opposite.unop X✝ ⟶ X)
source
def CategoryTheory.uliftYonedaIsoYoneda {C : Type u₁} [Category.{max w v₁, u₁} C] :
uliftYoneda.{w, max v₁ w, u₁} ≅ yoneda

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.uliftYonedaIsoYoneda_hom_app_app {C : Type u₁} [Category.{max w v₁, u₁} C] (X : C) (X✝ : C ᵒᵖ) (a✝ : (uliftYoneda.{w, max v₁ w, u₁}.obj X).obj X✝) :
(uliftYonedaIsoYoneda.hom.app X).app X✝ a✝ = a✝.down
source
@[simp]
theorem CategoryTheory.uliftYonedaIsoYoneda_inv_app_app_down {C : Type u₁} [Category.{max w v₁, u₁} C] (X : C) (X✝ : C ᵒᵖ) (a✝ : (yoneda.obj X).obj X✝) :
((uliftYonedaIsoYoneda.inv.app X).app X✝ a✝).down = a✝
source
@[reducible, inline]
abbrev CategoryTheory.coyoneda {C : Type u₁} [Category.{v₁, u₁} C] :
Functor C ᵒᵖ (Functor C (Type v₁))

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

Equations

- CategoryTheory.coyoneda = CategoryTheory.yoneda.flip

Instances For

source
@[reducible, inline]
abbrev CategoryTheory.uliftCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] :
Functor C ᵒᵖ (Functor C (Type (max w v₁)))

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

Equations

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

Instances For

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

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.uliftCoyonedaIsoCoyoneda_inv_app_app_down {C : Type u₁} [Category.{max w v₁, u₁} C] (X : C ᵒᵖ) (X✝ : C) (a✝ : (coyoneda.obj X).obj X✝) :
((uliftCoyonedaIsoCoyoneda.inv.app X).app X✝ a✝).down = a✝
source
@[simp]
theorem CategoryTheory.uliftCoyonedaIsoCoyoneda_hom_app_app {C : Type u₁} [Category.{max w v₁, u₁} C] (X : C ᵒᵖ) (X✝ : C) (a✝ : (uliftCoyoneda.{w, max v₁ w, u₁}.obj X).obj X✝) :
(uliftCoyonedaIsoCoyoneda.hom.app X).app X✝ a✝ = a✝.down
source
theorem CategoryTheory.Yoneda.obj_map_id {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Opposite.op X ⟶ Opposite.op Y) :
(yoneda.obj X).map f (CategoryStruct.id X) = (yoneda.map f.unop).app (Opposite.op Y) (CategoryStruct.id Y)
source
@[simp]
theorem CategoryTheory.Yoneda.naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : yoneda.obj X ⟶ yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) :
CategoryStruct.comp f (α.app (Opposite.op Z') h) = α.app (Opposite.op Z) (CategoryStruct.comp f h)
source
def CategoryTheory.Yoneda.fullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] :
yoneda.FullyFaithful

The Yoneda embedding is fully faithful.

Equations

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

Instances For

source
theorem CategoryTheory.Yoneda.fullyFaithful_preimage {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : yoneda.obj X ⟶ yoneda.obj Y) :
fullyFaithful.preimage f = f.app (Opposite.op X) (CategoryStruct.id X)
source
instance CategoryTheory.Yoneda.yoneda_full {C : Type u₁} [Category.{v₁, u₁} C] :
yoneda.Full

The Yoneda embedding is full.

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

The Yoneda embedding is faithful.

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

Extensionality via Yoneda. The typical usage would be

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

Equations

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

Instances For

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

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

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

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

Equations

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

Instances For

source
instance CategoryTheory.ULiftYoneda.instFullFunctorOppositeTypeUliftYoneda (C : Type u₁) [Category.{v₁, u₁} C] :
uliftYoneda.{w, v₁, u₁}.Full
source
instance CategoryTheory.ULiftYoneda.instFaithfulFunctorOppositeTypeUliftYoneda (C : Type u₁) [Category.{v₁, u₁} C] :
uliftYoneda.{w, v₁, u₁}.Faithful
source
@[simp]
theorem CategoryTheory.Coyoneda.naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (α : coyoneda.obj X ⟶ coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z) (h : Opposite.unop X ⟶ Z') :
CategoryStruct.comp (α.app Z' h) f = α.app Z (CategoryStruct.comp h f)
source
def CategoryTheory.Coyoneda.fullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] :
coyoneda.FullyFaithful

The co-Yoneda embedding is fully faithful.

Equations

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

Instances For

source
theorem CategoryTheory.Coyoneda.fullyFaithful_preimage {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (f : coyoneda.obj X ⟶ coyoneda.obj Y) :
fullyFaithful.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryStruct.id (Opposite.unop X)))
source
def CategoryTheory.Coyoneda.preimage {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (f : coyoneda.obj X ⟶ coyoneda.obj Y) :
X ⟶ Y

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

Equations

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

Instances For

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

Extensionality via Coyoneda. The typical usage would be

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

Equations

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

Instances For

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

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

source
def CategoryTheory.Coyoneda.punitIso :
coyoneda.obj (Opposite.op PUnit.{v₁ + 1}) ≅ Functor.id (Type v₁)

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

Equations

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

Instances For

source
def CategoryTheory.Coyoneda.objOpOp {C : Type u₁} [Category.{v₁, u₁} C] (X : C) :
coyoneda.obj (Opposite.op (Opposite.op X)) ≅ yoneda.obj X

Taking the `unop` of morphisms is a natural isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Coyoneda.objOpOp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X✝ : C ᵒᵖ) (a✝ : (yoneda.obj X).obj X✝) :
(objOpOp X).inv.app X✝ a✝ = (opEquiv (Opposite.op X) X✝).symm a✝
source
@[simp]
theorem CategoryTheory.Coyoneda.objOpOp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X✝ : C ᵒᵖ) (a✝ : (coyoneda.obj (Opposite.op (Opposite.op X))).obj X✝) :
(objOpOp X).hom.app X✝ a✝ = (opEquiv (Opposite.op X) X✝) a✝
source
def CategoryTheory.Coyoneda.opIso {C : Type u₁} [Category.{v₁, u₁} C] :
yoneda.comp ((Functor.whiskeringLeft C C ᵒᵖ ᵒᵖ (Type v₁)).obj (opOp C)) ≅ coyoneda

Taking the `unop` of morphisms is a natural isomorphism.

Equations

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

Instances For

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

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

Equations

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

Instances For

source
instance CategoryTheory.Coyoneda.ULiftCoyoneda.instFullOppositeFunctorTypeUliftCoyoneda (C : Type u₁) [Category.{v₁, u₁} C] :
uliftCoyoneda.{w, v₁, u₁}.Full
source
instance CategoryTheory.Coyoneda.ULiftCoyoneda.instFaithfulOppositeFunctorTypeUliftCoyoneda (C : Type u₁) [Category.{v₁, u₁} C] :
uliftCoyoneda.{w, v₁, u₁}.Faithful
source
structure CategoryTheory.Functor.RepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C ᵒᵖ (Type v)) (Y : C) :
Type (max (max u₁ v) v₁)

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

- homEquiv {X : C} : (X ⟶ Y) ≃ F.obj (Opposite.op X)

  the natural bijection `(X ⟶ Y) ≃ F.obj (op X)`.

- homEquiv_comp {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y) : self.homEquiv (CategoryStruct.comp f g) = F.map f.op (self.homEquiv g)

Instances For

source
theorem CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (Opposite.op X')) (f : X ⟶ X') :
CategoryStruct.comp f (e.homEquiv.symm x) = e.homEquiv.symm (F.map f.op x)
source
def CategoryTheory.Functor.RepresentableBy.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {F F' : Functor C ᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) (e' : F ≅ F') :
F'.RepresentableBy Y

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

Equations

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

Instances For

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

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

- homEquiv {Y : C} : (X ⟶ Y) ≃ F.obj Y

  the natural bijection `(X ⟶ Y) ≃ F.obj Y`.

- homEquiv_comp {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y) : self.homEquiv (CategoryStruct.comp f g) = F.map g (self.homEquiv f)

Instances For

source
theorem CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') :
CategoryStruct.comp (e.homEquiv.symm y) g = e.homEquiv.symm (F.map g y)
source
def CategoryTheory.Functor.CorepresentableBy.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {F F' : Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) (e' : F ≅ F') :
F'.CorepresentableBy X

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

Equations

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

Instances For

source
theorem CategoryTheory.Functor.RepresentableBy.homEquiv_eq {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y) :
e.homEquiv f = F.map f.op (e.homEquiv (CategoryStruct.id Y))
source
theorem CategoryTheory.Functor.CorepresentableBy.homEquiv_eq {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y) :
e.homEquiv f = F.map f (e.homEquiv (CategoryStruct.id X))
source
def CategoryTheory.Functor.RepresentableBy.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y Y' : C} (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y') :
Y ≅ Y'

Representing objects are unique up to isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y Y' : C} (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y') :
(e.uniqueUpToIso e').hom = Yoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : C ᵒᵖ) => { hom := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, inv := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).hom
source
@[simp]
theorem CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y Y' : C} (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y') :
(e.uniqueUpToIso e').inv = Yoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : C ᵒᵖ) => { hom := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, inv := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).inv
source
def CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X X' : C} (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X') :
X ≅ X'

Corepresenting objects are unique up to isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X X' : C} (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X') :
(e.uniqueUpToIso e').inv = (Coyoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : C) => { hom := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, inv := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).inv).unop
source
@[simp]
theorem CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X X' : C} (e : F.CorepresentableBy X) (e' : F.CorepresentableBy X') :
(e.uniqueUpToIso e').hom = (Coyoneda.fullyFaithful.preimage (NatIso.ofComponents (fun (Z : C) => { hom := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, inv := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯).hom).unop
source
theorem CategoryTheory.Functor.RepresentableBy.ext {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y : C} {e e' : F.RepresentableBy Y} (h : e.homEquiv (CategoryStruct.id Y) = e'.homEquiv (CategoryStruct.id Y)) :
e = e'
source
theorem CategoryTheory.Functor.RepresentableBy.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v)} {Y : C} {e e' : F.RepresentableBy Y} :
e = e' ↔ e.homEquiv (CategoryStruct.id Y) = e'.homEquiv (CategoryStruct.id Y)
source
theorem CategoryTheory.Functor.CorepresentableBy.ext {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X : C} {e e' : F.CorepresentableBy X} (h : e.homEquiv (CategoryStruct.id X) = e'.homEquiv (CategoryStruct.id X)) :
e = e'
source
theorem CategoryTheory.Functor.CorepresentableBy.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X : C} {e e' : F.CorepresentableBy X} :
e = e' ↔ e.homEquiv (CategoryStruct.id X) = e'.homEquiv (CategoryStruct.id X)
source
def CategoryTheory.Functor.representableByEquiv {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C ᵒᵖ (Type v₁)} {Y : C} :
F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)

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

Equations

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

Instances For

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

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

Equations

- e.toIso = CategoryTheory.Functor.representableByEquiv e

Instances For

source
def CategoryTheory.Functor.corepresentableByEquiv {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v₁)} {X : C} :
F.CorepresentableBy X ≃ (coyoneda.obj (Opposite.op X) ≅ F)

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

Equations

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

Instances For

source
def CategoryTheory.Functor.CorepresentableBy.toIso {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v₁)} {X : C} (e : F.CorepresentableBy X) :
coyoneda.obj (Opposite.op X) ≅ F

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

Equations

- e.toIso = CategoryTheory.Functor.corepresentableByEquiv e

Instances For

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

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

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

Instances

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

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

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

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

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

Instances

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

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

source
instance CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ} :
(coyoneda.obj X).IsCorepresentable
source
noncomputable def CategoryTheory.Functor.reprX {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C ᵒᵖ (Type v)) [hF : F.IsRepresentable] :
C

The representing object for the representable functor `F`.

Equations

- F.reprX = ⋯.choose

Instances For

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

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

Equations

- F.representableBy = ⋯.some

Instances For

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

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

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

Equations

- F.reprW = F.representableBy.toIso

Instances For

source
theorem CategoryTheory.Functor.reprW_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C ᵒᵖ (Type v₁)) [F.IsRepresentable] (X : C ᵒᵖ) (f : Opposite.unop X ⟶ F.reprX) :
F.reprW.hom.app X f = F.map f.op F.reprx
source
noncomputable def CategoryTheory.Functor.coreprX {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type v)) [hF : F.IsCorepresentable] :
C

The representing object for the corepresentable functor `F`.

Equations

- F.coreprX = ⋯.choose

Instances For

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

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

Equations

- F.corepresentableBy = ⋯.some

Instances For

source
noncomputable def CategoryTheory.Functor.CorepresentableBy.isoCoreprX {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} [hF : F.IsCorepresentable] {Y : C} (e : F.CorepresentableBy Y) :
Y ≅ F.coreprX

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

Equations

- e.isoCoreprX = e.uniqueUpToIso F.corepresentableBy

Instances For

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

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

Equations

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

Instances For

source
noncomputable def CategoryTheory.Functor.coreprW {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type v₁)) [F.IsCorepresentable] :
coyoneda.obj (Opposite.op F.coreprX) ≅ F

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

Equations

- F.coreprW = F.corepresentableBy.toIso

Instances For

source
theorem CategoryTheory.Functor.coreprW_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type v₁)) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) :
F.coreprW.hom.app X f = F.map f F.coreprx
source
theorem CategoryTheory.isRepresentable_of_natIso {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C ᵒᵖ (Type v₁)) {G : Functor C ᵒᵖ (Type v₁)} (i : F ≅ G) [F.IsRepresentable] :
G.IsRepresentable
source
theorem CategoryTheory.corepresentable_of_natIso {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type v₁)) {G : Functor C (Type v₁)} (i : F ≅ G) [F.IsCorepresentable] :
G.IsCorepresentable
source
instance CategoryTheory.instIsCorepresentableIdType :
(Functor.id (Type v₁)).IsCorepresentable
source
instance CategoryTheory.prodCategoryInstance1 (C : Type u₁) [Category.{v₁, u₁} C] :
Category.{max u₁ v₁, max u₁ (max (v₁ + 1) u₁) v₁} (Functor C ᵒᵖ (Type v₁) × C ᵒᵖ)
Equations

- CategoryTheory.prodCategoryInstance1 C = CategoryTheory.prod' (CategoryTheory.Functor C ᵒᵖ (Type ?u.15)) C ᵒᵖ

source
instance CategoryTheory.prodCategoryInstance2 (C : Type u₁) [Category.{v₁, u₁} C] :
Category.{max u₁ v₁, max (max (max (v₁ + 1) u₁) v₁) u₁} (C ᵒᵖ × Functor C ᵒᵖ (Type v₁))
Equations

- CategoryTheory.prodCategoryInstance2 C = CategoryTheory.prod' C ᵒᵖ (CategoryTheory.Functor C ᵒᵖ (Type ?u.15))

source
def CategoryTheory.yonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type v₁)} :
(yoneda.obj X ⟶ F) ≃ F.obj (Opposite.op X)

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

Equations

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

Instances For

source
theorem CategoryTheory.yonedaEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type v₁)} (f : yoneda.obj X ⟶ F) :
yonedaEquiv f = f.app (Opposite.op X) (CategoryStruct.id X)
source
@[simp]
theorem CategoryTheory.yonedaEquiv_symm_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : C ᵒᵖ) (f : Opposite.unop Y ⟶ X) :
(yonedaEquiv.symm x).app Y f = F.map f.op x
source
theorem CategoryTheory.yonedaEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor C ᵒᵖ (Type v₁)} (f : yoneda.obj X ⟶ F) (g : Y ⟶ X) :
F.map g.op (yonedaEquiv f) = yonedaEquiv (CategoryStruct.comp (yoneda.map g) f)

See also `yonedaEquiv_naturality'` for a more general version.

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

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

source
theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F G : Functor C ᵒᵖ (Type v₁)} (α : yoneda.obj X ⟶ F) (β : F ⟶ G) :
yonedaEquiv (CategoryStruct.comp α β) = β.app (Opposite.op X) (yonedaEquiv α)
source
theorem CategoryTheory.yonedaEquiv_yoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
yonedaEquiv (yoneda.map f) = f
source
theorem CategoryTheory.yonedaEquiv_symm_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {X X' : C} (f : X' ⟶ X) (F : Functor C ᵒᵖ (Type v₁)) (x : F.obj (Opposite.op X)) :
CategoryStruct.comp (yoneda.map f) (yonedaEquiv.symm x) = yonedaEquiv.symm (F.map f.op x)
source
theorem CategoryTheory.yonedaEquiv_symm_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {F F' : Functor C ᵒᵖ (Type v₁)} (f : F ⟶ F') (x : F.obj (Opposite.op X)) :
CategoryStruct.comp (yonedaEquiv.symm x) f = yonedaEquiv.symm (f.app (Opposite.op X) x)
source
theorem CategoryTheory.map_yonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor C ᵒᵖ (Type v₁)} (f : yoneda.obj X ⟶ F) (g : Y ⟶ X) :
F.map g.op (yonedaEquiv f) = f.app (Opposite.op Y) g

See also `map_yonedaEquiv'` for a more general version.

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

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

source
theorem CategoryTheory.yonedaEquiv_symm_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (f : X ⟶ Y) {F : Functor C ᵒᵖ (Type v₁)} (t : F.obj X) :
yonedaEquiv.symm (F.map f t) = CategoryStruct.comp (yoneda.map f.unop) (yonedaEquiv.symm t)
source
theorem CategoryTheory.hom_ext_yoneda {C : Type u₁} [Category.{v₁, u₁} C] {P Q : Functor C ᵒᵖ (Type v₁)} {f g : P ⟶ Q} (h : ∀ (X : C) (p : yoneda.obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g) :
f = g

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

source
def CategoryTheory.yonedaEvaluation (C : Type u₁) [Category.{v₁, u₁} C] :
Functor (C ᵒᵖ × Functor C ᵒᵖ (Type v₁)) (Type (max u₁ v₁))

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

Equations

- CategoryTheory.yonedaEvaluation C = (CategoryTheory.evaluationUncurried C ᵒᵖ (Type ?u.19)).comp CategoryTheory.uliftFunctor.{?u.18, ?u.19}

Instances For

source
@[simp]
theorem CategoryTheory.yonedaEvaluation_map_down (C : Type u₁) [Category.{v₁, u₁} C] (P Q : C ᵒᵖ × Functor C ᵒᵖ (Type v₁)) (α : P ⟶ Q) (x : (yonedaEvaluation C).obj P) :
((yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
source
def CategoryTheory.yonedaPairing (C : Type u₁) [Category.{v₁, u₁} C] :
Functor (C ᵒᵖ × Functor C ᵒᵖ (Type v₁)) (Type (max u₁ v₁))

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

Equations

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

Instances For

source
theorem CategoryTheory.yonedaPairingExt (C : Type u₁) [Category.{v₁, u₁} C] {X : C ᵒᵖ × Functor C ᵒᵖ (Type v₁)} {x y : (yonedaPairing C).obj X} (w : ∀ (Y : C ᵒᵖ), x.app Y = y.app Y) :
x = y
source
theorem CategoryTheory.yonedaPairingExt_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ × Functor C ᵒᵖ (Type v₁)} {x y : (yonedaPairing C).obj X} :
x = y ↔ ∀ (Y : C ᵒᵖ), x.app Y = y.app Y
source
@[simp]
theorem CategoryTheory.yonedaPairing_map (C : Type u₁) [Category.{v₁, u₁} C] (P Q : C ᵒᵖ × Functor C ᵒᵖ (Type v₁)) (α : P ⟶ Q) (β : (yonedaPairing C).obj P) :
(yonedaPairing C).map α β = CategoryStruct.comp (yoneda.map α.1.unop) (CategoryStruct.comp β α.2)
source
def CategoryTheory.yonedaLemma (C : Type u₁) [Category.{v₁, u₁} C] :
yonedaPairing C ≅ yonedaEvaluation C

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

Equations

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

Instances For

source
def CategoryTheory.curriedYonedaLemma {C : Type u₁} [SmallCategory C] :
yoneda.op.comp coyoneda ≅ evaluation C ᵒᵖ (Type u₁)

The curried version of yoneda lemma when `C` is small.

Equations

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

Instances For

source
def CategoryTheory.largeCurriedYonedaLemma {C : Type u₁} [Category.{v₁, u₁} C] :
yoneda.op.comp coyoneda ≅ (evaluation C ᵒᵖ (Type v₁)).comp ((Functor.whiskeringRight (Functor C ᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁})

The curried version of the Yoneda lemma.

Equations

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

Instances For

source
def CategoryTheory.yonedaOpCompYonedaObj {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor C ᵒᵖ (Type v₁)) :
yoneda.op.comp (yoneda.obj P) ≅ P.comp uliftFunctor.{u₁, v₁}

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

Equations

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

Instances For

source
def CategoryTheory.curriedYonedaLemma' {C : Type u₁} [SmallCategory C] :
yoneda.comp ((Functor.whiskeringLeft C ᵒᵖ (Functor C ᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj yoneda.op) ≅ Functor.id (Functor C ᵒᵖ (Type u₁))

The curried version of yoneda lemma when `C` is small.

Equations

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

Instances For

source
theorem CategoryTheory.isIso_of_yoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryStruct.comp x f) :
IsIso f
source
theorem CategoryTheory.isIso_iff_yoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryStruct.comp x f
source
theorem CategoryTheory.isIso_iff_isIso_yoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
IsIso f ↔ ∀ (c : C), IsIso ((yoneda.map f).app (Opposite.op c))
source
def CategoryTheory.uliftYonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type (max w v₁))} :
(uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.op X)

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.uliftYonedaEquiv_symm_apply_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type (max w v₁))} (x : F.obj (Opposite.op X)) (Y : C ᵒᵖ) (y : (uliftYoneda.{w, v₁, u₁}.obj X).obj Y) :
(uliftYonedaEquiv.symm x).app Y y = F.map y.down.op x
source
theorem CategoryTheory.uliftYonedaEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type (max w v₁))} (τ : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) :
uliftYonedaEquiv τ = τ.app (Opposite.op X) { down := CategoryStruct.id X }
source
@[deprecated CategoryTheory.uliftYonedaEquiv (since := "2025-08-04")]
def CategoryTheory.yonedaCompUliftFunctorEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C ᵒᵖ (Type (max w v₁))} :
(uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.op X)

Alias of `CategoryTheory.uliftYonedaEquiv`.

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

Equations

- @CategoryTheory.yonedaCompUliftFunctorEquiv = @CategoryTheory.uliftYonedaEquiv

Instances For

source
theorem CategoryTheory.uliftYonedaEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} {F : Functor C ᵒᵖ (Type (max w v₁))} (f : uliftYoneda.{w, v₁, u₁}.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) :
F.map g (uliftYonedaEquiv f) = uliftYonedaEquiv (CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map g.unop) f)
source
theorem CategoryTheory.uliftYonedaEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F G : Functor C ᵒᵖ (Type (max w v₁))} (α : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) (β : F ⟶ G) :
uliftYonedaEquiv (CategoryStruct.comp α β) = β.app (Opposite.op X) (uliftYonedaEquiv α)
source
theorem CategoryTheory.uliftYonedaEquiv_symm_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (f : X ⟶ Y) {F : Functor C ᵒᵖ (Type (max w v₁))} (t : F.obj X) :
uliftYonedaEquiv.symm (F.map f t) = CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map f.unop) (uliftYonedaEquiv.symm t)
source
theorem CategoryTheory.uliftYonedaEquiv_symm_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (f : X ⟶ Y) {F : Functor C ᵒᵖ (Type (max w v₁))} (t : F.obj X) {Z : Functor C ᵒᵖ (Type (max w v₁))} (h : F ⟶ Z) :
CategoryStruct.comp (uliftYonedaEquiv.symm (F.map f t)) h = CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map f.unop) (CategoryStruct.comp (uliftYonedaEquiv.symm t) h)
source
@[simp]
theorem CategoryTheory.uliftYonedaEquiv_uliftYoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f) = { down := f }
source
theorem CategoryTheory.hom_ext_uliftYoneda {C : Type u₁} [Category.{v₁, u₁} C] {P Q : Functor C ᵒᵖ (Type (max w v₁))} {f g : P ⟶ Q} (h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g) :
f = g

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

source
def CategoryTheory.uliftYonedaOpCompCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] :
uliftYoneda.{w, v₁, u₁}.op.comp coyoneda ≅ (evaluation C ᵒᵖ (Type (max v₁ w))).comp ((Functor.whiskeringRight (Functor C ᵒᵖ (Type (max v₁ w))) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj uliftFunctor.{u₁, max v₁ w})

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

Equations

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

Instances For

source
def CategoryTheory.coyonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C (Type v₁)} :
(coyoneda.obj (Opposite.op X) ⟶ F) ≃ F.obj X

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

Equations

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

Instances For

source
theorem CategoryTheory.coyonedaEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C (Type v₁)} (f : coyoneda.obj (Opposite.op X) ⟶ F) :
coyonedaEquiv f = f.app X (CategoryStruct.id X)
source
@[simp]
theorem CategoryTheory.coyonedaEquiv_symm_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C (Type v₁)} (x : F.obj X) (Y : C) (f : X ⟶ Y) :
(coyonedaEquiv.symm x).app Y f = F.map f x
source
theorem CategoryTheory.coyonedaEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor C (Type v₁)} (f : coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) :
F.map g (coyonedaEquiv f) = coyonedaEquiv (CategoryStruct.comp (coyoneda.map g.op) f)
source
theorem CategoryTheory.coyonedaEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F G : Functor C (Type v₁)} (α : coyoneda.obj (Opposite.op X) ⟶ F) (β : F ⟶ G) :
coyonedaEquiv (CategoryStruct.comp α β) = β.app X (coyonedaEquiv α)
source
theorem CategoryTheory.coyonedaEquiv_coyoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
coyonedaEquiv (coyoneda.map f.op) = f
source
theorem CategoryTheory.map_coyonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor C (Type v₁)} (f : coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) :
F.map g (coyonedaEquiv f) = f.app Y g
source
theorem CategoryTheory.coyonedaEquiv_symm_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : Functor C (Type v₁)} (t : F.obj X) :
coyonedaEquiv.symm (F.map f t) = CategoryStruct.comp (coyoneda.map f.op) (coyonedaEquiv.symm t)
source
def CategoryTheory.coyonedaEvaluation (C : Type u₁) [Category.{v₁, u₁} C] :
Functor (C × Functor C (Type v₁)) (Type (max u₁ v₁))

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

Equations

- CategoryTheory.coyonedaEvaluation C = (CategoryTheory.evaluationUncurried C (Type ?u.19)).comp CategoryTheory.uliftFunctor.{?u.18, ?u.19}

Instances For

source
@[simp]
theorem CategoryTheory.coyonedaEvaluation_map_down (C : Type u₁) [Category.{v₁, u₁} C] (P Q : C × Functor C (Type v₁)) (α : P ⟶ Q) (x : (coyonedaEvaluation C).obj P) :
((coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
source
def CategoryTheory.coyonedaPairing (C : Type u₁) [Category.{v₁, u₁} C] :
Functor (C × Functor C (Type v₁)) (Type (max u₁ v₁))

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

Equations

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

Instances For

source
theorem CategoryTheory.coyonedaPairingExt (C : Type u₁) [Category.{v₁, u₁} C] {X : C × Functor C (Type v₁)} {x y : (coyonedaPairing C).obj X} (w : ∀ (Y : C), x.app Y = y.app Y) :
x = y
source
theorem CategoryTheory.coyonedaPairingExt_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C × Functor C (Type v₁)} {x y : (coyonedaPairing C).obj X} :
x = y ↔ ∀ (Y : C), x.app Y = y.app Y
source
@[simp]
theorem CategoryTheory.coyonedaPairing_map (C : Type u₁) [Category.{v₁, u₁} C] (P Q : C × Functor C (Type v₁)) (α : P ⟶ Q) (β : (coyonedaPairing C).obj P) :
(coyonedaPairing C).map α β = CategoryStruct.comp (coyoneda.map α.1.op) (CategoryStruct.comp β α.2)
source
def CategoryTheory.coyonedaLemma (C : Type u₁) [Category.{v₁, u₁} C] :
coyonedaPairing C ≅ coyonedaEvaluation C

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

Equations

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

Instances For

source
def CategoryTheory.curriedCoyonedaLemma {C : Type u₁} [SmallCategory C] :
coyoneda.rightOp.comp coyoneda ≅ evaluation C (Type u₁)

The curried version of coyoneda lemma when `C` is small.

Equations

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

Instances For

source
def CategoryTheory.largeCurriedCoyonedaLemma {C : Type u₁} [Category.{v₁, u₁} C] :
coyoneda.rightOp.comp coyoneda ≅ (evaluation C (Type v₁)).comp ((Functor.whiskeringRight (Functor C (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁})

The curried version of the Coyoneda lemma.

Equations

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

Instances For

source
def CategoryTheory.coyonedaCompYonedaObj {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor C (Type v₁)) :
coyoneda.rightOp.comp (yoneda.obj P) ≅ P.comp uliftFunctor.{u₁, v₁}

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

Equations

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

Instances For

source
def CategoryTheory.curriedCoyonedaLemma' {C : Type u₁} [SmallCategory C] :
yoneda.comp ((Functor.whiskeringLeft C (Functor C (Type u₁))ᵒᵖ (Type u₁)).obj coyoneda.rightOp) ≅ Functor.id (Functor C (Type u₁))

The curried version of coyoneda lemma when `C` is small.

Equations

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

Instances For

source
theorem CategoryTheory.isIso_of_coyoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryStruct.comp f x) :
IsIso f
source
theorem CategoryTheory.isIso_iff_coyoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryStruct.comp f x
source
theorem CategoryTheory.isIso_iff_isIso_coyoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
IsIso f ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)
source
def CategoryTheory.uliftCoyonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ} {F : Functor C (Type (max w v₁))} :
(uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.unop X)

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.uliftCoyonedaEquiv_symm_apply_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ} {F : Functor C (Type (max w v₁))} (x : F.obj (Opposite.unop X)) (Y : C) (y : (uliftCoyoneda.{w, v₁, u₁}.obj X).obj Y) :
(uliftCoyonedaEquiv.symm x).app Y y = F.map y.down x
source
theorem CategoryTheory.uliftCoyonedaEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ} {F : Functor C (Type (max w v₁))} (τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) :
uliftCoyonedaEquiv τ = τ.app (Opposite.unop X) { down := CategoryStruct.id (Opposite.unop X) }
source
@[deprecated CategoryTheory.uliftCoyonedaEquiv (since := "2025-08-04")]
def CategoryTheory.coyonedaCompUliftFunctorEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ} {F : Functor C (Type (max w v₁))} :
(uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.unop X)

Alias of `CategoryTheory.uliftCoyonedaEquiv`.

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

Equations

- @CategoryTheory.coyonedaCompUliftFunctorEquiv = @CategoryTheory.uliftCoyonedaEquiv

Instances For

source
theorem CategoryTheory.uliftCoyonedaEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor C (Type (max w v₁))} (f : uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) :
F.map g (uliftCoyonedaEquiv f) = uliftCoyonedaEquiv (CategoryStruct.comp (uliftCoyoneda.{w, v₁, u₁}.map g.op) f)
source
theorem CategoryTheory.uliftCoyonedaEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C ᵒᵖ} {F G : Functor C (Type (max w v₁))} (α : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) (β : F ⟶ G) :
uliftCoyonedaEquiv (CategoryStruct.comp α β) = β.app (Opposite.unop X) (uliftCoyonedaEquiv α)
source
theorem CategoryTheory.uliftCoyonedaEquiv_symm_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : Functor C (Type (max w v₁))} (t : F.obj X) :
uliftCoyonedaEquiv.symm (F.map f t) = CategoryStruct.comp (uliftCoyoneda.{w, v₁, u₁}.map f.op) (uliftCoyonedaEquiv.symm t)
source
theorem CategoryTheory.uliftCoyonedaEquiv_symm_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : Functor C (Type (max w v₁))} (t : F.obj X) {Z : Functor C (Type (max w v₁))} (h : F ⟶ Z) :
CategoryStruct.comp (uliftCoyonedaEquiv.symm (F.map f t)) h = CategoryStruct.comp (uliftCoyoneda.{w, v₁, u₁}.map f.op) (CategoryStruct.comp (uliftCoyonedaEquiv.symm t) h)
source
@[simp]
theorem CategoryTheory.uliftCoyonedaEquiv_uliftCoyoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (f : X ⟶ Y) :
uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f) = { down := f.unop }
source
theorem CategoryTheory.hom_ext_uliftCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] {P Q : Functor C (Type (max w v₁))} {f g : P ⟶ Q} (h : ∀ (X : C ᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g) :
f = g

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

source
def CategoryTheory.uliftCoyonedaRightOpCompCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] :
uliftCoyoneda.{w, v₁, u₁}.rightOp.comp coyoneda ≅ (evaluation C (Type (max v₁ w))).comp ((Functor.whiskeringRight (Functor C (Type (max v₁ w))) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj uliftFunctor.{u₁, max v₁ w})

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

Equations

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

Instances For

source
def CategoryTheory.yonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v₁, u_1} D] (F : Functor C D) (X : C) :
yoneda.obj X ⟶ F.op.comp (yoneda.obj (F.obj X))

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.yonedaMap_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v₁, u_1} D] (F : Functor C D) {Y : C} {X : C ᵒᵖ} (f : Opposite.unop X ⟶ Y) :
(yonedaMap F Y).app X f = F.map f
source
def CategoryTheory.uliftYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ F.op.comp (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X))

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.uliftYonedaMap_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {Y : C} {X : C ᵒᵖ} (f : Opposite.unop X ⟶ Y) :
(uliftYonedaMap F Y).app X { down := f } = { down := F.map f }
source
def CategoryTheory.Functor.sectionsEquivHom {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type u₂)) (X : Type u₂) [Unique X] :
↑F.sections ≃ ((const C).obj X ⟶ F)

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

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Functor.sectionsEquivHom_apply_app {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type u₂)) (X : Type u₂) [Unique X] (s : ↑F.sections) (j : C) (x : ((const C).obj X).obj j) :
((F.sectionsEquivHom X) s).app j x = ↑s j
source
theorem CategoryTheory.Functor.sectionsEquivHom_naturality {C : Type u₁} [Category.{v₁, u₁} C] {F G : Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (x : ↑F.sections) :
(G.sectionsEquivHom X) ((sectionsFunctor C).map f x) = CategoryStruct.comp ((F.sectionsEquivHom X) x) f
source
theorem CategoryTheory.Functor.sectionsEquivHom_naturality_symm {C : Type u₁} [Category.{v₁, u₁} C] {F G : Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (τ : (const C).obj X ⟶ F) :
(G.sectionsEquivHom X).symm (CategoryStruct.comp τ f) = (sectionsFunctor C).map f ((F.sectionsEquivHom X).symm τ)
source
noncomputable def CategoryTheory.sectionsFunctorNatIsoCoyoneda {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] :
Functor.sectionsFunctor C ≅ coyoneda.obj (Opposite.op ((Functor.const C).obj X))

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

Equations

- CategoryTheory.sectionsFunctorNatIsoCoyoneda X = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor C (Type (max ?u.35 ?u.34))) => (F.sectionsEquivHom X).toIso) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : Functor C (Type (max u₁ u₂))) (a✝ : (Functor.sectionsFunctor C).obj X✝) (j : C) (x : ((Functor.const C).obj X).obj j) :
((sectionsFunctorNatIsoCoyoneda X).hom.app X✝ a✝).app j x = ↑a✝ j
source
@[simp]
theorem CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_coe {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : Functor C (Type (max u₁ u₂))) (a✝ : (coyoneda.obj (Opposite.op ((Functor.const C).obj X))).obj X✝) (j : C) :
↑((sectionsFunctorNatIsoCoyoneda X).inv.app X✝ a✝) j = a✝.app j default
source
def CategoryTheory.Functor.FullyFaithful.homNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) :
F.op.comp (uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)) ≅ uliftYoneda.{v₂, v₁, u₁}.obj X

`FullyFaithful.homEquiv` as a natural isomorphism.

Equations

- hF.homNatIso X = CategoryTheory.NatIso.ofComponents (fun (Y : C ᵒᵖ) => (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (uliftYoneda.{v₂, v₁, u₁}.obj X).obj X✝) :
((hF.homNatIso X).inv.app X✝ a✝).down = F.map a✝.down
source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (F.op.comp (uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X))).obj X✝) :
((hF.homNatIso X).hom.app X✝ a✝).down = hF.preimage a✝.down
source
@[deprecated CategoryTheory.Functor.FullyFaithful.homNatIso (since := "2025-10-28")]
def CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) :
F.op.comp (yoneda.obj (F.obj X)) ≅ uliftYoneda.{v₂, v₁, u₁}.obj X

`FullyFaithful.homEquiv` as a natural isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (F.op.comp (yoneda.obj (F.obj X))).obj X✝) :
((hF.homNatIsoMaxRight X).hom.app X✝ a✝).down = hF.preimage a✝
source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (uliftYoneda.{v₂, v₁, u₁}.obj X).obj X✝) :
(hF.homNatIsoMaxRight X).inv.app X✝ a✝ = F.map a✝.down
source
def CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) :
F.comp (uliftYoneda.{v₁, v₂, u₂}.comp ((whiskeringLeft C ᵒᵖ D ᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅ uliftYoneda.{v₂, v₁, u₁}

`FullyFaithful.homEquiv` as a natural isomorphism.

Equations

- hF.compUliftYonedaCompWhiskeringLeft = CategoryTheory.NatIso.ofComponents (fun (X : C) => hF.homNatIso X) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (F.op.comp (uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X))).obj X✝) :
((hF.compUliftYonedaCompWhiskeringLeft.hom.app X).app X✝ a✝).down = hF.preimage a✝.down
source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (uliftYoneda.{v₂, v₁, u₁}.obj X).obj X✝) :
((hF.compUliftYonedaCompWhiskeringLeft.inv.app X).app X✝ a✝).down = F.map a✝.down
source
@[deprecated CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft (since := "2025-10-20")]
def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) :
F.comp (uliftYoneda.{v₁, v₂, u₂}.comp ((whiskeringLeft C ᵒᵖ D ᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅ uliftYoneda.{v₂, v₁, u₁}

Alias of `CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft`.

`FullyFaithful.homEquiv` as a natural isomorphism.

Equations

- @CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft = @CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft

Instances For

source
@[deprecated CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft (since := "2025-10-28")]
def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) :
F.comp (yoneda.comp ((whiskeringLeft C ᵒᵖ D ᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅ uliftYoneda.{v₂, v₁, u₁}

`FullyFaithful.homEquiv` as a natural isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : ((F.comp (yoneda.comp ((whiskeringLeft C ᵒᵖ D ᵒᵖ (Type (max v₁ v₂))).obj F.op))).obj X).obj X✝) :
((hF.compYonedaCompWhiskeringLeftMaxRight.hom.app X).app X✝ a✝).down = hF.preimage a✝
source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : C ᵒᵖ) (a✝ : (uliftYoneda.{v₂, v₁, u₁}.obj X).obj X✝) :
(hF.compYonedaCompWhiskeringLeftMaxRight.inv.app X).app X✝ a✝ = F.map a✝.down
source
def CategoryTheory.Functor.FullyFaithful.homNatIso' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) :
F.comp (uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj X))) ≅ uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op X)

`FullyFaithful.homEquiv` as a natural isomorphism, using coyoneda.

Equations

- hF.homNatIso' X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.homNatIso'_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X X✝ : C) (a✝ : (F.comp (uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj X)))).obj X✝) :
((hF.homNatIso' X).hom.app X✝ a✝).down = hF.preimage a✝.down
source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.homNatIso'_inv_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X X✝ : C) (a✝ : (uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op X)).obj X✝) :
((hF.homNatIso' X).inv.app X✝ a✝).down = F.map a✝.down
source
def CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) :
F.op.comp (uliftCoyoneda.{v₁, v₂, u₂}.comp ((whiskeringLeft C D (Type (max v₁ v₂))).obj F)) ≅ uliftCoyoneda.{v₂, v₁, u₁}

`FullyFaithful.homEquiv` as a natural isomorphism, using coyoneda.

Equations

- hF.compUliftCoyonedaCompWhiskeringLeft = CategoryTheory.NatIso.ofComponents (fun (X : C ᵒᵖ) => hF.homNatIso' (Opposite.unop X)) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C ᵒᵖ) (X✝ : C) (a✝ : (uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op (Opposite.unop X))).obj X✝) :
((hF.compUliftCoyonedaCompWhiskeringLeft.inv.app X).app X✝ a✝).down = F.map a✝.down
source
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C ᵒᵖ) (X✝ : C) (a✝ : (F.comp (uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj (Opposite.unop X))))).obj X✝) :
((hF.compUliftCoyonedaCompWhiskeringLeft.hom.app X).app X✝ a✝).down = hF.preimage a✝.down