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