mathlib docs: category

@[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' := _}

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' := _}

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

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

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

def 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

Equations

category_theory.yoneda.is_iso f = category_theory.is_iso_of_fully_faithful category_theory.yoneda 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

@[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), category_theory.has_hom.hom.op (f.app (opposite.unop X) (𝟙 (opposite.unop X))), witness' := _}

source

@[instance]

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

category_theory.faithful category_theory.coyoneda

source

def 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

Equations

category_theory.coyoneda.is_iso f = category_theory.is_iso_of_fully_faithful category_theory.coyoneda f

source

@[class]

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

Type (max u₁ v₁)

X : C
w : category_theory.yoneda.obj (category_theory.representable.X F) ≅ F

A presheaf F is representable if there is object X so F ≅ yoneda.obj X.

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

source

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

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

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

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 (category_theory.has_hom.hom.op a) x.down, naturality' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

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

Equations

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

source

@[simp]

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)

Equations

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

mathlib documentation

The Yoneda embedding

References