category_theory.yoneda - mathlib3 docs

@[simp]

theorem category_theory.yoneda_map_app {C : Type u₁} [category_theory.category C] (X X' : C) (f : X ⟶ X') (Y : Cᵒᵖ) (g : {obj := λ (Y : Cᵒᵖ), opposite.unop Y ⟶ X, map := λ (Y Y' : Cᵒᵖ) (f : Y ⟶ Y') (g : opposite.unop Y ⟶ X), f.unop ≫ g, map_id' := _, map_comp' := _}.obj Y) :

(category_theory.yoneda.map f).app Y g = g ≫ f

source

def category_theory.yoneda {C : Type u₁} [category_theory.category C] :

C ⥤ Cᵒᵖ ⥤ Type v₁

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

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

Equations

category_theory.yoneda = {obj := λ (X : C), {obj := λ (Y : Cᵒᵖ), opposite.unop Y ⟶ X, map := λ (Y Y' : Cᵒᵖ) (f : Y ⟶ Y') (g : opposite.unop Y ⟶ X), f.unop ≫ g, map_id' := _, map_comp' := _}, map := λ (X X' : C) (f : X ⟶ X'), {app := λ (Y : Cᵒᵖ) (g : {obj := λ (Y : Cᵒᵖ), opposite.unop Y ⟶ X, map := λ (Y Y' : Cᵒᵖ) (f : Y ⟶ Y') (g : opposite.unop Y ⟶ X), f.unop ≫ g, map_id' := _, map_comp' := _}.obj Y), g ≫ f, naturality' := _}, map_id' := _, map_comp' := _}

Instances for category_theory.yoneda

source

@[simp]

theorem category_theory.yoneda_obj_obj {C : Type u₁} [category_theory.category C] (X : C) (Y : Cᵒᵖ) :

(category_theory.yoneda.obj X).obj Y = (opposite.unop Y ⟶ X)

source

@[simp]

theorem category_theory.yoneda_obj_map {C : Type u₁} [category_theory.category C] (X : C) (Y Y' : Cᵒᵖ) (f : Y ⟶ Y') (g : opposite.unop Y ⟶ X) :

(category_theory.yoneda.obj X).map f g = f.unop ≫ g

source

@[simp]

theorem category_theory.coyoneda_obj_obj {C : Type u₁} [category_theory.category C] (X : Cᵒᵖ) (Y : C) :

(category_theory.coyoneda.obj X).obj Y = (opposite.unop X ⟶ Y)

source

def category_theory.coyoneda {C : Type u₁} [category_theory.category C] :

Cᵒᵖ ⥤ C ⥤ Type v₁

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

Equations

category_theory.coyoneda = {obj := λ (X : Cᵒᵖ), {obj := λ (Y : C), opposite.unop X ⟶ Y, map := λ (Y Y' : C) (f : Y ⟶ Y') (g : opposite.unop X ⟶ Y), g ≫ f, map_id' := _, map_comp' := _}, map := λ (X X' : Cᵒᵖ) (f : X ⟶ X'), {app := λ (Y : C) (g : {obj := λ (Y : C), opposite.unop X ⟶ Y, map := λ (Y Y' : C) (f : Y ⟶ Y') (g : opposite.unop X ⟶ Y), g ≫ f, map_id' := _, map_comp' := _}.obj Y), f.unop ≫ g, naturality' := _}, map_id' := _, map_comp' := _}

Instances for category_theory.coyoneda

source

@[simp]

theorem category_theory.coyoneda_map_app {C : Type u₁} [category_theory.category C] (X X' : Cᵒᵖ) (f : X ⟶ X') (Y : C) (g : {obj := λ (Y : C), opposite.unop X ⟶ Y, map := λ (Y Y' : C) (f : Y ⟶ Y') (g : opposite.unop X ⟶ Y), g ≫ f, map_id' := _, map_comp' := _}.obj Y) :

(category_theory.coyoneda.map f).app Y g = f.unop ≫ g

source

@[simp]

theorem category_theory.coyoneda_obj_map {C : Type u₁} [category_theory.category C] (X : Cᵒᵖ) (Y Y' : C) (f : Y ⟶ Y') (g : opposite.unop X ⟶ Y) :

(category_theory.coyoneda.obj X).map f g = g ≫ f

source

theorem category_theory.yoneda.obj_map_id {C : Type u₁} [category_theory.category C] {X Y : C} (f : opposite.op X ⟶ opposite.op Y) :

(category_theory.yoneda.obj X).map f (𝟙 X) = (category_theory.yoneda.map f.unop).app (opposite.op Y) (𝟙 Y)

source

@[simp]

theorem category_theory.yoneda.naturality {C : Type u₁} [category_theory.category C] {X Y : C} (α : category_theory.yoneda.obj X ⟶ category_theory.yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) :

f ≫ α.app (opposite.op Z') h = α.app (opposite.op Z) (f ≫ h)

source

@[protected, instance]

def category_theory.yoneda.yoneda_full {C : Type u₁} [category_theory.category C] :

category_theory.full category_theory.yoneda

The Yoneda embedding is full.

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

Equations

category_theory.yoneda.yoneda_full = {preimage := λ (X Y : C) (f : category_theory.yoneda.obj X ⟶ category_theory.yoneda.obj Y), f.app (opposite.op X) (𝟙 X), witness' := _}

source

@[protected, instance]

def category_theory.yoneda.yoneda_faithful {C : Type u₁} [category_theory.category C] :

category_theory.faithful category_theory.yoneda

The Yoneda embedding is faithful.

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

source

def category_theory.yoneda.ext {C : Type u₁} [category_theory.category 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 (f ≫ g) = 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

category_theory.yoneda.ext X Y p q h₁ h₂ n = category_theory.yoneda.preimage_iso (category_theory.nat_iso.of_components (λ (Z : Cᵒᵖ), {hom := p (opposite.unop Z), inv := q (opposite.unop Z), hom_inv_id' := _, inv_hom_id' := _}) _)

source

theorem category_theory.yoneda.is_iso {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso (category_theory.yoneda.map f)] :

category_theory.is_iso f

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

source

@[simp]

theorem category_theory.coyoneda.naturality {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (α : category_theory.coyoneda.obj X ⟶ category_theory.coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z) (h : opposite.unop X ⟶ Z') :

α.app Z' h ≫ f = α.app Z (h ≫ f)

source

@[protected, instance]

def category_theory.coyoneda.coyoneda_full {C : Type u₁} [category_theory.category C] :

category_theory.full category_theory.coyoneda

Equations

category_theory.coyoneda.coyoneda_full = {preimage := λ (X Y : Cᵒᵖ) (f : category_theory.coyoneda.obj X ⟶ category_theory.coyoneda.obj Y), quiver.hom.op (f.app (opposite.unop X) (𝟙 (opposite.unop X))), witness' := _}

source

@[protected, instance]

def category_theory.coyoneda.coyoneda_faithful {C : Type u₁} [category_theory.category C] :

category_theory.faithful category_theory.coyoneda

source

theorem category_theory.coyoneda.is_iso {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [category_theory.is_iso (category_theory.coyoneda.map f)] :

category_theory.is_iso f

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

source

def category_theory.coyoneda.punit_iso :

category_theory.coyoneda.obj (opposite.op punit) ≅ 𝟭 (Type v₁)

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

Equations

category_theory.coyoneda.punit_iso = category_theory.nat_iso.of_components (λ (X : Type v₁), {hom := λ (f : (category_theory.coyoneda.obj (opposite.op punit)).obj X), f punit.star, inv := λ (x : (𝟭 (Type v₁)).obj X) (_x : opposite.unop (opposite.op punit)), x, hom_inv_id' := _, inv_hom_id' := _}) category_theory.coyoneda.punit_iso._proof_3

source

@[simp]

theorem category_theory.coyoneda.obj_op_op_inv_app {C : Type u₁} [category_theory.category C] (X : C) (X_1 : Cᵒᵖ) (ᾰ : (category_theory.yoneda.obj X).obj X_1) :

(category_theory.coyoneda.obj_op_op X).inv.app X_1 ᾰ = quiver.hom.op ᾰ

source

def category_theory.coyoneda.obj_op_op {C : Type u₁} [category_theory.category C] (X : C) :

category_theory.coyoneda.obj (opposite.op (opposite.op X)) ≅ category_theory.yoneda.obj X

Taking the unop of morphisms is a natural isomorphism.

Equations

category_theory.coyoneda.obj_op_op X = category_theory.nat_iso.of_components (λ (Y : Cᵒᵖ), (category_theory.op_equiv (opposite.unop (opposite.op (opposite.op X))) Y).to_iso) _

source

@[simp]

theorem category_theory.coyoneda.obj_op_op_hom_app {C : Type u₁} [category_theory.category C] (X : C) (X_1 : Cᵒᵖ) (ᾰ : (category_theory.coyoneda.obj (opposite.op (opposite.op X))).obj X_1) :

(category_theory.coyoneda.obj_op_op X).hom.app X_1 ᾰ = quiver.hom.unop ᾰ

source

@[class]

structure category_theory.functor.representable {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) :

Prop

has_representation : ∃ (X : C) (f : category_theory.yoneda.obj X ⟶ F), category_theory.is_iso 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.

Instances of this typeclass

category_theory.functor.obj.representable

source

@[protected, instance]

def category_theory.functor.obj.representable {C : Type u₁} [category_theory.category C] {X : C} :

(category_theory.yoneda.obj X).representable

source

@[class]

structure category_theory.functor.corepresentable {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) :

Prop

has_corepresentation : ∃ (X : Cᵒᵖ) (f : category_theory.coyoneda.obj X ⟶ F), category_theory.is_iso 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.

Instances of this typeclass

source

@[protected, instance]

def category_theory.functor.obj.corepresentable {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} :

(category_theory.coyoneda.obj X).corepresentable

source

noncomputable def category_theory.functor.repr_X {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] :

C

The representing object for the representable functor F.

Equations

F.repr_X = category_theory.functor.representable.has_representation.some

source

noncomputable def category_theory.functor.repr_f {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] :

category_theory.yoneda.obj F.repr_X ⟶ F

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

Equations

F.repr_f = Exists.some _

Instances for category_theory.functor.repr_f

category_theory.functor.repr_f.category_theory.is_iso

source

noncomputable def category_theory.functor.repr_x {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] :

F.obj (opposite.op F.repr_X)

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

Equations

F.repr_x = F.repr_f.app (opposite.op F.repr_X) (𝟙 F.repr_X)

source

@[protected, instance]

def category_theory.functor.repr_f.category_theory.is_iso {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] :

category_theory.is_iso F.repr_f

source

noncomputable def category_theory.functor.repr_w {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] :

category_theory.yoneda.obj F.repr_X ≅ 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

F.repr_w = category_theory.as_iso F.repr_f

source

@[simp]

theorem category_theory.functor.repr_w_hom {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] :

F.repr_w.hom = F.repr_f

source

theorem category_theory.functor.repr_w_app_hom {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) [F.representable] (X : Cᵒᵖ) (f : opposite.unop X ⟶ F.repr_X) :

(F.repr_w.app X).hom f = F.map f.op F.repr_x

source

noncomputable def category_theory.functor.corepr_X {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) [F.corepresentable] :

C

The representing object for the corepresentable functor F.

Equations

F.corepr_X = opposite.unop category_theory.functor.corepresentable.has_corepresentation.some

source

noncomputable def category_theory.functor.corepr_f {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) [F.corepresentable] :

category_theory.coyoneda.obj (opposite.op F.corepr_X) ⟶ F

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

Equations

F.corepr_f = Exists.some _

Instances for category_theory.functor.corepr_f

category_theory.functor.corepr_f.category_theory.is_iso

source

noncomputable def category_theory.functor.corepr_x {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) [F.corepresentable] :

F.obj F.corepr_X

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

Equations

F.corepr_x = F.corepr_f.app F.corepr_X (𝟙 F.corepr_X)

source

@[protected, instance]

def category_theory.functor.corepr_f.category_theory.is_iso {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) [F.corepresentable] :

category_theory.is_iso F.corepr_f

source

noncomputable def category_theory.functor.corepr_w {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) [F.corepresentable] :

category_theory.coyoneda.obj (opposite.op F.corepr_X) ≅ 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

F.corepr_w = category_theory.as_iso F.corepr_f

source

theorem category_theory.functor.corepr_w_app_hom {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) [F.corepresentable] (X : C) (f : F.corepr_X ⟶ X) :

(F.corepr_w.app X).hom f = F.map f F.corepr_x

source

theorem category_theory.representable_of_nat_iso {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ ⥤ Type v₁) {G : Cᵒᵖ ⥤ Type v₁} (i : F ≅ G) [F.representable] :

G.representable

source

theorem category_theory.corepresentable_of_nat_iso {C : Type u₁} [category_theory.category C] (F : C ⥤ Type v₁) {G : C ⥤ Type v₁} (i : F ≅ G) [F.corepresentable] :

G.corepresentable

source

@[protected, instance]

def category_theory.functor.id.functor.corepresentable :

(𝟭 (Type v₁)).corepresentable

source

@[protected, instance]

def category_theory.prod_category_instance_1 (C : Type u₁) [category_theory.category C] :

category_theory.category ((Cᵒᵖ ⥤ Type v₁) × Cᵒᵖ)

Equations

category_theory.prod_category_instance_1 C = category_theory.prod (Cᵒᵖ ⥤ Type v₁) Cᵒᵖ

source

@[protected, instance]

def category_theory.prod_category_instance_2 (C : Type u₁) [category_theory.category C] :

category_theory.category (Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁))

Equations

category_theory.prod_category_instance_2 C = category_theory.prod Cᵒᵖ (Cᵒᵖ ⥤ Type v₁)

source

def category_theory.yoneda_evaluation (C : Type u₁) [category_theory.category C] :

Cᵒᵖ × (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

category_theory.yoneda_evaluation C = category_theory.evaluation_uncurried Cᵒᵖ (Type v₁) ⋙ category_theory.ulift_functor

source

@[simp]

theorem category_theory.yoneda_evaluation_map_down (C : Type u₁) [category_theory.category C] (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (x : (category_theory.yoneda_evaluation C).obj P) :

((category_theory.yoneda_evaluation C).map α x).down = α.snd.app Q.fst (P.snd.map α.fst x.down)

source

def category_theory.yoneda_pairing (C : Type u₁) [category_theory.category C] :

Cᵒᵖ × (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

category_theory.yoneda_pairing C = category_theory.yoneda.op.prod (𝟭 (Cᵒᵖ ⥤ Type v₁)) ⋙ category_theory.functor.hom (Cᵒᵖ ⥤ Type v₁)

source

@[simp]

theorem category_theory.yoneda_pairing_map (C : Type u₁) [category_theory.category C] (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (β : (category_theory.yoneda_pairing C).obj P) :

(category_theory.yoneda_pairing C).map α β = category_theory.yoneda.map α.fst.unop ≫ β ≫ α.snd

source

def category_theory.yoneda_lemma (C : Type u₁) [category_theory.category C] :

category_theory.yoneda_pairing C ≅ category_theory.yoneda_evaluation C

The Yoneda lemma asserts that 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

category_theory.yoneda_lemma C = {hom := {app := λ (F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (x : (category_theory.yoneda_pairing C).obj F), {down := x.app F.fst (𝟙 (opposite.unop F.fst))}, naturality' := _}, inv := {app := λ (F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (x : (category_theory.yoneda_evaluation C).obj F), {app := λ (X : Cᵒᵖ) (a : (opposite.unop ((category_theory.yoneda.op.prod (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst).obj X), F.snd.map (quiver.hom.op a) x.down, naturality' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.yoneda_sections_hom_down {C : Type u₁} [category_theory.category C] (X : C) (F : Cᵒᵖ ⥤ Type v₁) (ᾰ : (category_theory.yoneda_pairing C).obj (opposite.op X, F)) :

((category_theory.yoneda_sections X F).hom ᾰ).down = ᾰ.app (opposite.op X) (𝟙 X)

source

@[simp]

theorem category_theory.yoneda_sections_inv_app {C : Type u₁} [category_theory.category C] (X : C) (F : Cᵒᵖ ⥤ Type v₁) (ᾰ : (category_theory.yoneda_evaluation C).obj (opposite.op X, F)) (X_1 : Cᵒᵖ) (a : (opposite.unop ((category_theory.yoneda.op.prod (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj (opposite.op X, F)).fst).obj X_1) :

((category_theory.yoneda_sections X F).inv ᾰ).app X_1 a = F.map (quiver.hom.op a) ᾰ.down

source

def category_theory.yoneda_sections {C : Type u₁} [category_theory.category C] (X : C) (F : Cᵒᵖ ⥤ Type v₁) :

(category_theory.yoneda.obj X ⟶ F) ≅ ulift (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

category_theory.yoneda_sections X F = (category_theory.yoneda_lemma C).app (opposite.op X, F)

source

def category_theory.yoneda_equiv {C : Type u₁} [category_theory.category C] {X : C} {F : Cᵒᵖ ⥤ Type v₁} :

(category_theory.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

category_theory.yoneda_equiv = (category_theory.yoneda_sections X F).to_equiv.trans equiv.ulift

source

@[simp]

theorem category_theory.yoneda_equiv_apply {C : Type u₁} [category_theory.category C] {X : C} {F : Cᵒᵖ ⥤ Type v₁} (f : category_theory.yoneda.obj X ⟶ F) :

⇑category_theory.yoneda_equiv f = f.app (opposite.op X) (𝟙 X)

source

@[simp]

theorem category_theory.yoneda_equiv_symm_app_apply {C : Type u₁} [category_theory.category C] {X : C} {F : Cᵒᵖ ⥤ Type v₁} (x : F.obj (opposite.op X)) (Y : Cᵒᵖ) (f : opposite.unop Y ⟶ X) :

(⇑(category_theory.yoneda_equiv.symm) x).app Y f = F.map f.op x

source

theorem category_theory.yoneda_equiv_naturality {C : Type u₁} [category_theory.category C] {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : category_theory.yoneda.obj X ⟶ F) (g : Y ⟶ X) :

F.map g.op (⇑category_theory.yoneda_equiv f) = ⇑category_theory.yoneda_equiv (category_theory.yoneda.map g ≫ f)

source

def category_theory.yoneda_sections_small {C : Type u₁} [category_theory.small_category C] (X : C) (F : Cᵒᵖ ⥤ Type u₁) :

(category_theory.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

category_theory.yoneda_sections_small X F = category_theory.yoneda_sections X F ≪≫ category_theory.ulift_trivial (F.obj (opposite.op X))

source

@[simp]

theorem category_theory.yoneda_sections_small_hom {C : Type u₁} [category_theory.small_category C] (X : C) (F : Cᵒᵖ ⥤ Type u₁) (f : category_theory.yoneda.obj X ⟶ F) :

(category_theory.yoneda_sections_small X F).hom f = f.app (opposite.op X) (𝟙 (opposite.unop (opposite.op X)))

source

@[simp]

theorem category_theory.yoneda_sections_small_inv_app_apply {C : Type u₁} [category_theory.small_category C] (X : C) (F : Cᵒᵖ ⥤ Type u₁) (t : F.obj (opposite.op X)) (Y : Cᵒᵖ) (f : opposite.unop Y ⟶ X) :

((category_theory.yoneda_sections_small X F).inv t).app Y f = F.map f.op t

source

def category_theory.curried_yoneda_lemma {C : Type u₁} [category_theory.small_category C] :

category_theory.yoneda.op ⋙ category_theory.coyoneda ≅ category_theory.evaluation Cᵒᵖ (Type u₁)

The curried version of yoneda lemma when C is small.

Equations

category_theory.curried_yoneda_lemma = category_theory.eq_to_iso category_theory.curried_yoneda_lemma._proof_1 ≪≫ category_theory.curry.map_iso (category_theory.yoneda_lemma C ≪≫ category_theory.iso_whisker_left (category_theory.evaluation_uncurried Cᵒᵖ (Type u₁)) category_theory.ulift_functor_trivial) ≪≫ category_theory.eq_to_iso category_theory.curried_yoneda_lemma._proof_2

source

def category_theory.curried_yoneda_lemma' {C : Type u₁} [category_theory.small_category C] :

category_theory.yoneda ⋙ (category_theory.whiskering_left Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj category_theory.yoneda.op ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁)

The curried version of yoneda lemma when C is small.

Equations

category_theory.curried_yoneda_lemma' = category_theory.eq_to_iso category_theory.curried_yoneda_lemma'._proof_1 ≪≫ category_theory.curry.map_iso (category_theory.iso_whisker_left (category_theory.prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ) (category_theory.yoneda_lemma C ≪≫ category_theory.iso_whisker_left (category_theory.evaluation_uncurried Cᵒᵖ (Type u₁)) category_theory.ulift_functor_trivial)) ≪≫ category_theory.eq_to_iso category_theory.curried_yoneda_lemma'._proof_2

mathlib3 documentation

The Yoneda embedding #

References #