The Yoneda embedding for `R`-linear categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The Yoneda embedding for R-linear categories C, sends an object X : C to the Module R-valued presheaf on C, with value on Y : Cᵒᵖ given by Module.of R (unop Y ⟶ X).

TODO: linear_yoneda R C is R-linear. TODO: In fact, linear_yoneda itself is additive and R-linear.

source

def category_theory.linear_yoneda (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

C ⥤ Cᵒᵖ ⥤ Module R

The Yoneda embedding for R-linear categories C, sending an object X : C to the Module R-valued presheaf on C, with value on Y : Cᵒᵖ given by Module.of R (unop Y ⟶ X).

Equations

category_theory.linear_yoneda R C = {obj := λ (X : C), {obj := λ (Y : Cᵒᵖ), Module.of R (opposite.unop Y ⟶ X), map := λ (Y Y' : Cᵒᵖ) (f : Y ⟶ Y'), category_theory.linear.left_comp R X f.unop, map_id' := _, map_comp' := _}, map := λ (X X' : C) (f : X ⟶ X'), {app := λ (Y : Cᵒᵖ), category_theory.linear.right_comp R (opposite.unop Y) f, naturality' := _}, map_id' := _, map_comp' := _}

Instances for category_theory.linear_yoneda

source

@[simp]

theorem category_theory.linear_yoneda_map_app (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (X X' : C) (f : X ⟶ X') (Y : Cᵒᵖ) :

((category_theory.linear_yoneda R C).map f).app Y = category_theory.linear.right_comp R (opposite.unop Y) f

source

@[simp]

theorem category_theory.linear_yoneda_obj_obj (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (X : C) (Y : Cᵒᵖ) :

((category_theory.linear_yoneda R C).obj X).obj Y = Module.of R (opposite.unop Y ⟶ X)

source

@[simp]

theorem category_theory.linear_yoneda_obj_map (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (X : C) (Y Y' : Cᵒᵖ) (f : Y ⟶ Y') :

((category_theory.linear_yoneda R C).obj X).map f = category_theory.linear.left_comp R X f.unop

source

@[simp]

theorem category_theory.linear_coyoneda_map_app (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (Y Y' : Cᵒᵖ) (f : Y ⟶ Y') (X : C) :

((category_theory.linear_coyoneda R C).map f).app X = category_theory.linear.left_comp R X f.unop

source

@[simp]

theorem category_theory.linear_coyoneda_obj_map (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (Y : Cᵒᵖ) (Y_1 Y' : C) (g : Y_1 ⟶ Y') :

((category_theory.linear_coyoneda R C).obj Y).map g = category_theory.linear.right_comp R (opposite.unop Y) g

source

def category_theory.linear_coyoneda (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

Cᵒᵖ ⥤ C ⥤ Module R

The Yoneda embedding for R-linear categories C, sending an object Y : Cᵒᵖ to the Module R-valued copresheaf on C, with value on X : C given by Module.of R (unop Y ⟶ X).

Equations

category_theory.linear_coyoneda R C = {obj := λ (Y : Cᵒᵖ), {obj := λ (X : C), Module.of R (opposite.unop Y ⟶ X), map := λ (Y_1 Y' : C), category_theory.linear.right_comp R (opposite.unop Y), map_id' := _, map_comp' := _}, map := λ (Y Y' : Cᵒᵖ) (f : Y ⟶ Y'), {app := λ (X : C), category_theory.linear.left_comp R X f.unop, naturality' := _}, map_id' := _, map_comp' := _}

Instances for category_theory.linear_coyoneda

source

@[simp]

theorem category_theory.linear_coyoneda_obj_obj (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (Y : Cᵒᵖ) (X : C) :

((category_theory.linear_coyoneda R C).obj Y).obj X = Module.of R (opposite.unop Y ⟶ X)

source

@[protected, instance]

def category_theory.linear_yoneda_obj_additive (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (X : C) :

((category_theory.linear_yoneda R C).obj X).additive

source

@[protected, instance]

def category_theory.linear_coyoneda_obj_additive (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (Y : Cᵒᵖ) :

((category_theory.linear_coyoneda R C).obj Y).additive

source

@[simp]

theorem category_theory.whiskering_linear_yoneda (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.linear_yoneda R C ⋙ (category_theory.whiskering_right Cᵒᵖ (Module R) (Type v)).obj (category_theory.forget (Module R)) = category_theory.yoneda

source

@[simp]

theorem category_theory.whiskering_linear_yoneda₂ (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.linear_yoneda R C ⋙ (category_theory.whiskering_right Cᵒᵖ (Module R) AddCommGroup).obj (category_theory.forget₂ (Module R) AddCommGroup) = category_theory.preadditive_yoneda

source

@[simp]

theorem category_theory.whiskering_linear_coyoneda (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.linear_coyoneda R C ⋙ (category_theory.whiskering_right C (Module R) (Type v)).obj (category_theory.forget (Module R)) = category_theory.coyoneda

source

@[simp]

theorem category_theory.whiskering_linear_coyoneda₂ (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.linear_coyoneda R C ⋙ (category_theory.whiskering_right C (Module R) AddCommGroup).obj (category_theory.forget₂ (Module R) AddCommGroup) = category_theory.preadditive_coyoneda

source

@[protected, instance]

def category_theory.linear_yoneda_full (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.full (category_theory.linear_yoneda R C)

Equations

category_theory.linear_yoneda_full R C = let yoneda_full : category_theory.full (category_theory.linear_yoneda R C ⋙ (category_theory.whiskering_right Cᵒᵖ (Module R) (Type v)).obj (category_theory.forget (Module R))) := category_theory.yoneda.yoneda_full in category_theory.full.of_comp_faithful (category_theory.linear_yoneda R C) ((category_theory.whiskering_right Cᵒᵖ (Module R) (Type v)).obj (category_theory.forget (Module R)))

source

@[protected, instance]

def category_theory.linear_coyoneda_full (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.full (category_theory.linear_coyoneda R C)

Equations

category_theory.linear_coyoneda_full R C = let coyoneda_full : category_theory.full (category_theory.linear_coyoneda R C ⋙ (category_theory.whiskering_right C (Module R) (Type v)).obj (category_theory.forget (Module R))) := category_theory.coyoneda.coyoneda_full in category_theory.full.of_comp_faithful (category_theory.linear_coyoneda R C) ((category_theory.whiskering_right C (Module R) (Type v)).obj (category_theory.forget (Module R)))

source

@[protected, instance]

def category_theory.linear_yoneda_faithful (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.faithful (category_theory.linear_yoneda R C)

source

@[protected, instance]

def category_theory.linear_coyoneda_faithful (R : Type w) [ring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :

category_theory.faithful (category_theory.linear_coyoneda R C)

The Yoneda embedding for R-linear categories #

The Yoneda embedding for `R`-linear categories #