Theorems · Definition · category theory

CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        CategoryTheory.Functor D Cᵒᵖ →
          [inst_2 : CategoryTheory.Abelian C] → [CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Cited by

0 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelian