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

@[simp]

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

@[simp]

theorem CategoryTheory.yoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : C} (f : X ⟶ Y) (Y_1 : Cᵒᵖ) (g : ((fun X => CategoryTheory.Functor.mk { obj := fun Y => Y.unop ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop g }) X).obj Y_1), Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types ((fun X => CategoryTheory.Functor.mk { obj := fun Y => Y.unop ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop g }) X) ((fun X => CategoryTheory.Functor.mk { obj := fun Y => Y.unop ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop g }) Y) (CategoryTheory.yoneda.map f) Y_1 g = CategoryTheory.CategoryStruct.comp g f

@[simp]

theorem CategoryTheory.yoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (g : X.unop ⟶ X), Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.yoneda.obj X).toPrefunctor X Y f g = CategoryTheory.CategoryStruct.comp f.unop g

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

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

See https://stacks.math.columbia.edu/tag/001O.

Equations

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

@[simp]

theorem CategoryTheory.coyoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) : ∀ {X Y : C} (f : X ⟶ Y) (g : X.unop ⟶ X), C.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.coyoneda.obj X).toPrefunctor X Y f g = CategoryTheory.CategoryStruct.comp g f

@[simp]

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

@[simp]

theorem CategoryTheory.coyoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (Y_1 : C) (g : ((fun X => CategoryTheory.Functor.mk { obj := fun Y => X.unop ⟶ Y, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp g f }) X).obj Y_1), C.app inst✝ (Type v₁) CategoryTheory.types ((fun X => CategoryTheory.Functor.mk { obj := fun Y => X.unop ⟶ Y, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp g f }) X) ((fun X => CategoryTheory.Functor.mk { obj := fun Y => X.unop ⟶ Y, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp g f }) Y) (CategoryTheory.coyoneda.map f) Y_1 g = CategoryTheory.CategoryStruct.comp f.unop g

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

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

Equations

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

theorem CategoryTheory.Yoneda.obj_map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Opposite.op X ⟶ Opposite.op Y) : Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.yoneda.obj X).toPrefunctor (Opposite.op X) (Opposite.op Y) f (CategoryTheory.CategoryStruct.id X) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.yoneda.obj (Opposite.op Y).unop) (CategoryTheory.yoneda.obj (Opposite.op X).unop) (CategoryTheory.yoneda.map f.unop) (Opposite.op Y) (CategoryTheory.CategoryStruct.id Y)

@[simp]

theorem CategoryTheory.Yoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (α : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y) {Z : C} {Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) : CategoryTheory.CategoryStruct.comp f (Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) (CategoryTheory.yoneda.obj Y) α (Opposite.op Z') h) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) (CategoryTheory.yoneda.obj Y) α (Opposite.op Z) (CategoryTheory.CategoryStruct.comp f h)

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

The Yoneda embedding is full.

See https://stacks.math.columbia.edu/tag/001P.

Equations

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

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

The Yoneda embedding is faithful.

See https://stacks.math.columbia.edu/tag/001P.

Equations

• @CategoryTheory.Yoneda.yoneda_faithful = @CategoryTheory.Yoneda.yoneda_faithful.proof_1

def CategoryTheory.Yoneda.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : C) (p : {Z : C} → (Z ⟶ X) → (Z ⟶ Y)) (q : {Z : C} → (Z ⟶ Y) → (Z ⟶ X)) (h₁ : ∀ {Z : C} (f : Z ⟶ X), q Z (p Z f) = f) (h₂ : ∀ {Z : C} (f : Z ⟶ Y), p Z (q Z f) = f) (n : ∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ X), p Z' (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f (p Z 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

• CategoryTheory.Yoneda.ext X Y p q h₁ h₂ n = CategoryTheory.Functor.preimageIso CategoryTheory.yoneda (CategoryTheory.NatIso.ofComponents fun Z => CategoryTheory.Iso.mk (p Z.unop) (q Z.unop))

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

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

@[simp]

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

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

Equations

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

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

Equations

• @CategoryTheory.Coyoneda.coyoneda_faithful = @CategoryTheory.Coyoneda.coyoneda_faithful.proof_1

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

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

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

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

Equations

• CategoryTheory.Coyoneda.punitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.mk (fun f => f PUnit.unit) fun x x_1 => x

@[simp]

theorem CategoryTheory.Coyoneda.objOpOp_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X))).obj X), Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X))) (CategoryTheory.yoneda.obj X) (CategoryTheory.Coyoneda.objOpOp X).hom X a = ↑(CategoryTheory.opEquiv (Opposite.op X) X) a

@[simp]

theorem CategoryTheory.Coyoneda.objOpOp_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.yoneda.obj X).obj X), (CategoryTheory.Coyoneda.objOpOp X).inv.app X a = ↑(CategoryTheory.opEquiv (Opposite.op X) X).symm a

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

Taking the unop of morphisms is a natural isomorphism.

Equations

• CategoryTheory.Coyoneda.objOpOp X = CategoryTheory.NatIso.ofComponents fun x => Equiv.toIso (CategoryTheory.opEquiv (Opposite.op (Opposite.op X)).unop x)

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

• has_representation : ∃ X f, CategoryTheory.IsIso f

  Hom(-,X) ≅ F via f

A functor F : Cᵒᵖ ⥤ Type v₁ is representable if there is object X so F ≅ yoneda.obj X.

See https://stacks.math.columbia.edu/tag/001Q.

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

Equations

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

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

• has_corepresentation : ∃ X f, CategoryTheory.IsIso f

  Hom(X,-) ≅ F via f

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

See https://stacks.math.columbia.edu/tag/001Q.

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

Equations

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

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

The representing object for the representable functor F.

Equations

• CategoryTheory.Functor.reprX F = Exists.choose (_ : ∃ X f, CategoryTheory.IsIso f)

noncomputable def CategoryTheory.Functor.reprF {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [CategoryTheory.Functor.Representable F] : CategoryTheory.yoneda.obj (CategoryTheory.Functor.reprX F) ⟶ F

The (forward direction of the) isomorphism witnessing F is representable.

Equations

• CategoryTheory.Functor.reprF F = Exists.choose (_ : ∃ f, CategoryTheory.IsIso f)

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

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

Equations

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

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

Equations

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

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

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

Equations

• CategoryTheory.Functor.reprW F = CategoryTheory.asIso (CategoryTheory.Functor.reprF F)

@[simp]

theorem CategoryTheory.Functor.reprW_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [CategoryTheory.Functor.Representable F] : (CategoryTheory.Functor.reprW F).hom = CategoryTheory.Functor.reprF F

theorem CategoryTheory.Functor.reprW_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [CategoryTheory.Functor.Representable F] (X : Cᵒᵖ) (f : X.unop ⟶ CategoryTheory.Functor.reprX F) : Type v₁.hom CategoryTheory.types ((CategoryTheory.yoneda.obj (CategoryTheory.Functor.reprX F)).obj X) (F.obj X) ((CategoryTheory.Functor.reprW F).app X) f = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (Opposite.op (CategoryTheory.Functor.reprX F)) (Opposite.op X.unop) f.op (CategoryTheory.Functor.reprx F)

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

The representing object for the corepresentable functor F.

Equations

• CategoryTheory.Functor.coreprX F = (Exists.choose (_ : ∃ X f, CategoryTheory.IsIso f)).unop

noncomputable def CategoryTheory.Functor.coreprF {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [CategoryTheory.Functor.Corepresentable F] : CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Functor.coreprX F)) ⟶ F

The (forward direction of the) isomorphism witnessing F is corepresentable.

Equations

• CategoryTheory.Functor.coreprF F = Exists.choose (_ : ∃ f, CategoryTheory.IsIso f)

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

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

Equations

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

instance CategoryTheory.Functor.instIsIsoFunctorTypeTypesCategoryObjOppositeToQuiverToCategoryStructOppositeToQuiverToCategoryStructToPrefunctorCoyonedaOpCoreprXCoreprF {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [CategoryTheory.Functor.Corepresentable F] : CategoryTheory.IsIso (CategoryTheory.Functor.coreprF F)

Equations

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

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

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

Equations

• CategoryTheory.Functor.coreprW F = CategoryTheory.asIso (CategoryTheory.Functor.coreprF F)

theorem CategoryTheory.Functor.coreprW_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [CategoryTheory.Functor.Corepresentable F] (X : C) (f : CategoryTheory.Functor.coreprX F ⟶ X) : Type v₁.hom CategoryTheory.types ((CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Functor.coreprX F))).obj X) (F.obj X) ((CategoryTheory.Functor.coreprW F).app X) f = C.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (CategoryTheory.Functor.coreprX F) X f (CategoryTheory.Functor.coreprx F)

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

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

instance CategoryTheory.instCorepresentableTypeTypesId : CategoryTheory.Functor.Corepresentable (CategoryTheory.Functor.id (Type v₁))

Equations

• CategoryTheory.instCorepresentableTypeTypesId = CategoryTheory.instCorepresentableTypeTypesId.proof_1

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

Equations

• CategoryTheory.prodCategoryInstance1 C = CategoryTheory.prod (CategoryTheory.Functor Cᵒᵖ (Type v₁)) Cᵒᵖ

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

Equations

• CategoryTheory.prodCategoryInstance2 C = CategoryTheory.prod Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type v₁))

def CategoryTheory.yonedaEvaluation (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.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.Functor.comp (CategoryTheory.evaluationUncurried Cᵒᵖ (Type v₁)) CategoryTheory.uliftFunctor.{u₁, v₁}

@[simp]

theorem CategoryTheory.yonedaEvaluation_map_down (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (x : (CategoryTheory.yonedaEvaluation C).obj P) : ((CategoryTheory.yonedaEvaluation C).map α x).down = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types P.snd Q.snd α.snd Q.fst (Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver P.snd.toPrefunctor P.fst Q.fst α.fst x.down)

def CategoryTheory.yonedaPairing (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.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.

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

@[simp]

theorem CategoryTheory.yonedaPairing_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.yonedaPairing C).obj P) : (CategoryTheory.yonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.fst.unop) (CategoryTheory.CategoryStruct.comp β α.snd)

def CategoryTheory.yonedaLemma (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.yonedaPairing C ≅ CategoryTheory.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.

See https://stacks.math.columbia.edu/tag/001P.

Equations

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

@[simp]

theorem CategoryTheory.yonedaSections_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : ∀ (a : (CategoryTheory.yonedaEvaluation C).obj (Opposite.op X, F)) (X : Cᵒᵖ) (a_1 : ((CategoryTheory.Functor.prod CategoryTheory.yoneda.op (CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type v₁)))).obj (Opposite.op X, F)).fst.unop.obj X), Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types ((CategoryTheory.Functor.prod CategoryTheory.yoneda.op (CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type v₁)))).obj (Opposite.op X, F)).fst.unop ((CategoryTheory.Functor.prod CategoryTheory.yoneda.op (CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type v₁)))).obj (Opposite.op X, F)).snd ((CategoryTheory.yonedaSections X F).inv a) X a_1 = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (Opposite.op X) X a_1.op a.down

@[simp]

theorem CategoryTheory.yonedaSections_hom_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : ∀ (a : (CategoryTheory.yonedaPairing C).obj (Opposite.op X, F)), ((CategoryTheory.yonedaSections X F).hom a).down = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) F a (Opposite.op X) (CategoryTheory.CategoryStruct.id X)

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

The isomorphism between yoneda.obj X ⟶ F and F.obj (op X) (we need to insert a ulift to get the universes right!) given by the Yoneda lemma.

Equations

• CategoryTheory.yonedaSections X F = (CategoryTheory.yonedaLemma C).app (Opposite.op X, F)

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

• CategoryTheory.yonedaEquiv = (CategoryTheory.yonedaSections X F).trans Equiv.ulift

@[simp]

theorem CategoryTheory.yonedaEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) : ↑CategoryTheory.yonedaEquiv f = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) F f (Opposite.op X) (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem CategoryTheory.yonedaEquiv_symm_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Y.unop ⟶ X) : Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) F (↑CategoryTheory.yonedaEquiv.symm x) Y f = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (Opposite.op X) (Opposite.op Y.unop) f.op x

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

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

theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X ⟶ F) (β : F ⟶ G) : ↑CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types F G β (Opposite.op X) (↑CategoryTheory.yonedaEquiv α)

theorem CategoryTheory.yonedaEquiv_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X.unop ⟶ F) (β : F ⟶ G) : ↑CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types F G β X (↑CategoryTheory.yonedaEquiv α)

@[simp]

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

theorem CategoryTheory.yonedaEquiv_symm_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (t : F.obj X) : ↑CategoryTheory.yonedaEquiv.symm (Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type v₁) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Y f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (↑CategoryTheory.yonedaEquiv.symm t)

def CategoryTheory.yonedaSectionsSmall {C : Type u₁} [CategoryTheory.SmallCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.yoneda.obj X ⟶ F) ≅ F.obj (Opposite.op X)

When C is a small category, we can restate the isomorphism from yoneda_sections without having to change universes.

Equations

• CategoryTheory.yonedaSectionsSmall X F = CategoryTheory.yonedaSections X F ≪≫ CategoryTheory.uliftTrivial (F.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.yonedaSectionsSmall_hom {C : Type u₁} [CategoryTheory.SmallCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (f : CategoryTheory.yoneda.obj X ⟶ F) : Type u₁.hom CategoryTheory.types (CategoryTheory.yoneda.obj X ⟶ F) (F.obj (Opposite.op X)) (CategoryTheory.yonedaSectionsSmall X F) f = Cᵒᵖ.app CategoryTheory.Category.opposite (Type u₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) F f { unop := X } (CategoryTheory.CategoryStruct.id { unop := X }.unop)

@[simp]

theorem CategoryTheory.yonedaSectionsSmall_inv_app_apply {C : Type u₁} [CategoryTheory.SmallCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (t : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Y.unop ⟶ X) : Cᵒᵖ.app CategoryTheory.Category.opposite (Type u₁) CategoryTheory.types (CategoryTheory.yoneda.obj X) F (Type u₁.inv CategoryTheory.types (CategoryTheory.yoneda.obj X ⟶ F) (F.obj (Opposite.op X)) (CategoryTheory.yonedaSectionsSmall X F) t) Y f = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type u₁) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (Opposite.op X) (Opposite.op Y.unop) f.op t

def CategoryTheory.curriedYonedaLemma {C : Type u₁} [CategoryTheory.SmallCategory C] : CategoryTheory.Functor.comp CategoryTheory.yoneda.op CategoryTheory.coyoneda ≅ CategoryTheory.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.

def CategoryTheory.curriedYonedaLemma' {C : Type u₁} [CategoryTheory.SmallCategory C] : CategoryTheory.Functor.comp CategoryTheory.yoneda ((CategoryTheory.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj CategoryTheory.yoneda.op) ≅ CategoryTheory.Functor.id (CategoryTheory.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.

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