The Gabriel-Popescu theorem

We prove the following Gabriel-Popescu theorem: if C is a Grothendieck abelian category and G is a separator, then the functor preadditiveCoyonedaObj G : C ⥤ ModuleCat (End G)ᵐᵒᵖ sending X to Hom(G, X) is fully faithful and has an exact left adjoint.

We closely follow the elementary proof given by Barry Mitchell.

Future work

The left adjoint tensorObj G actually exists as soon as C is cocomplete and additive, so the construction could be generalized.

The theorem as stated here implies that C is a Serre quotient of ModuleCat (End R)ᵐᵒᵖ.

References

• [Barry Mitchell, A quick proof of the Gabriel-Popesco theorem][mitchell1981]

instance CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G : C} : (preadditiveCoyonedaObj G).IsRightAdjoint

noncomputable def CategoryTheory.IsGrothendieckAbelian.tensorObj {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] (G : C) : Functor (ModuleCat (End G)ᵐᵒᵖ) C

The left adjoint of the functor Hom(G, ·), which can be thought of as · ⊗ G.

Equations

• CategoryTheory.IsGrothendieckAbelian.tensorObj G = (CategoryTheory.preadditiveCoyonedaObj G).leftAdjoint

noncomputable def CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] (G : C) : tensorObj G ⊣ preadditiveCoyonedaObj G

The tensor-hom adjunction (· ⊗ G) ⊣ Hom(G, ·).

Equations

• CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction G = CategoryTheory.Adjunction.ofIsRightAdjoint (CategoryTheory.preadditiveCoyonedaObj G)

instance CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G : C} : (tensorObj G).IsLeftAdjoint

noncomputable def CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : (∐ fun (x : ↑M) => G) ⟶ A

This is the map ⨁ₘ G ⟶ A induced by M ⟶ Hom(G, A).

Equations

• CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g = CategoryTheory.Limits.Sigma.desc fun (m : ↑M) => (CategoryTheory.ConcreteCategory.hom g) m

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) (m : ↑M) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ↑M) => G) m) (d g) = (ModuleCat.Hom.hom g) m

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) (m : ↑M) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ↑M) => G) m) (CategoryStruct.comp (d g) h) = CategoryStruct.comp ((ModuleCat.Hom.hom g) m) h

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G : C} (hG : IsSeparator G) {A B : C} {M : ModuleCat (End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) (hg : Mono g) (f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : CategoryStruct.comp (Limits.kernel.ι (d g)) (d f) = 0

This is the "Lemma" in [mitchell1981].

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] {G : C} (hG : IsSeparator G) {A : C} (B : C) [Injective B] {M : ModuleCat (End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) (hg : Mono g) (f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : ∃ (l : A ⟶ B), CategoryStruct.comp (d g) l = d f

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] (G : C) (hG : IsSeparator G) : (preadditiveCoyonedaObj G).Full

Faithfulness follows because G is a separator, see isSeparator_iff_faithful_preadditiveCoyonedaObj.

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] (G : C) (hG : IsSeparator G) : (preadditiveCoyonedaObj G).PreservesInjectiveObjects

theorem CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{v, v, u} C] (G : C) (hG : IsSeparator G) : Limits.PreservesFiniteLimits (tensorObj G)

Right exactness follows because tensorObj G is a left adjoint.