Ext-orthogonal subcategories of an abelian category

Let C be an abelian category and P a property of objects of C. The objects X with Extⁿ(X, Y) = 0 for every Y satisfying P form the Ext-left-orthogonal P.extLeftOrthogonal n. By the long exact Ext sequence it is closed under extensions, so it carries the exact structure inherited from the abelian structure of C.

In degree one, a projective object Q of C satisfying P is both projective and injective for this exact structure: it is projective in C, and every inflation X ↪ Y in the orthogonal has a cokernel Z with Ext¹(Z, Q) = 0, so morphisms X ⟶ Q extend along it. For P the projective objects, this is the setting of complete resolutions by projectives.

Main definitions

• CategoryTheory.ObjectProperty.extLeftOrthogonal: the objects X with Extⁿ(X, Y) = 0 for every Y satisfying P.
• CategoryTheory.ObjectProperty.extLeftOrthogonalExactStructure: its exact structure, inherited from the abelian structure of C.

Main results

• CategoryTheory.ObjectProperty.isExtensionClosed_extLeftOrthogonal: the orthogonal is closed under extensions.
• CategoryTheory.ObjectProperty.extLeftOrthogonalExactStructure_conflation_iff: its conflations are the short exact sequences of C.
• CategoryTheory.ObjectProperty.isProjective_extLeftOrthogonalExactStructure and CategoryTheory.ObjectProperty.isInjective_extLeftOrthogonalExactStructure: in degree one, a projective object of C satisfying P is projective and injective for this exact structure.

def CategoryTheory.ObjectProperty.extLeftOrthogonal {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (n : ℕ) : ObjectProperty C

The Ext-left-orthogonal of P in degree n: the objects X with Extⁿ(X, Y) = 0 for every Y satisfying P.

theorem CategoryTheory.ObjectProperty.extLeftOrthogonal_iff {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {P : ObjectProperty C} {n : ℕ} {X : C} : P.extLeftOrthogonal n X ↔ ∀ ⦃Y : C⦄, P Y → ∀ (x : Abelian.Ext X Y n), x = 0

An object lies in the Ext-left-orthogonal of P in degree n when it has no n-th extensions by objects satisfying P.

theorem CategoryTheory.ObjectProperty.extLeftOrthogonal_of_projective {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (X : C) [Projective X] (n : ℕ) : P.extLeftOrthogonal (n + 1) X

A projective object has no extensions of positive degree, so it lies in every positive Ext-left-orthogonal.

theorem CategoryTheory.ObjectProperty.isExtensionClosed_extLeftOrthogonal {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (n : ℕ) : (TauCeti.ExactStructure.abelian C).IsExtensionClosed (P.extLeftOrthogonal n)

Extension closure: the Ext-left-orthogonal of P is closed under extensions.

instance CategoryTheory.ObjectProperty.instContainsZeroExtLeftOrthogonal {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (n : ℕ) : (P.extLeftOrthogonal n).ContainsZero

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsExtLeftOrthogonal {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (n : ℕ) : (P.extLeftOrthogonal n).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderBinaryProductsExtLeftOrthogonal {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (n : ℕ) : (P.extLeftOrthogonal n).IsClosedUnderBinaryProducts

@[reducible, inline]

noncomputable abbrev CategoryTheory.ObjectProperty.extLeftOrthogonalExactStructure {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (n : ℕ) : TauCeti.ExactStructure (P.extLeftOrthogonal n).FullSubcategory

The exact structure on the Ext-left-orthogonal of P in degree n, inherited from the abelian structure of C.

theorem CategoryTheory.ObjectProperty.extLeftOrthogonalExactStructure_conflation_iff {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) {n : ℕ} (S : ShortComplex (P.extLeftOrthogonal n).FullSubcategory) : (P.extLeftOrthogonalExactStructure n).Conflation S ↔ (S.map (P.extLeftOrthogonal n).ι).ShortExact

The conflations of P.extLeftOrthogonalExactStructure n are the short exact sequences of C.

theorem CategoryTheory.ObjectProperty.isProjective_extLeftOrthogonalExactStructure {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) {n : ℕ} (Q : C) [Projective Q] (hQ : P.extLeftOrthogonal n Q) : (P.extLeftOrthogonalExactStructure n).isProjective { obj := Q, property := hQ }

A projective object of C is projective for the exact structure on an Ext-left-orthogonal, by TauCeti.ExactStructure.isProjective_fullSubcategory_of_isProjective.

theorem CategoryTheory.ObjectProperty.isInjective_extLeftOrthogonalExactStructure {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (P : ObjectProperty C) (Q : C) (hQ : P.extLeftOrthogonal 1 Q) (hPQ : P Q) : (P.extLeftOrthogonalExactStructure 1).isInjective { obj := Q, property := hQ }

An object of the degree-one Ext-left-orthogonal of P that satisfies P is injective for its exact structure: the cokernel Z of an inflation satisfies Ext¹(Z, Q) = 0, so morphisms to Q extend along the inflation.