Documentation

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Embedding opposites of Grothendieck categories #

If C is Grothendieck abelian and F : D ⥤ Cᵒᵖ is a functor from a small category, we construct an object G : Cᵒᵖ such that preadditiveCoyonedaObj G : Cᵒᵖ ⥤ ModuleCat (End G)ᵐᵒᵖ is faithful and exact and its precomposition with F is full if F is.

source
def CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] :
Type v

Given a functor F : D ⥤ Cᵒᵖ, where C is Grothendieck abelian, this is a ring R such that Cᵒᵖ has a nice embedding into ModuleCat (EmbeddingRing F); see OppositeModuleEmbedding.embedding.

Equations
Instances For
    source
    noncomputable instance CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.instRingEmbeddingRing {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] :
    Ring (EmbeddingRing F)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable def CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] :
    Functor Cᵒᵖ (ModuleCat (EmbeddingRing F))

    This is a functor embedding F : Cᵒᵖ ⥤ ModuleCat (EmbeddingRing F). We have that embedding F is faithful and preserves finite limits and colimits. Furthermore, F ⋙ embedding F is full.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] [Nonempty D] :
      (embedding F).Faithful
      source
      instance CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] [Nonempty D] [F.Full] :
      (F.comp (embedding F)).Full
      source
      instance CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] :
      Limits.PreservesFiniteLimits (embedding F)
      source
      instance CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding {C : Type u} [Category.{v, u} C] {D : Type v} [SmallCategory D] (F : Functor D Cᵒᵖ) [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] :
      Limits.PreservesFiniteColimits (embedding F)