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 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.

source
@[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.ofHom (CategoryTheory.Linear.leftComp R X f.unop)
source
@[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)
source
@[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.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
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 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
    source
    @[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)
    source
    @[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.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
    source
    @[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.ofHom (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 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
      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
      Equations
      • ⋯ = ⋯
      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
      Equations
      • ⋯ = ⋯
      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
      Equations
      • ⋯ = ⋯
      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
      Equations
      • ⋯ = ⋯
      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
      Equations
      • ⋯ = ⋯
      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
      Equations
      • ⋯ = ⋯