@[reducible, inline]

abbrev SimpleObj (M : Type u₂) [CategoryTheory.Category.{v₂, u₂} M] [CategoryTheory.Limits.HasZeroMorphisms M] : Type u₂

The subtype of simple objects of M, packaging an object together with its Simple instance.

def subquotientRelation (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Type u₂) [CategoryTheory.Category.{v₂, u₂} M] [CategoryTheory.LeftModuleCategory C M] [CategoryTheory.Limits.HasZeroMorphisms M] : SimpleObj M → SimpleObj M → Prop

The relation on simple objects of a left C-module category which holds when one is a subquotient of X ⊗ Y for some X ∈ C; this is the equivalence used to decompose an exact module category.