The Milnor sequence of a tower of complexes of modules

A tower of complexes is a functor C : ℕᵒᵖ ⥤ HomologicalComplex (ModuleCat R) c, a sequence of complexes C₀ ← C₁ ← C₂ ← ⋯ of R-modules of an arbitrary shape c. In each degree i its terms form a tower of modules C.term i, and the differentials form morphisms of towers. Applying ModuleTower.lim degreewise gives the limit complex C.limComplex, which with its projections is a limit of C (ComplexTower.isLimitLimComplexCone), and applying ModuleTower.Product gives the product complex C.productComplex. The shift maps δ(x)ₙ = xₙ - φₙ(xₙ₊₁) form a chain map of the product complex whose kernel is the limit complex. When the shift is surjective in every degree, equivalently lim¹ of every tower of terms vanishes (for instance when every transition map Cₙ₊₁ → Cₙ is surjective, ModuleTower.shift_surjective, or every tower of terms is Mittag-Leffler, ModuleTower.shift_surjective_of_isMittagLeffler),

0 → lim C → ∏ₙ Cₙ → ∏ₙ Cₙ → 0

is a short exact sequence of complexes (ComplexTower.shortComplex_shortExact). Products of modules are exact, so the homology of the product complex is the product of the homologies (ComplexTower.productHomologyEquiv), and the shift acts on it as the shift of the tower of homology modules C.homology i. For a tower whose shift is surjective in every degree, the long exact homology sequence then splits into the Milnor sequences: for every pair of degrees i, j with c.Rel i j,

0 → lim¹ Hᵢ(Cₙ) → Hⱼ(lim C) → lim Hⱼ(Cₙ) → 0

is exact (ComplexTower.limOneToHomology_injective, ComplexTower.exact_limOneToHomology_homologyToLim, ComplexTower.homologyToLim_surjective). The map Hⱼ(lim C) → lim Hⱼ(Cₙ) is induced by the projections lim C → Cₙ, and the map lim¹ Hᵢ(Cₙ) → Hⱼ(lim C) is induced by the connecting map of the short exact sequence above.

For cochain complexes indexed by ℤ and i = k - 1, j = k, this is the cochain sequence 0 → lim¹ H^(k-1)(Cₙ) → H^k(lim C) → lim H^k(Cₙ) → 0; for chain complexes indexed by ℕ and i = j + 1, it is the chain sequence 0 → lim¹ H_(j+1)(Cₙ) → H_j(lim C) → lim H_j(Cₙ) → 0. When, in addition to the degreewise surjectivity of the shift, lim¹ Hᵢ(Cₙ) vanishes, for instance when the tower of homology modules is Mittag-Leffler (ModuleTower.subsingleton_limOne_of_isMittagLeffler), the map Hⱼ(lim C) → lim Hⱼ(Cₙ) is therefore bijective (ComplexTower.homologyToLim_bijective). If no differential reaches degree j, the map Hⱼ(lim C) → lim Hⱼ(Cₙ) is injective with no lim¹ hypothesis (ComplexTower.homologyToLim_injective_of_forall_not_rel).

Consequently, if a cone over a tower whose shift is surjective in every degree has legs that, in each degree, induce isomorphisms on homology for all sufficiently large n, then the induced map into the limit complex is a quasi-isomorphism (ComplexTower.quasiIso_isLimitLimComplexCone_lift): the towers of homology modules have eventually surjective transitions, so the lim¹ terms of the Milnor sequences vanish.

Main declarations

• TauCeti.ComplexTower: towers of complexes of R-modules of shape c.
• TauCeti.ComplexTower.limComplex, TauCeti.ComplexTower.isLimitLimComplexCone: the limit complex, a limit of the tower.
• TauCeti.ComplexTower.productComplex, TauCeti.ComplexTower.productComplexShift: the product complex and the shift chain map.
• TauCeti.ComplexTower.shortComplex_shortExact: 0 → lim C → ∏ₙ Cₙ → ∏ₙ Cₙ → 0 is short exact for towers whose shift is surjective in every degree.
• TauCeti.ComplexTower.productHomologyEquiv: the homology of the product complex is the product of the homologies, compatibly with the shifts.
• TauCeti.ComplexTower.homologyToLim, TauCeti.ComplexTower.limOneToHomology: the two maps of the Milnor sequence.
• TauCeti.ComplexTower.limOneToHomology_injective, TauCeti.ComplexTower.exact_limOneToHomology_homologyToLim, TauCeti.ComplexTower.homologyToLim_surjective: exactness of the Milnor sequence for towers whose shift is surjective in every degree.
• TauCeti.ComplexTower.homologyToLim_bijective: Hⱼ(lim C) ≅ lim Hⱼ(Cₙ) when, in addition, lim¹ Hᵢ(Cₙ) vanishes.
• TauCeti.ComplexTower.quasiIso_isLimitLimComplexCone_lift: a cone whose legs are eventually isomorphisms on homology in each degree induces a quasi-isomorphism into the limit complex.

References

• J. Milnor, On axiomatic homology theory, Pacific J. Math. 12 (1962), 337–341.
• C. A. Weibel, An introduction to homological algebra, Theorem 3.5.8.
• Stacks: More on Algebra, Lemma 15.88.10, Tag 07KY

@[reducible, inline]

abbrev TauCeti.ComplexTower (R : Type u) [Ring R] {ι : Type w} (c : ComplexShape ι) : Type (max (max v w) (max w (v + 1) u) v)

A tower of complexes of R-modules of shape c: a functor ℕᵒᵖ ⥤ HomologicalComplex, given by complexes Cₙ and chain maps Cₙ₊₁ → Cₙ.

@[reducible, inline]

abbrev TauCeti.ComplexTower.term {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : ModuleTower R

The tower of degree-i terms of a tower of complexes.

@[reducible, inline]

noncomputable abbrev TauCeti.ComplexTower.homology {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : ModuleTower R

The tower of degree-i homology modules of a tower of complexes.

def TauCeti.ComplexTower.dTower {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i j : ι) : C.term i ⟶ C.term j

The differentials Cₙ^i → Cₙ^j of a tower of complexes, as a morphism of towers.

@[simp]

theorem TauCeti.ComplexTower.dTower_app {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i j : ι) (n : ℕᵒᵖ) : (C.dTower i j).app n = (C.obj n).d i j

The component of dTower i j at level n is the differential d i j of the n-th complex.

theorem TauCeti.ComplexTower.dTower_comp_dTower {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i j k : ι) : CategoryTheory.CategoryStruct.comp (C.dTower i j) (C.dTower j k) = 0

Consecutive differentials of a tower of complexes compose to zero.

theorem TauCeti.ComplexTower.dTower_eq_zero {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) {i j : ι} (h : ¬c.Rel i j) : C.dTower i j = 0

The differential between degrees not related by the complex shape vanishes.

theorem TauCeti.ComplexTower.homology_transition {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) (n : ℕ) : (C.homology i).transition n = ModuleCat.Hom.hom (HomologicalComplex.homologyMap (C.map (CategoryTheory.homOfLE ⋯).op) i)

The transition maps of the tower of homology modules are the maps induced on homology by the transition chain maps of the tower.

def TauCeti.ComplexTower.limComplex {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : HomologicalComplex (ModuleCat R) c

The limit complex of a tower of complexes: in degree i, the limit of the tower of degree-i terms, with the differential induced by the differentials of the tower.

@[simp]

theorem TauCeti.ComplexTower.limComplex_X {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : C.limComplex.X i = ↧↥(C.term i).lim

The degree-i term of the limit complex is the limit of the degree-i terms.

@[simp]

theorem TauCeti.ComplexTower.limComplex_d_hom {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i j : ι) : ModuleCat.Hom.hom (C.limComplex.d i j) = ModuleTower.limMap (C.dTower i j)

The differential of the limit complex is the map induced on limits by the differentials of the tower.

def TauCeti.ComplexTower.productComplex {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : HomologicalComplex (ModuleCat R) c

The product complex of a tower of complexes: in degree i, the product of the degree-i terms, with the product of the differentials.

@[simp]

theorem TauCeti.ComplexTower.productComplex_X {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : C.productComplex.X i = ↧(C.term i).Product

The degree-i term of the product complex is the product of the degree-i terms.

@[simp]

theorem TauCeti.ComplexTower.productComplex_d_hom {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i j : ι) : ModuleCat.Hom.hom (C.productComplex.d i j) = ModuleTower.productMap (C.dTower i j)

The differential of the product complex is the map induced on products by the differentials of the tower.

def TauCeti.ComplexTower.limComplexι {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : C.limComplex ⟶ C.productComplex

The inclusion of the limit complex into the product complex.

@[simp]

theorem TauCeti.ComplexTower.limComplexι_f_hom {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : ModuleCat.Hom.hom (C.limComplexι.f i) = (C.term i).lim.subtype

The degree-i component of the inclusion of the limit complex into the product complex is the subtype inclusion of the limit.

def TauCeti.ComplexTower.productComplexShift {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : C.productComplex ⟶ C.productComplex

The shift maps δ(x)ₙ = xₙ - φₙ(xₙ₊₁) of the towers of terms, as a chain map of the product complex.

@[simp]

theorem TauCeti.ComplexTower.productComplexShift_f_hom {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : ModuleCat.Hom.hom (C.productComplexShift.f i) = (C.term i).shift

The degree-i component of the shift map on the product complex is the shift map on the degree-i product.

def TauCeti.ComplexTower.productComplexπ {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) : C.productComplex ⟶ C.obj (Opposite.op n)

The projection of the product complex onto the complex Cₙ.

@[simp]

theorem TauCeti.ComplexTower.productComplexπ_f_hom {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) (i : ι) : ModuleCat.Hom.hom ((C.productComplexπ n).f i) = LinearMap.proj n

The degree-i component of the n-th projection of the product complex is the coordinate projection LinearMap.proj n.

def TauCeti.ComplexTower.limComplexπ {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) : C.limComplex ⟶ C.obj (Opposite.op n)

The projection of the limit complex onto the complex Cₙ.

@[simp]

theorem TauCeti.ComplexTower.limComplexπ_f_hom {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) (i : ι) : ModuleCat.Hom.hom ((C.limComplexπ n).f i) = (C.term i).limπ n

The degree-i component of the n-th projection of the limit complex is the projection limπ n of the degree-i limit.

@[simp]

theorem TauCeti.ComplexTower.limComplexι_comp_productComplexπ {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) : CategoryTheory.CategoryStruct.comp C.limComplexι (C.productComplexπ n) = C.limComplexπ n

The inclusion of the limit complex into the product complex followed by the n-th projection is the n-th projection of the limit complex.

@[simp]

theorem TauCeti.ComplexTower.limComplexι_comp_productComplexπ_assoc {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) {Z : HomologicalComplex (ModuleCat R) c} (h : C.obj (Opposite.op n) ⟶ Z) : CategoryTheory.CategoryStruct.comp C.limComplexι (CategoryTheory.CategoryStruct.comp (C.productComplexπ n) h) = CategoryTheory.CategoryStruct.comp (C.limComplexπ n) h

The inclusion of the limit complex into the product complex followed by the n-th projection is the n-th projection of the limit complex.

theorem TauCeti.ComplexTower.productComplexShift_comp_productComplexπ {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) : CategoryTheory.CategoryStruct.comp C.productComplexShift (C.productComplexπ n) = C.productComplexπ n - CategoryTheory.CategoryStruct.comp (C.productComplexπ (n + 1)) (C.map (CategoryTheory.homOfLE ⋯).op)

The shift followed by the projection to Cₙ is the difference of the projections to Cₙ and to Cₙ₊₁, the latter followed by the transition Cₙ₊₁ → Cₙ.

@[simp]

theorem TauCeti.ComplexTower.limComplexπ_comp_map {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) {n k : ℕ} (f : Opposite.op k ⟶ Opposite.op n) : CategoryTheory.CategoryStruct.comp (C.limComplexπ k) (C.map f) = C.limComplexπ n

The projections of the limit complex are compatible with the maps of the tower.

@[simp]

theorem TauCeti.ComplexTower.limComplexπ_comp_map_assoc {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) {n k : ℕ} (f : Opposite.op k ⟶ Opposite.op n) {Z : HomologicalComplex (ModuleCat R) c} (h : C.obj (Opposite.op n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.limComplexπ k) (CategoryTheory.CategoryStruct.comp (C.map f) h) = CategoryTheory.CategoryStruct.comp (C.limComplexπ n) h

The projections of the limit complex are compatible with the maps of the tower.

def TauCeti.ComplexTower.limComplexCone {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : CategoryTheory.Limits.Cone C

The limit complex, with its projections onto the complexes Cₙ, as a cone over the tower.

@[simp]

theorem TauCeti.ComplexTower.limComplexCone_pt {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : C.limComplexCone.pt = C.limComplex

The cone point of the limit cone is the limit complex.

@[simp]

theorem TauCeti.ComplexTower.limComplexCone_π_app {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (n : ℕ) : C.limComplexCone.π.app (Opposite.op n) = C.limComplexπ n

The component of the limit cone at level n is the n-th projection of the limit complex.

def TauCeti.ComplexTower.isLimitLimComplexCone {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : CategoryTheory.Limits.IsLimit C.limComplexCone

The limit complex, with its projections, is a limit of the tower of complexes.

def TauCeti.ComplexTower.shortComplex {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : CategoryTheory.ShortComplex (HomologicalComplex (ModuleCat R) c)

The sequence of complexes lim C → ∏ₙ Cₙ → ∏ₙ Cₙ formed by the inclusion and the shift.

@[simp]

theorem TauCeti.ComplexTower.shortComplex_f {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : C.shortComplex.f = C.limComplexι

The first map of the Milnor short complex is the inclusion of the limit complex.

@[simp]

theorem TauCeti.ComplexTower.shortComplex_g {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : C.shortComplex.g = C.productComplexShift

The second map of the Milnor short complex is the shift map of the product complex.

theorem TauCeti.ComplexTower.shortComplex_shortExact {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) : C.shortComplex.ShortExact

The product-complex short exact sequence. If the shift of a tower of complexes is surjective in every degree, for instance if every transition map is surjective in every degree, then 0 → lim C → ∏ₙ Cₙ → ∏ₙ Cₙ → 0, formed by the inclusion and the shift, is a short exact sequence of complexes.

def TauCeti.ComplexTower.isLimitProductComplexFan {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk C.productComplex C.productComplexπ)

The product complex, with its projections, is a product of the complexes Cₙ.

noncomputable def TauCeti.ComplexTower.productHomologyEquiv {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) : ↑(C.productComplex.homology i) ≃ₗ[R] (C.homology i).Product

Homology of the product complex. The degree-i homology of the product complex is the product of the degree-i homology modules of the complexes Cₙ, through the maps induced by the projections; see productHomologyEquiv_apply.

@[simp]

theorem TauCeti.ComplexTower.productHomologyEquiv_apply {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) (x : ↑(C.productComplex.homology i)) (n : ℕ) : (C.productHomologyEquiv i) x n = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (C.productComplexπ n) i)) x

The degree-i homology of the product complex maps to the product of the homologies, componentwise by the maps induced by the projections.

theorem TauCeti.ComplexTower.productHomologyEquiv_homologyMap_productComplexShift {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) (x : ↑(C.productComplex.homology i)) : (C.productHomologyEquiv i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap C.productComplexShift i)) x) = (C.homology i).shift ((C.productHomologyEquiv i) x)

On homology, the projections of the product complex intertwine the shift chain map with the shift of the tower of homology modules.

theorem TauCeti.ComplexTower.productHomologyEquiv_homologyMap_limComplexι {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (i : ι) (x : ↑(C.limComplex.homology i)) (n : ℕ) : (C.productHomologyEquiv i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap C.limComplexι i)) x) n = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (C.limComplexπ n) i)) x

On homology, the projections of the product complex restrict to those of the limit complex.

noncomputable def TauCeti.ComplexTower.homologyToLim {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (j : ι) : ↑(C.limComplex.homology j) →ₗ[R] ↥(C.homology j).lim

The map Hⱼ(lim C) → lim Hⱼ(Cₙ) of the Milnor sequence, induced by the projections of the limit complex onto the complexes Cₙ.

@[simp]

theorem TauCeti.ComplexTower.coe_homologyToLim_apply {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (j : ι) (x : ↑(C.limComplex.homology j)) (n : ℕ) : ↑((C.homologyToLim j) x) n = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (C.limComplexπ n) j)) x

The n-th component of the image of a class in the homology of the limit complex is the class induced by the n-th projection.

theorem TauCeti.ComplexTower.coe_homologyToLim {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) (j : ι) (x : ↑(C.limComplex.homology j)) : ↑((C.homologyToLim j) x) = (C.productHomologyEquiv j) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap C.limComplexι j)) x)

The map Hⱼ(lim C) → lim Hⱼ(Cₙ) is the map induced by the inclusion into the product complex, read in the product of the homologies.

theorem TauCeti.ComplexTower.homologyToLim_injective_of_forall_not_rel {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} (C : ComplexTower R c) {j : ι} (hj : ∀ (i : ι), ¬c.Rel i j) : Function.Injective ⇑(C.homologyToLim j)

If no differential reaches degree j, then Hⱼ(lim C) → lim Hⱼ(Cₙ) is injective: homology in degree j is the module of cycles, and the cycles of the limit complex embed in the limit of the cycles.

noncomputable def TauCeti.ComplexTower.limOneToHomology {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) {i j : ι} (hij : c.Rel i j) : (C.homology i).limOne →ₗ[R] ↑(C.limComplex.homology j)

The map lim¹ Hᵢ(Cₙ) → Hⱼ(lim C) of the Milnor sequence, for c.Rel i j: the connecting map of the product-complex short exact sequence, read on the product of the homologies, descends to the cokernel lim¹ of the shift.

@[simp]

theorem TauCeti.ComplexTower.limOneToHomology_mk {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) {i j : ι} (hij : c.Rel i j) (x : (C.homology i).Product) : (limOneToHomology hC hij) (Submodule.Quotient.mk x) = (CategoryTheory.ConcreteCategory.hom (⋯.δ i j hij)) ((C.productHomologyEquiv i).symm x)

The class of a family of homology classes is sent to the connecting map of the corresponding homology class of the product complex.

theorem TauCeti.ComplexTower.limOneToHomology_injective {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) {i j : ι} (hij : c.Rel i j) : Function.Injective ⇑(limOneToHomology hC hij)

Exactness of the Milnor sequence at lim¹. For a tower whose shift is surjective in every degree, the map lim¹ Hᵢ(Cₙ) → Hⱼ(lim C) is injective.

theorem TauCeti.ComplexTower.exact_limOneToHomology_homologyToLim {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) {i j : ι} (hij : c.Rel i j) : Function.Exact ⇑(limOneToHomology hC hij) ⇑(C.homologyToLim j)

Exactness of the Milnor sequence at Hⱼ(lim C). For a tower whose shift is surjective in every degree, the image of lim¹ Hᵢ(Cₙ) → Hⱼ(lim C) is the kernel of Hⱼ(lim C) → lim Hⱼ(Cₙ).

theorem TauCeti.ComplexTower.homologyToLim_surjective {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) (j : ι) : Function.Surjective ⇑(C.homologyToLim j)

Exactness of the Milnor sequence at lim Hⱼ(Cₙ). For a tower whose shift is surjective in every degree, the map Hⱼ(lim C) → lim Hⱼ(Cₙ) is surjective.

theorem TauCeti.ComplexTower.homologyToLim_bijective {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) {i j : ι} (hij : c.Rel i j) [Subsingleton (C.homology i).limOne] : Function.Bijective ⇑(C.homologyToLim j)

If the shift of every tower of terms is surjective and lim¹ Hᵢ(Cₙ) vanishes, for instance when the tower of degree-i homology modules is Mittag-Leffler, then Hⱼ(lim C) → lim Hⱼ(Cₙ) is bijective.

theorem TauCeti.ComplexTower.transition_comp_homologyMap_π {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (s : CategoryTheory.Limits.Cone C) (j : ι) (n : ℕ) : (C.homology j).transition n ∘ₗ ModuleCat.Hom.hom (HomologicalComplex.homologyMap (s.π.app (Opposite.op (n + 1))) j) = ModuleCat.Hom.hom (HomologicalComplex.homologyMap (s.π.app (Opposite.op n)) j)

The maps induced on homology by the legs of a cone over a tower of complexes are compatible with the transitions of the tower of homology modules.

theorem TauCeti.ComplexTower.quasiIso_isLimitLimComplexCone_lift {R : Type u} [Ring R] {ι : Type w} {c : ComplexShape ι} {C : ComplexTower R c} (hC : ∀ (i : ι), Function.Surjective ⇑(C.term i).shift) (s : CategoryTheory.Limits.Cone C) (hs : ∀ (j : ι), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → QuasiIsoAt (s.π.app (Opposite.op n)) j) : QuasiIso (C.isLimitLimComplexCone.lift s)

Quasi-isomorphisms into the limit of a tower of complexes. Let C be a tower of complexes whose shift is surjective in every degree, for instance one whose transitions are surjective in every degree. If s is a cone over C whose legs s.pt → Cₙ induce isomorphisms on the degree-j homology for all sufficiently large n, for every j, then the induced map from s.pt to the limit complex is a quasi-isomorphism.