Orthogonal of a property of objects

Let P be a property of objects in a category with zero morphisms. We define P.rightOrthogonal as the property of objects Y such that any map f : X ⟶ Y vanishes when P X holds. Similarly, we define P.leftOrthogonal as the property of objects X such that any map f : X ⟶ Y vanishes when P Y holds.

def CategoryTheory.ObjectProperty.rightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : ObjectProperty C

In a category with zero morphisms, the right orthogonal of a property of objects P is the property of objects Y such that any map X ⟶ Y vanishes when P X holds.

theorem CategoryTheory.ObjectProperty.rightOrthogonal_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (Y : C) : P.rightOrthogonal Y ↔ ∀ ⦃X : C⦄ (f : X ⟶ Y), P X → f = 0

def CategoryTheory.ObjectProperty.leftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : ObjectProperty C

In a category with zero morphisms, the left orthogonal of a property of objects P is the property of objects X such that any map X ⟶ Y vanishes when P Y holds.

theorem CategoryTheory.ObjectProperty.leftOrthogonal_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (X : C) : P.leftOrthogonal X ↔ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P Y → f = 0

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.rightOrthogonal.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.leftOrthogonal.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instContainsZeroRightOrthogonalOfHasZeroObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [Limits.HasZeroObject C] : P.rightOrthogonal.ContainsZero

instance CategoryTheory.ObjectProperty.instContainsZeroLeftOrthogonalOfHasZeroObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [Limits.HasZeroObject C] : P.leftOrthogonal.ContainsZero