Subcomplexes from degreewise subobject data

Neither Mathlib nor this repository has a way to build a subcomplex of a HomologicalComplex from a degreewise family of subobjects. Mathlib goes the other way — a mono of complexes is degreewise mono (HomologicalComplexLimits.lean) — and has the degreewise exactness criteria, but nothing assembles degreewise data into a complex.

This file supplies that. The point worth stating is how little is needed: given objects with monomorphisms into the ambient complex and differentials that commute with its own, both HomologicalComplex laws are automatic. shape and d_comp_d' are each proved by cancelling the mono in the next degree, so a caller supplies no coherence beyond the commuting squares.

Main definitions

• SubcomplexData: objects, monos into K, and differentials commuting with K's.
• SubcomplexData.toComplex: the resulting complex.
• SubcomplexData.toComplexι: its inclusion into K, a monomorphism of complexes.

Why this exists

Stacks 13.17.4 (tag 0FCL) — D⁻(𝓑) → D⁻_𝓑(𝓐) is an equivalence for a Serre subcategory 𝓑 ⊆ 𝓐 with the lifting property — is proved by a dévissage that constructs, by descending induction, subobjects E^i ⊂ X^i lying in 𝓑 and assembles them into a subcomplex quasi-isomorphic to the original. This is the assembly step of that argument, isolated because it is independent of 𝓑, of the Serre condition, and of the induction that produces the E^i.

Implementation notes

The data is unbundled from Subobject: a family X with monos, rather than a family of Subobject (K.X i). The subobject-valued form needs the restriction condition as an inequality (Subobject.«exists» (K.d i j)).obj (S i) ≤ S j and then has to extract the differential from it; that is a further step, and this is the primitive it would be built on.

structure HomologicalComplex.SubcomplexData {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) : Type (max (max u u_1) v)

Degreewise subobject data for a complex K: an object in each degree, a monomorphism into K in each degree, and differentials commuting with those of K.

• X : ι → V

  The object in degree i.

• ι (i : ι) : self.X i ⟶ K.X i

  The monomorphism into K in degree i.

• mono (i : ι) : CategoryTheory.Mono (self.ι i)

  Each inclusion is a monomorphism; this is what makes the complex laws automatic.

• d (i j : ι) : self.X i ⟶ self.X j

  The restricted differential.

• comm (i j : ι) : CategoryTheory.CategoryStruct.comp (self.d i j) (self.ι j) = CategoryTheory.CategoryStruct.comp (self.ι i) (K.d i j)

  The differentials commute with the inclusions.

def HomologicalComplex.SubcomplexData.toComplex {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {K : HomologicalComplex V c} (S : K.SubcomplexData) : HomologicalComplex V c

The subcomplex determined by degreewise subobject data.

Neither complex law is a hypothesis: shape holds because d i j ≫ ι j factors through K.d i j = 0, and d_comp_d' because it factors through K.d i j ≫ K.d j k = 0. Both then follow by cancelling the monomorphism in the target degree.

Equations

• S.toComplex = { X := S.X, d := S.d, shape := ⋯, d_comp_d' := ⋯ }

@[simp]

theorem HomologicalComplex.SubcomplexData.toComplex_X {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {K : HomologicalComplex V c} (S : K.SubcomplexData) (a✝ : ι) : S.toComplex.X a✝ = S.X a✝

@[simp]

theorem HomologicalComplex.SubcomplexData.toComplex_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {K : HomologicalComplex V c} (S : K.SubcomplexData) (i j : ι) : S.toComplex.d i j = S.d i j

def HomologicalComplex.SubcomplexData.toComplexι {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {K : HomologicalComplex V c} (S : K.SubcomplexData) : S.toComplex ⟶ K

The inclusion of the subcomplex into K.

Equations

• S.toComplexι = { f := S.ι, comm' := ⋯ }

@[simp]

theorem HomologicalComplex.SubcomplexData.toComplexι_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {K : HomologicalComplex V c} (S : K.SubcomplexData) (i : ι) : S.toComplexι.f i = S.ι i

instance HomologicalComplex.SubcomplexData.instMonoToComplexι {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {K : HomologicalComplex V c} (S : K.SubcomplexData) : CategoryTheory.Mono S.toComplexι

The inclusion is a monomorphism of complexes, being one in each degree.

def HomologicalComplex.SubcomplexData.top {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) : K.SubcomplexData

K as a subcomplex of itself.

Equations

• HomologicalComplex.SubcomplexData.top K = { X := K.X, ι := fun (x : ι) => CategoryTheory.CategoryStruct.id (K.X x), mono := ⋯, d := K.d, comm := ⋯ }

@[simp]

theorem HomologicalComplex.SubcomplexData.top_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) (i j : ι) : (top K).d i j = K.d i j

@[simp]

theorem HomologicalComplex.SubcomplexData.top_X {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) (a✝ : ι) : (top K).X a✝ = K.X a✝

@[simp]

theorem HomologicalComplex.SubcomplexData.top_ι {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) (x✝ : ι) : (top K).ι x✝ = CategoryTheory.CategoryStruct.id (K.X x✝)

def HomologicalComplex.SubcomplexData.ofDegreewiseMono {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) {L : HomologicalComplex V c} (φ : L ⟶ K) [∀ (i : ι), CategoryTheory.Mono (φ.f i)] : K.SubcomplexData

A degreewise monomorphism of complexes is subcomplex data.

Stated with [∀ i, Mono (φ.f i)] rather than [Mono φ]: the two agree when the ambient category has finite limits (HomologicalComplex.mono_of_mono_f and its converse), but the degreewise form is what the construction uses and it needs no hypothesis on V.

Equations

• HomologicalComplex.SubcomplexData.ofDegreewiseMono K φ = { X := L.X, ι := φ.f, mono := ⋯, d := L.d, comm := ⋯ }

@[simp]

theorem HomologicalComplex.SubcomplexData.ofDegreewiseMono_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) {L : HomologicalComplex V c} (φ : L ⟶ K) [∀ (i : ι), CategoryTheory.Mono (φ.f i)] (i j : ι) : (ofDegreewiseMono K φ).d i j = L.d i j

@[simp]

theorem HomologicalComplex.SubcomplexData.ofDegreewiseMono_ι {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) {L : HomologicalComplex V c} (φ : L ⟶ K) [∀ (i : ι), CategoryTheory.Mono (φ.f i)] (i : ι) : (ofDegreewiseMono K φ).ι i = φ.f i

@[simp]

theorem HomologicalComplex.SubcomplexData.ofDegreewiseMono_X {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (K : HomologicalComplex V c) {L : HomologicalComplex V c} (φ : L ⟶ K) [∀ (i : ι), CategoryTheory.Mono (φ.f i)] (a✝ : ι) : (ofDegreewiseMono K φ).X a✝ = L.X a✝