Documentation

TauCeti.CategoryTheory.Exact.ExtensionClosed

The exact structure induced on an extension-closed full subcategory #

Let E be a Quillen exact structure on an additive category C and let P : ObjectProperty C be closed under extensions: whenever X ⟶ Y ⟶ Z is an E-conflation with P X and P Z, also P Y. If moreover P holds for a zero object and is closed under binary products — the explicit form of "the full subcategory is additive" — then P.FullSubcategory carries an exact structure whose conflations are the conflations of E all of whose terms lie in P, and the inclusion functor both preserves and reflects conflations.

This is the third of the three fundamental constructions of exact structures, after the split structure on an additive category and the canonical structure on an abelian category. It is what lets a subcategory such as the finitely generated projective modules, or the modules admitting a finite projective resolution, be treated as an exact category in its own right.

Main definitions #

Main results #

References #

source
instance TauCeti.instHasBinaryBiproductsFullSubcategoryOfIsClosedUnderBinaryProducts_tauCeti {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderBinaryProducts] :
CategoryTheory.Limits.HasBinaryBiproducts P.FullSubcategory

A full subcategory of an additive category closed under binary products has binary biproducts: in a preadditive category binary products already are biproducts.

source
structure TauCeti.ExactStructure.IsExtensionClosed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) :
Prop

An object property is extension closed for an exact structure E when the middle term of every E-conflation whose outer terms satisfy the property satisfies the property.

For the canonical exact structure of an abelian category this is Mathlib's CategoryTheory.ObjectProperty.IsClosedUnderExtensions; see TauCeti.ExactStructure.isExtensionClosed_abelian_iff.

Instances For
    source
    theorem TauCeti.ExactStructure.IsExtensionClosed.prop_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} (hP : E.IsExtensionClosed P) {X Y : C} (hX : P X) (hY : P Y) :
    P (X ⊞ Y)

    An extension-closed property is closed under binary biproducts, because the biproduct short complex is a conflation of every exact structure.

    source
    theorem TauCeti.ExactStructure.IsExtensionClosed.isClosedUnderBinaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} (hP : E.IsExtensionClosed P) [P.IsClosedUnderIsomorphisms] :
    P.IsClosedUnderBinaryProducts

    A replete extension-closed property is closed under binary products. Together with CategoryTheory.ObjectProperty.ContainsZero this is exactly the additivity of the full subcategory, so no separate closure hypothesis on biproducts is needed.

    source
    theorem TauCeti.ExactStructure.IsExtensionClosed.isClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} (hP : E.IsExtensionClosed P) [P.ContainsZero] :
    P.IsClosedUnderIsomorphisms

    An extension-closed property holding for some zero object is closed under isomorphisms: an isomorphism X ≅ Y followed by the zero map to a zero object is a split conflation.

    source
    theorem TauCeti.ExactStructure.isExtensionClosed_split_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
    (split C).IsExtensionClosed P ↔ ∀ (X Y : C), P X → P Y → P (X ⊞ Y)

    For the split exact structure, extension closure is exactly closure under binary biproducts. This is the hypothesis under which a subcategory such as the finitely generated projective modules inherits the split structure.

    source
    theorem TauCeti.ExactStructure.isExtensionClosed_abelian_iff {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (P : CategoryTheory.ObjectProperty A) :
    (abelian A).IsExtensionClosed P ↔ P.IsClosedUnderExtensions

    For the canonical exact structure of an abelian category, extension closure agrees with Mathlib's CategoryTheory.ObjectProperty.IsClosedUnderExtensions.

    source
    noncomputable def TauCeti.ExactStructure.fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) :
    ExactStructure P.FullSubcategory

    The exact structure induced on an extension-closed full subcategory. Its conflations are the conflations of E all of whose terms lie in P.

    The subcategory is required to be additive in the explicit form of containing a zero object and being closed under binary products; by TauCeti.ExactStructure.IsExtensionClosed.isClosedUnderBinaryProducts the second condition is automatic for a replete extension-closed P.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.ExactStructure.fullSubcategory_conflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (S : CategoryTheory.ShortComplex P.FullSubcategory) :
      (fullSubcategory P hP).Conflation S ↔ E.Conflation (S.map P.ι)

      A short complex of the subcategory is a conflation of the induced exact structure exactly when its image in the ambient category is a conflation.

      source
      theorem TauCeti.ExactStructure.isConflationExact_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) :
      (fullSubcategory P hP).IsConflationExact E P.ι

      The inclusion of an extension-closed full subcategory is conflation-exact.

      source
      theorem TauCeti.ExactStructure.isConflationExact_ιOfLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {Q : CategoryTheory.ObjectProperty C} [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : E.IsExtensionClosed Q) (h : P ≤ Q) :
      (fullSubcategory P hP).IsConflationExact (fullSubcategory Q hQ) (CategoryTheory.ObjectProperty.ιOfLE h)

      The inclusion associated to an implication between two extension-closed object properties is conflation-exact for their induced exact structures.

      source
      theorem TauCeti.ExactStructure.isConflationExact_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {Q : CategoryTheory.ObjectProperty D} [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : E'.IsExtensionClosed Q) (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) (hPQ : ∀ (X : P.FullSubcategory), Q (F.obj X.obj)) :
      (fullSubcategory P hP).IsConflationExact (fullSubcategory Q hQ) (Q.lift (P.ι.comp F) hPQ)

      A conflation-exact functor carrying one extension-closed property into another restricts to a conflation-exact functor between their induced exact structures.

      source
      theorem TauCeti.ExactStructure.isConflationExact_congrFullSubcategory_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {Q : CategoryTheory.ObjectProperty D} [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] [Q.IsClosedUnderIsomorphisms] (hQ : E'.IsExtensionClosed Q) (e : C ≌ D) [e.functor.Additive] (hF : E.IsConflationExact E' e.functor) (h : Q.inverseImage e.functor = P) :
      (fullSubcategory P hP).IsConflationExact (fullSubcategory Q hQ) (e.congrFullSubcategory h).functor

      The forward functor of an exact equivalence restricts to a conflation-exact functor between corresponding extension-closed full subcategories.

      source
      theorem TauCeti.ExactStructure.isConflationExact_congrFullSubcategory_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {Q : CategoryTheory.ObjectProperty D} [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] [Q.IsClosedUnderIsomorphisms] (hQ : E'.IsExtensionClosed Q) (e : C ≌ D) [e.inverse.Additive] (hG : E'.IsConflationExact E e.inverse) (h : Q.inverseImage e.functor = P) :
      (fullSubcategory Q hQ).IsConflationExact (fullSubcategory P hP) (e.congrFullSubcategory h).inverse

      The inverse functor of an exact equivalence restricts to a conflation-exact functor between corresponding extension-closed full subcategories.

      source
      theorem TauCeti.ExactStructure.reflectsConflations_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) :
      (fullSubcategory P hP).ReflectsConflations E P.ι

      The inclusion of an extension-closed full subcategory reflects conflations: a short complex of the subcategory whose image is a conflation of E is a conflation of the induced structure.