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) [Category.{v, u} C] [Preadditive C] [Linear R C] :
Functor C (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) [Category.{v, u} C] [Preadditive C] [Linear R C] (X : C) (Y : Cᵒᵖ) :
    ↑(((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) [Category.{v, u} C] [Preadditive C] [Linear R C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : Cᵒᵖ) :
    (((linearYoneda R C).map f).app Y).hom = Linear.rightComp R (Opposite.unop Y) f
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_obj_isModule (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (X : C) (Y : Cᵒᵖ) :
    (((linearYoneda R C).obj X).obj Y).isModule = Linear.homModule (Opposite.unop Y) X
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_obj_isAddCommGroup (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (X : C) (Y : Cᵒᵖ) :
    (((linearYoneda R C).obj X).obj Y).isAddCommGroup = Preadditive.homGroup (Opposite.unop Y) X
    source
    @[simp]
    theorem CategoryTheory.linearYoneda_obj_map_hom (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :
    (((linearYoneda R C).obj X).map f).hom = Linear.leftComp R X f.unop
    source
    def CategoryTheory.linearCoyoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
    Functor Cᵒᵖ (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) [Category.{v, u} C] [Preadditive C] [Linear R C] (Y : Cᵒᵖ) (X : C) :
      (((linearCoyoneda R C).obj Y).obj X).isModule = Linear.homModule (Opposite.unop Y) X
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_obj_carrier (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (Y : Cᵒᵖ) (X : C) :
      ↑(((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) [Category.{v, u} C] [Preadditive C] [Linear R C] {Y₁ Y₂ : Cᵒᵖ} (f : Y₁ ⟶ Y₂) (X : C) :
      (((linearCoyoneda R C).map f).app X).hom = Linear.leftComp R X f.unop
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_map_hom (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (Y : Cᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
      (((linearCoyoneda R C).obj Y).map f).hom = Linear.rightComp R (Opposite.unop Y) f
      source
      @[simp]
      theorem CategoryTheory.linearCoyoneda_obj_obj_isAddCommGroup (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (Y : Cᵒᵖ) (X : C) :
      (((linearCoyoneda R C).obj Y).obj X).isAddCommGroup = Preadditive.homGroup (Opposite.unop Y) X
      source
      instance CategoryTheory.linearYoneda_obj_additive (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (X : C) :
      ((linearYoneda R C).obj X).Additive
      source
      instance CategoryTheory.linearCoyoneda_obj_additive (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (Y : Cᵒᵖ) :
      ((linearCoyoneda R C).obj Y).Additive
      source
      @[simp]
      theorem CategoryTheory.whiskering_linearYoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearYoneda R C).comp ((whiskeringRight Cᵒᵖ (ModuleCat R) (Type v)).obj (forget (ModuleCat R))) = yoneda
      source
      @[simp]
      theorem CategoryTheory.whiskering_linearYoneda₂ (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearYoneda R C).comp ((whiskeringRight Cᵒᵖ (ModuleCat R) AddCommGrp).obj (forget₂ (ModuleCat R) AddCommGrp)) = preadditiveYoneda
      source
      @[simp]
      theorem CategoryTheory.whiskering_linearCoyoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearCoyoneda R C).comp ((whiskeringRight C (ModuleCat R) (Type v)).obj (forget (ModuleCat R))) = coyoneda
      source
      @[simp]
      theorem CategoryTheory.whiskering_linearCoyoneda₂ (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearCoyoneda R C).comp ((whiskeringRight C (ModuleCat R) AddCommGrp).obj (forget₂ (ModuleCat R) AddCommGrp)) = preadditiveCoyoneda
      source
      instance CategoryTheory.full_linearYoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearYoneda R C).Full
      source
      instance CategoryTheory.full_linearCoyoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearCoyoneda R C).Full
      source
      instance CategoryTheory.faithful_linearYoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearYoneda R C).Faithful
      source
      instance CategoryTheory.faithful_linearCoyoneda (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] :
      (linearCoyoneda R C).Faithful