The Yoneda embedding for R-linear categories #
The Yoneda embedding for R-linear categories C,
sends an object X : C to the ModuleCat R-valued presheaf on C,
with value on Y : Cᵒᵖ given by ModuleCat.of R (unop Y ⟶ X).
TODO: linearYoneda R C is R-linear.
TODO: In fact, linearYoneda itself is additive and R-linear.
def
CategoryTheory.linearYoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
The Yoneda embedding for R-linear categories C,
sending an object X : C to the ModuleCat R-valued presheaf on C,
with value on Y : Cᵒᵖ given by ModuleCat.of R (unop Y ⟶ X).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.linearYoneda_obj_obj
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
(X : C)
(Y : Cᵒᵖ)
:
((CategoryTheory.linearYoneda R C).obj X).obj Y = ModuleCat.of R (Opposite.unop Y ⟶ X)
@[simp]
theorem
CategoryTheory.linearYoneda_obj_map
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
(X : C)
:
∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
((CategoryTheory.linearYoneda R C).obj X).map f = ModuleCat.asHom (CategoryTheory.Linear.leftComp R X f.unop)
@[simp]
theorem
CategoryTheory.linearYoneda_map_app
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{X₁ : C}
{X₂ : C}
(f : X₁ ⟶ X₂)
(Y : Cᵒᵖ)
:
((CategoryTheory.linearYoneda R C).map f).app Y = ModuleCat.asHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
def
CategoryTheory.linearCoyoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
The Yoneda embedding for R-linear categories C,
sending an object Y : Cᵒᵖ to the ModuleCat R-valued copresheaf on C,
with value on X : C given by ModuleCat.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)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
(Y : Cᵒᵖ)
(X : C)
:
((CategoryTheory.linearCoyoneda R C).obj Y).obj X = ModuleCat.of R (Opposite.unop Y ⟶ X)
@[simp]
theorem
CategoryTheory.linearCoyoneda_obj_map
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
(Y : Cᵒᵖ)
:
∀ {X Y_1 : C} (f : X ⟶ Y_1),
((CategoryTheory.linearCoyoneda R C).obj Y).map f = ModuleCat.asHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
@[simp]
theorem
CategoryTheory.linearCoyoneda_map_app
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{Y₁ : Cᵒᵖ}
{Y₂ : Cᵒᵖ}
(f : Y₁ ⟶ Y₂)
(X : C)
:
((CategoryTheory.linearCoyoneda R C).map f).app X = ModuleCat.asHom (CategoryTheory.Linear.leftComp R X f.unop)
instance
CategoryTheory.linearYoneda_obj_additive
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
(X : C)
:
((CategoryTheory.linearYoneda R C).obj X).Additive
Equations
- ⋯ = ⋯
instance
CategoryTheory.linearCoyoneda_obj_additive
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
(Y : Cᵒᵖ)
:
((CategoryTheory.linearCoyoneda R C).obj Y).Additive
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.whiskering_linearYoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearYoneda R C).comp
((CategoryTheory.whiskeringRight Cᵒᵖ (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) = CategoryTheory.yoneda
@[simp]
theorem
CategoryTheory.whiskering_linearYoneda₂
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearYoneda R C).comp
((CategoryTheory.whiskeringRight Cᵒᵖ (ModuleCat R) AddCommGrp).obj
(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)) = CategoryTheory.preadditiveYoneda
@[simp]
theorem
CategoryTheory.whiskering_linearCoyoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearCoyoneda R C).comp
((CategoryTheory.whiskeringRight C (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) = CategoryTheory.coyoneda
@[simp]
theorem
CategoryTheory.whiskering_linearCoyoneda₂
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearCoyoneda R C).comp
((CategoryTheory.whiskeringRight C (ModuleCat R) AddCommGrp).obj
(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)) = CategoryTheory.preadditiveCoyoneda
instance
CategoryTheory.full_linearYoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearYoneda R C).Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.full_linearCoyoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearCoyoneda R C).Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.faithful_linearYoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearYoneda R C).Faithful
Equations
- ⋯ = ⋯
instance
CategoryTheory.faithful_linearCoyoneda
(R : Type w)
[Ring R]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
:
(CategoryTheory.linearCoyoneda R C).Faithful
Equations
- ⋯ = ⋯