The ind-embedding preserves simplicity

For a small abelian category C the embedding RS.indOf : C ⥤ Ind C carries simple objects to simple objects, and hence the unit of Ind C is simple as soon as the unit of C is.

The proof is short because the pin already supplies every input.

• the embedded objects form a separating family in Ind C (CategoryTheory.Ind.isSeparating_range_yoneda), the consequence of "every ind-object is a filtered colimit of embedded objects" that the argument actually needs;
• RS.indOf is fully faithful, and it preserves and reflects vanishing of morphisms (RS.indOf_map_eq_zero_iff);
• RS.indOf preserves finite colimits, hence epimorphisms;
• Ind C is abelian (CategoryTheory.Ind is abelian for C abelian and small), hence balanced.

Given a nonzero monomorphism m : U ⟶ indOf.obj X, separation produces an object W of C and a map g : indOf.obj W ⟶ U with g ≫ m ≠ 0. Full faithfulness writes g ≫ m = indOf.map f for a unique nonzero f : W ⟶ X, simplicity of X makes f an epimorphism, and preservation of epimorphisms makes g ≫ m — and therefore m — an epimorphism. A monomorphism that is also an epimorphism in an abelian category is an isomorphism.

Main results

• RS.simple_indOf — the embedding preserves simplicity;
• RS.simple_unit_ind — the unit of Ind C is simple when the unit of C is;
• RS.mono_unit_ind — a nonzero algebra unit in Ind C is a monomorphism.

theorem RS.simple_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.Simple X] : CategoryTheory.Simple (indOf.obj X)

The ind-embedding preserves simplicity. If X is a simple object of a small abelian category C, then indOf.obj X is a simple object of Ind C.

theorem RS.simple_unit_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (hsimple : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C))

The unit of Ind C is simple whenever the unit of C is: the unit of Ind C is the embedded unit (RS.indOfUnitIso), and the embedding preserves simplicity.

theorem RS.mono_unit_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (hsimple : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (hne : CategoryTheory.MonObj.one ≠ 0) : CategoryTheory.Mono CategoryTheory.MonObj.one

A nonzero algebra unit in Ind C is a monomorphism. This is the faithful-flatness input to faithfulness of Deligne's fibre functor: the unit of Ind C is simple, so any nonzero morphism out of it is a monomorphism.