Full dg subcategories

dg-enhancements-e8, part one. Given a dg category C and a predicate P on its objects, the objects satisfying P form a dg category whose Hom-complexes are the ambient ones, unchanged.

Why this is a root rather than a one-off

The derived dg enhancement is the full dg subcategory of C^dg A on the K-injective complexes, and its dual is the one on the K-projective complexes. Neither is a new dg category: both are C^dg A with its objects cut down, and writing either one directly would duplicate five axiom proofs that have nothing to do with resolutions. HomotopyCategory/DGEnhancement/KInjective.lean and HomotopyCategory/DGEnhancement/KProjective.lean are the two consumers, and they supply only the predicate.

The construction is definitional, and that is the point

dgHom X Y is dgHom X.obj Y.obj by definition, not up to an isomorphism that later files would have to transport along. So is dgId, and so is dgComp. Every field of DGCategory is therefore the ambient field applied, and every axiom is the ambient axiom applied -- there is no sign, no re-association, and no AddMonoidHom to rebuild. Contrast Product.lean, where the Hom-complex is a genuinely new complex and the file is four times this length.

Two consequences worth stating, because later files rely on both:

• the inclusion iota has AddMonoidHom.id for its action on Hom-complexes, so it is faithful and full in every degree on the nose (iota_map_apply, which is deliberately not @[simp] -- see its docstring);
• DGLinear transfers with no new module structure, because the graded pieces are literally the same abelian groups (homModule, linear, and iota_map_smul as the test).

Why there are no @[simp] lemmas for the identifications

The obvious candidates -- dgHom X Y = dgHom X.obj Y.obj and its siblings -- have the same head symbol on both sides and differ only in the DGCategoryStruct instance. simp's discrimination tree does not separate those reliably, so tagging them invites a loop for no gain: every one of them is rfl, and a goal that needs one is discharged by rfl, exact, or show. The lemmas are stated anyway, named, so that a reader can see the identification and cite it.

def CategoryTheory.DGFullSubcategory {C : Type u} (P : C → Prop) : Type u

The objects of a dg category satisfying a predicate P.

A def on Subtype P rather than an abbreviation, so that the DGCategory instance below attaches here and not to Subtype generally.

Equations

• CategoryTheory.DGFullSubcategory P = { X : C // P X }

The objects

These five need no dg structure at all, so they are stated before C acquires one. Keeping them outside the [DGCategory C] scope is not cosmetic: the unusedSectionVars linter runs library-wide in CI and fails on an automatically included instance a declaration does not use.

def CategoryTheory.DGFullSubcategory.obj {C : Type u} {P : C → Prop} (X : DGFullSubcategory P) : C

The underlying ambient object.

Equations

• X.obj = ↑X

theorem CategoryTheory.DGFullSubcategory.prop {C : Type u} {P : C → Prop} (X : DGFullSubcategory P) : P X.obj

The underlying object satisfies the defining predicate.

def CategoryTheory.DGFullSubcategory.mk {C : Type u} {P : C → Prop} (X : C) (hX : P X) : DGFullSubcategory P

An ambient object satisfying P, as an object of the full dg subcategory.

Equations

• CategoryTheory.DGFullSubcategory.mk X hX = ⟨X, hX⟩

@[simp]

theorem CategoryTheory.DGFullSubcategory.obj_mk {C : Type u} {P : C → Prop} (X : C) (hX : P X) : (mk X hX).obj = X

mk and obj are inverse on objects.

theorem CategoryTheory.DGFullSubcategory.ext {C : Type u} {P : C → Prop} {X Y : DGFullSubcategory P} (h : X.obj = Y.obj) : X = Y

Two objects of the full dg subcategory agree as soon as their ambient objects do; P is a Prop, so there is nothing else to check.

theorem CategoryTheory.DGFullSubcategory.ext_iff {C : Type u} {P : C → Prop} {X Y : DGFullSubcategory P} : X = Y ↔ X.obj = Y.obj

@[implicit_reducible]

instance CategoryTheory.DGFullSubcategory.struct {C : Type u} {P : C → Prop} [DGCategory C] : DGCategoryStruct (DGFullSubcategory P)

The Hom-complexes, identity and composition are the ambient ones.

Equations

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

The identifications

All three are rfl. See the module docstring on why none is @[simp].

theorem CategoryTheory.DGFullSubcategory.dgHom_eq {C : Type u} {P : C → Prop} [DGCategory C] (X Y : DGFullSubcategory P) : DGCategoryStruct.dgHom X Y = DGCategoryStruct.dgHom X.obj Y.obj

The Hom-complex is the ambient one.

theorem CategoryTheory.DGFullSubcategory.dgId_eq {C : Type u} {P : C → Prop} [DGCategory C] (X : DGFullSubcategory P) : DGCategoryStruct.dgId X = DGCategoryStruct.dgId X.obj

The identity is the ambient one.

theorem CategoryTheory.DGFullSubcategory.dgComp_eq {C : Type u} {P : C → Prop} [DGCategory C] {X Y Z : DGFullSubcategory P} (p q r : ℤ) (h : p + q = r) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (g : ↑((DGCategoryStruct.dgHom Y Z).X q)) : ((DGCategoryStruct.dgComp p q r h) f) g = ((DGCategoryStruct.dgComp p q r h) f) g

Graded composition is the ambient one.

@[implicit_reducible]

instance CategoryTheory.DGFullSubcategory.dgCategory {C : Type u} {P : C → Prop} [DGCategory C] : DGCategory (DGFullSubcategory P)

The full dg subcategory is a dg category. Every axiom is the ambient axiom applied to the ambient objects; nothing is reproved.

Equations

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

The identity and composition tests

The two laws that would be wrong if the instance above had transported anything rather than reusing it. Both are rfl, and that they are rfl is the claim.

theorem CategoryTheory.DGFullSubcategory.dgId_comp_eq {C : Type u} {P : C → Prop} [DGCategory C] {X Y : DGFullSubcategory P} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((DGCategoryStruct.dgComp 0 p p ⋯) (DGCategoryStruct.dgId X)) f = f

The identity test. dgId is a left unit for dgComp, by the ambient unit law rather than a transported one.

theorem CategoryTheory.DGFullSubcategory.dgComp_id_eq {C : Type u} {P : C → Prop} [DGCategory C] {X Y : DGFullSubcategory P} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((DGCategoryStruct.dgComp p 0 p ⋯) f) (DGCategoryStruct.dgId Y) = f

The composition test. dgId is a right unit for dgComp, likewise.

The inclusion

def CategoryTheory.DGFullSubcategory.iota {C : Type u} [DGCategory C] (P : C → Prop) : DGFunctor (DGFullSubcategory P) C

The inclusion of a full dg subcategory into its ambient dg category. Its action on Hom-complexes is the identity.

Equations

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

@[simp]

theorem CategoryTheory.DGFullSubcategory.iota_obj {C : Type u} {P : C → Prop} [DGCategory C] (X : DGFullSubcategory P) : (iota P).obj X = X.obj

The inclusion sends an object to its ambient object.

theorem CategoryTheory.DGFullSubcategory.iota_map_apply {C : Type u} {P : C → Prop} [DGCategory C] {X Y : DGFullSubcategory P} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((iota P).map p) f = f

The inclusion acts as the identity on every graded piece of every Hom-complex. This is the precise form of "full and faithful" available here: DGFunctor has no fullness or faithfulness class, and for this functor the statement is stronger than either would be.

Not @[simp], and the reason is iota_obj above. That lemma rewrites (iota P).obj X to X.obj -- including inside the type of this one's left-hand side, which mentions dgHom ((iota P).obj X) ((iota P).obj Y). The left-hand side is therefore never in simp-normal form and simpNF rejects the attribute. Keep the attribute on the obj lemma, drop it on the map one, and name this lemma explicitly in the simp only sets that need it.

Linearity

No module structure is introduced. The graded pieces of the Hom-complexes are the ambient ones, so the ambient Module k instances are the instances, and each DGLinear axiom is the ambient axiom applied.

@[implicit_reducible]

instance CategoryTheory.DGFullSubcategory.homModule {C : Type u} {P : C → Prop} [DGCategory C] (k : Type w) [CommRing k] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] (X Y : DGFullSubcategory P) (p : ℤ) : Module k ↑((DGCategoryStruct.dgHom X Y).X p)

The ambient module structure, seen through the subtype.

Equations

• CategoryTheory.DGFullSubcategory.homModule k X Y p = inst✝ X.obj Y.obj p

The scalar-compatibility test, and why it is not a lemma.

The statement one reaches for first -- that the subcategory's action on (dgHom X Y).X p is the ambient action on (dgHom X.obj Y.obj).X p -- cannot be written down usefully. Both sides elaborate to the same term, so the simpNF linter rejects it with "LHS equals RHS syntactically", and it is right to: a lemma that is rfl with no change of spelling records nothing.

That there is nothing to record is the claim. A transported module structure would need such a lemma; this one does not, because it is the ambient structure. What does carry content is that the inclusion preserves scalars, and that is iota_linear below with iota_map_smul reading it back.

instance CategoryTheory.DGFullSubcategory.linear {C : Type u} {P : C → Prop} [DGCategory C] (k : Type w) [CommRing k] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] : DGLinear k (DGFullSubcategory P)

A full dg subcategory of a k-linear dg category is k-linear.

Each field names the ambient dg category explicitly with (C := C). Without it, Lean reads the dg category off the type of f, which is the subcategory, and then tries to synthesize the very instance being defined.

instance CategoryTheory.DGFullSubcategory.iota_linear {C : Type u} {P : C → Prop} [DGCategory C] (k : Type w) [CommRing k] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] : DGFunctor.Linear k (iota P)

The inclusion is k-linear.

theorem CategoryTheory.DGFullSubcategory.iota_map_smul {C : Type u} {P : C → Prop} [DGCategory C] (k : Type w) [CommRing k] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {X Y : DGFullSubcategory P} (p : ℤ) (c : k) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((iota P).map p) (c • f) = c • ((iota P).map p) f

The scalar-compatibility test. The inclusion preserves scalar multiplication in every degree. Unlike the identity that the section comment above declines to state, this one is not rfl on the nose: the two sides differ by where the identity AddMonoidHom sits.