def IsSubquotientOf {C : Type u} [CategoryTheory.Category.{v, u} C] (Y Z : C) : Prop

Y is a subquotient of Z when there is some object A mapping monomorphically into Z and epimorphically onto Y.

class IsSurjectiveTensorFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) : Prop

A functor is a surjective tensor functor when every object of the target is a subquotient of some F.obj X.

• surjective (Y : D) : ∃ (X : C), IsSubquotientOf Y (F.obj X)