Isomorphism classes of simple objects

For a category with zero morphisms, TauCeti.SimpleClasses C is the subtype of the skeleton of C consisting of the classes represented by simple objects. Using the skeleton makes equality in this type exactly isomorphism of representatives, while retaining a chosen representative in C for constructions indexed by simple classes.

The type is invariant under equivalence of categories. This lets finiteness assumptions and sums over simple classes be transported without choosing a separate indexing family of objects. In a preadditive category with kernels, Schur's lemma makes the chosen representatives of distinct simple classes hom orthogonal.

Main declarations

• TauCeti.SimpleClasses: the type of isomorphism classes of simple objects;
• TauCeti.SimpleClasses.classOf: the class of a simple object;
• TauCeti.SimpleClasses.eq_iff_nonempty_iso: two classes are equal exactly when their representatives are isomorphic;
• TauCeti.SimpleClasses.equiv: an equivalence of categories induces an equivalence between their types of simple classes;
• TauCeti.SimpleClasses.homOrthogonal_repr: in a preadditive category with kernels, the chosen representatives of distinct simple classes are hom orthogonal (Schur's lemma).
• TauCeti.SimpleClasses.classOf_eq_of_ne_zero: simple objects related by a nonzero morphism have the same class.

@[reducible, inline]

abbrev TauCeti.SimpleClasses (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Type u₁

The isomorphism classes of simple objects of C, realized as the simple part of its skeleton.

@[reducible, inline]

noncomputable abbrev TauCeti.SimpleClasses.repr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : SimpleClasses C) : C

The chosen representative in C of a simple isomorphism class.

instance TauCeti.SimpleClasses.instSimpleRepr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : SimpleClasses C) : CategoryTheory.Simple S.repr

The chosen representative of a simple class is simple.

noncomputable def TauCeti.SimpleClasses.classOf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) [CategoryTheory.Simple X] : SimpleClasses C

The isomorphism class of a simple object.

noncomputable def TauCeti.SimpleClasses.classOfReprIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) [CategoryTheory.Simple X] : (classOf X).repr ≅ X

The chosen representative of the class of a simple object is isomorphic to that object.

@[simp]

theorem TauCeti.SimpleClasses.classOf_repr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : SimpleClasses C) : classOf S.repr = S

Taking the class of a chosen representative recovers the original simple class.

@[simp]

theorem TauCeti.SimpleClasses.eq_iff_nonempty_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S T : SimpleClasses C) : S = T ↔ Nonempty (S.repr ≅ T.repr)

Two simple classes are equal exactly when their chosen representatives are isomorphic.

theorem TauCeti.SimpleClasses.classOf_eq_iff_nonempty_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : classOf X = classOf Y ↔ Nonempty (X ≅ Y)

Two simple objects determine the same simple class exactly when they are isomorphic.

theorem TauCeti.SimpleClasses.existsUnique_nonempty_iso_repr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) [CategoryTheory.Simple X] : ∃! S : SimpleClasses C, Nonempty (X ≅ S.repr)

Every simple object is isomorphic to the representative of a unique simple class.

noncomputable def TauCeti.SimpleClasses.equiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (e : C ≌ D) : SimpleClasses C ≃ SimpleClasses D

An equivalence of categories induces an equivalence between their simple isomorphism classes.

noncomputable def TauCeti.SimpleClasses.equivApplyReprIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (e : C ≌ D) (S : SimpleClasses C) : ((equiv e) S).repr ≅ e.functor.obj S.repr

The representative of the image of a simple class under an equivalence is isomorphic to the image of its representative.

@[simp]

theorem TauCeti.SimpleClasses.equiv_apply_classOf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (e : C ≌ D) (X : C) [CategoryTheory.Simple X] : (equiv e) (classOf X) = classOf (e.functor.obj X)

The equivalence on simple classes maps the class of an object to the class of its image.

theorem TauCeti.SimpleClasses.homOrthogonal_repr {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasKernels D] : CategoryTheory.HomOrthogonal repr

Distinct isomorphism classes of simple objects have no nonzero morphisms between their representatives.

theorem TauCeti.SimpleClasses.classOf_eq_of_ne_zero {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasKernels D] {X Y : D} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] {f : X ⟶ Y} (hf : f ≠ 0) : classOf X = classOf Y

Two simple objects related by a nonzero morphism have the same class (Schur's lemma).