Theorems · Definition · category theory

CategoryTheory.HomOrthogonal

{C : Type u} → [CategoryTheory.Category.{v, u} C] → {ι : Type u_1} → (ι → C) → Prop

A family of objects is "hom orthogonal" if there is at most one morphism between distinct objects. (In a category with zero morphisms, that must be the zero morphism.)

Defined in

Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Cited by

11 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Category