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.

source

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.

Equations

P.rightOrthogonal Y = ∀ ⦃X : C⦄ (f : X ⟶ Y), P X → f = 0

Instances For

source

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

source

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.

Equations