Documentation

Mathlib.CategoryTheory.ObjectProperty.Orthogonal

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
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
    Instances For
      source
      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
      source
      theorem CategoryTheory.ObjectProperty.gc_rightOrthogonal_leftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
      GaloisConnection (⇑OrderDual.toDual ∘ rightOrthogonal) (leftOrthogonal ∘ ⇑OrderDual.ofDual)

      The pair (rightOrthogonal, leftOrthogonal) forms a Galois connection between ObjectProperty C and its opposite order.

      source
      theorem CategoryTheory.ObjectProperty.le_leftOrthogonal_iff_le_rightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P Q : ObjectProperty C) :
      P ≤ Q.leftOrthogonal ↔ Q ≤ P.rightOrthogonal
      source
      theorem CategoryTheory.ObjectProperty.le_leftOrthogonal_rightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P ≤ P.rightOrthogonal.leftOrthogonal
      source
      theorem CategoryTheory.ObjectProperty.le_rightOrthogonal_leftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P ≤ P.leftOrthogonal.rightOrthogonal
      source
      theorem CategoryTheory.ObjectProperty.antitone_rightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
      Antitone rightOrthogonal
      source
      theorem CategoryTheory.ObjectProperty.antitone_leftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
      Antitone leftOrthogonal
      source
      @[simp]
      theorem CategoryTheory.ObjectProperty.leftOrthogonal_rightOrthogonal_leftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P.leftOrthogonal.rightOrthogonal.leftOrthogonal = P.leftOrthogonal
      source
      @[simp]
      theorem CategoryTheory.ObjectProperty.rightOrthogonal_leftOrthogonal_rightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P.rightOrthogonal.leftOrthogonal.rightOrthogonal = P.rightOrthogonal
      source
      theorem CategoryTheory.ObjectProperty.rightOrthogonal_op {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P.op.rightOrthogonal = P.leftOrthogonal.op
      source
      theorem CategoryTheory.ObjectProperty.leftOrthogonal_op {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P.op.leftOrthogonal = P.rightOrthogonal.op
      source
      theorem CategoryTheory.ObjectProperty.rightOrthogonal_unop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (R : ObjectProperty Cᵒᵖ) :
      R.unop.rightOrthogonal = R.leftOrthogonal.unop
      source
      theorem CategoryTheory.ObjectProperty.leftOrthogonal_unop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (R : ObjectProperty Cᵒᵖ) :
      R.unop.leftOrthogonal = R.rightOrthogonal.unop
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsRightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P.rightOrthogonal.IsClosedUnderIsomorphisms
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) :
      P.leftOrthogonal.IsClosedUnderIsomorphisms
      source
      instance CategoryTheory.ObjectProperty.instContainsZeroRightOrthogonalOfHasZeroObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [Limits.HasZeroObject C] :
      P.rightOrthogonal.ContainsZero
      source
      instance CategoryTheory.ObjectProperty.instContainsZeroLeftOrthogonalOfHasZeroObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [Limits.HasZeroObject C] :
      P.leftOrthogonal.ContainsZero