Full differential graded subcategories

Restricting the objects of a differential graded category to those satisfying a predicate leaves its Hom complexes, differential, identities, and composition intact. The inclusion is an enriched functor whose maps on Hom complexes are identities. This construction is useful for selecting representable, finite cell, or perfect objects while retaining their chain-level morphisms.

The ambient DG category need not have an ordinary Category instance, so Mathlib's ObjectProperty.FullSubcategory is unavailable here.

Main definitions

• TauCeti.DGFullSubcategory: objects satisfying a predicate in a DG category.
• TauCeti.DGFullSubcategory.inclusion: the enriched inclusion.

References

• B. Keller, Deriving DG categories, Section 2.

structure TauCeti.DGFullSubcategory {C : Type u} (P : C → Prop) : Type u

The full DG subcategory on objects satisfying P. Its Hom complexes are those of C.

• obj : C

  The underlying object.

• property : P self.obj

  The predicate holds on the object.

theorem TauCeti.DGFullSubcategory.ext {C : Type u} {P : C → Prop} {x y : DGFullSubcategory P} (obj : x.obj = y.obj) : x = y

theorem TauCeti.DGFullSubcategory.ext_iff {C : Type u} {P : C → Prop} {x y : DGFullSubcategory P} : x = y ↔ x.obj = y.obj

@[instance_reducible]

noncomputable instance TauCeti.DGFullSubcategory.instDGCategory (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} : DGCategory R (DGFullSubcategory P)

The full subcategory inherits its enrichment from the ambient DG category.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.DGFullSubcategory.inclusion (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) (DGFullSubcategory P) C

The inclusion of a full DG subcategory into its ambient DG category. Every map on Hom complexes is the identity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DGFullSubcategory.inclusion_obj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} (X : DGFullSubcategory P) : (inclusion R).obj X = X.obj

The enriched inclusion sends an object to its underlying object.

@[simp]

theorem TauCeti.DGFullSubcategory.inclusion_map (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} (X Y : DGFullSubcategory P) : (inclusion R).map X Y = CategoryTheory.eqToHom ⋯

The enriched inclusion acts as the identity on each Hom complex.

@[simp]

theorem TauCeti.DGFullSubcategory.dgHomComplex_eq (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} (X Y : DGFullSubcategory P) : dgHomComplex R X Y = dgHomComplex R X.obj Y.obj

The Hom complex in the full DG subcategory is the ambient Hom complex.

@[simp]

theorem TauCeti.DGFullSubcategory.dgDifferential_eq (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} {X Y : DGFullSubcategory P} (n : ℤ) (f : DGHom R n X Y) : (dgDifferential R n) f = (dgDifferential R n) f

The differential of the full DG subcategory is the ambient differential.

@[simp]

theorem TauCeti.DGFullSubcategory.dgId_eq (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} (X : DGFullSubcategory P) : dgId R X = dgId R X.obj

The identity of the full DG subcategory is the ambient identity.

@[simp]

theorem TauCeti.DGFullSubcategory.dgComp_eq (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {P : C → Prop} {X Y Z : DGFullSubcategory P} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : dgComp R f g h = dgComp R f g h

Composition in the full DG subcategory is ambient composition.