Documentation

Mathlib.CategoryTheory.Linear.Yoneda

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.

source
def CategoryTheory.linearYoneda (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] :
CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (ModuleCat R))

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
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_obj_carrier (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) = (Opposite.unop Y ⟶ X)
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_map_app_hom (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : Cᵒᵖ) :
    (((CategoryTheory.linearYoneda R C).map f).app Y).hom = CategoryTheory.Linear.rightComp R (Opposite.unop Y) f
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_obj_isModule (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).isModule = CategoryTheory.Linear.homModule (Opposite.unop Y) X
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_obj_isAddCommGroup (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).isAddCommGroup = CategoryTheory.Preadditive.homGroup (Opposite.unop Y) X
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_map_hom (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :
    (((CategoryTheory.linearYoneda R C).obj X).map f).hom = CategoryTheory.Linear.leftComp R X f.unop
    source
    def CategoryTheory.linearCoyoneda (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] :
    CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (ModuleCat R))

    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
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_obj_isModule (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).isModule = CategoryTheory.Linear.homModule (Opposite.unop Y) X
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_obj_carrier (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) = (Opposite.unop Y ⟶ X)
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_map_app_hom (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {Y₁ Y₂ : Cᵒᵖ} (f : Y₁ ⟶ Y₂) (X : C) :
      (((CategoryTheory.linearCoyoneda R C).map f).app X).hom = CategoryTheory.Linear.leftComp R X f.unop
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_map_hom (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (Y : Cᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
      (((CategoryTheory.linearCoyoneda R C).obj Y).map f).hom = CategoryTheory.Linear.rightComp R (Opposite.unop Y) f
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_obj_isAddCommGroup (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).isAddCommGroup = CategoryTheory.Preadditive.homGroup (Opposite.unop Y) X
      source
      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
      source
      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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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
      source
      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
      source
      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
      source
      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