The Yoneda embedding for R-linear categories #

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: linearYoneda R C is R-linear. TODO: In fact, linearYoneda itself is additive and R-linear.

@[simp]
theorem CategoryTheory.linearYoneda_obj_map (R : Type w) [Ring R] (C : Type u) [] (X : C) :
∀ {X_1 Y : Cᵒᵖ} (f : X_1 Y), (.obj X).map f = ModuleCat.ofHom (CategoryTheory.Linear.leftComp R X f.unop)
@[simp]
theorem CategoryTheory.linearYoneda_obj_obj (R : Type w) [Ring R] (C : Type u) [] (X : C) (Y : Cᵒᵖ) :
(.obj X).obj Y = ModuleCat.of R (Y.unop X)
@[simp]
theorem CategoryTheory.linearYoneda_map_app (R : Type w) [Ring R] (C : Type u) [] {X₁ : C} {X₂ : C} (f : X₁ X₂) (Y : Cᵒᵖ) :
def CategoryTheory.linearYoneda (R : Type w) [Ring R] (C : Type u) [] :

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.linearCoyoneda_obj_obj (R : Type w) [Ring R] (C : Type u) [] (Y : Cᵒᵖ) (X : C) :
(.obj Y).obj X = ModuleCat.of R (Y.unop X)
@[simp]
theorem CategoryTheory.linearCoyoneda_obj_map (R : Type w) [Ring R] (C : Type u) [] (Y : Cᵒᵖ) :
∀ {X Y_1 : C} (f : X Y_1), (.obj Y).map f = ModuleCat.ofHom (CategoryTheory.Linear.rightComp R Y.unop f)
@[simp]
theorem CategoryTheory.linearCoyoneda_map_app (R : Type w) [Ring R] (C : Type u) [] {Y₁ : Cᵒᵖ} {Y₂ : Cᵒᵖ} (f : Y₁ Y₂) (X : C) :
def CategoryTheory.linearCoyoneda (R : Type w) [Ring R] (C : Type u) [] :

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
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.linearYoneda_obj_additive (R : Type w) [Ring R] (C : Type u) [] (X : C) :
Equations
• =
instance CategoryTheory.linearCoyoneda_obj_additive (R : Type w) [Ring R] (C : Type u) [] (Y : Cᵒᵖ) :
Equations
• =
@[simp]
theorem CategoryTheory.whiskering_linearYoneda (R : Type w) [Ring R] (C : Type u) [] :
.comp (().obj ) = CategoryTheory.yoneda
@[simp]
theorem CategoryTheory.whiskering_linearYoneda₂ (R : Type w) [Ring R] (C : Type u) [] :
@[simp]
theorem CategoryTheory.whiskering_linearCoyoneda (R : Type w) [Ring R] (C : Type u) [] :
.comp (().obj ) = CategoryTheory.coyoneda
@[simp]
theorem CategoryTheory.whiskering_linearCoyoneda₂ (R : Type w) [Ring R] (C : Type u) [] :
instance CategoryTheory.full_linearYoneda (R : Type w) [Ring R] (C : Type u) [] :
.Full
Equations
• =
instance CategoryTheory.full_linearCoyoneda (R : Type w) [Ring R] (C : Type u) [] :
.Full
Equations
• =
instance CategoryTheory.faithful_linearYoneda (R : Type w) [Ring R] (C : Type u) [] :
.Faithful
Equations
• =
instance CategoryTheory.faithful_linearCoyoneda (R : Type w) [Ring R] (C : Type u) [] :
.Faithful
Equations
• =