The homology of a square-zero linear endomorphism

A linear endomorphism d of a module M with d ∘ d = 0 is a differential module, and its homology is the kernel of d modulo its image. This file names that quotient concretely as d.homology hd = ker d ⧸ im d, where hd : d ∘ₗ d = 0, and identifies it with Mathlib's categorical homology of the short complex M ⟶ M ⟶ M whose two maps are d (LinearMap.homologyIso).

The concrete quotient is what one needs to transport extra structure to homology that the category of modules over the ring of d does not see, for instance an internal grading over a smaller coefficient ring by which d is homogeneous: the elements of d.homology hd are classes of elements of M, on which such structure is defined. The image is represented inside the kernel by boundariesInKer.

Main definitions

• LinearMap.boundariesInKer: the image of d as a submodule of the kernel of d.
• LinearMap.homology: for square-zero d, the kernel of d modulo its image.
• LinearMap.homologyπ: the class of an element of the kernel.
• LinearMap.homologyIso: for d ∘ d = 0, Mathlib's homology of the short complex with both maps d is d.homology hd.
• LinearMap.homologyMap: the map on homology induced by a chain map f with f ∘ d = e ∘ f.
• LinearMap.mappingCone: the mapping cone (m, n) ↦ (-d m, f m + e n) of such a chain map.
• LinearMap.sumMappingCone: the mapping cone of a map between free modules ι →₀ S and κ →₀ S, as an endomorphism of the free module (ι ⊕ κ) →₀ S.

Main results

• LinearMap.mem_boundariesInKer: an element of the kernel is a boundary exactly when it lies in the image of d.
• LinearMap.range_moduleCatToCycles_eq_boundariesInKer: for d ∘ d = 0, the boundaries used by Mathlib's explicit homology of a short complex of modules are d.boundariesInKer.
• LinearMap.homologyMap_surjective_iff and LinearMap.homologyMap_injective_iff: elementwise descriptions of surjectivity and injectivity of the map induced on homology.
• LinearMap.ker_le_range_mappingCone_iff: a chain map induces a bijection on homology exactly when its mapping cone is exact.
• LinearMap.ker_le_range_sumMappingCone_iff: the kernel of the mapping cone on (ι ⊕ κ) →₀ S lies in its range exactly when the same holds for the mapping cone on (ι →₀ S) × (κ →₀ S).
• HomologicalComplex.quasiIso_iff_bijective_homologyMap: a morphism of complexes of modules of shape ComplexShape.refl Unit, that is, of modules with a square-zero endomorphism, is a quasi-isomorphism exactly when it induces a bijection on ker d ⧸ im d.

@[reducible, inline]

abbrev LinearMap.boundariesInKer {S : Type u_1} {M : Type u_2} [Semiring S] [AddCommMonoid M] [Module S M] (d : M →ₗ[S] M) : Submodule S ↥d.ker

The intersection of the image and kernel of a linear endomorphism d, viewed as a submodule of the kernel. For a square-zero endomorphism, this is its full image.

Equations

• d.boundariesInKer = Submodule.comap d.ker.subtype d.range

theorem LinearMap.mem_boundariesInKer {S : Type u_1} {M : Type u_2} [Semiring S] [AddCommMonoid M] [Module S M] (d : M →ₗ[S] M) {z : ↥d.ker} : z ∈ d.boundariesInKer ↔ ↑z ∈ d.range

An element of the kernel of d is a boundary exactly when it is a value of d.

@[reducible, inline]

abbrev LinearMap.homology {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (_hd : d ∘ₗ d = 0) : Type u_2

The homology ker d ⧸ im d of a square-zero linear endomorphism d.

Equations

• d.homology _hd = (↥d.ker ⧸ d.boundariesInKer)

noncomputable def LinearMap.homologyπ {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) : ↥d.ker →ₗ[S] d.homology hd

The class in the homology of d of an element of the kernel of d.

Equations

• d.homologyπ hd = d.boundariesInKer.mkQ

@[simp]

theorem LinearMap.homologyπ_apply {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) (z : ↥d.ker) : (d.homologyπ hd) z = Submodule.Quotient.mk z

The class of an element of the kernel is its class modulo the boundaries.

theorem LinearMap.homologyπ_surjective {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) : Function.Surjective ⇑(d.homologyπ hd)

Every homology class is the class of an element of the kernel.

theorem LinearMap.homologyπ_eq_zero_iff {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) (z : ↥d.ker) : (d.homologyπ hd) z = 0 ↔ ↑z ∈ d.range

An element of the kernel has zero class exactly when it is a value of d.

@[reducible, inline]

abbrev LinearMap.shortComplex {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) : CategoryTheory.ShortComplex (ModuleCat S)

The short complex M ⟶ M ⟶ M of S-modules whose two maps are a square-zero endomorphism d.

Equations

• d.shortComplex hd = { X₁ := ↧M, X₂ := ↧M, X₃ := ↧M, f := ModuleCat.ofHom d, g := ModuleCat.ofHom d, zero := ⋯ }

theorem LinearMap.range_moduleCatToCycles_eq_boundariesInKer {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) : (d.shortComplex hd).moduleCatToCycles.range = d.boundariesInKer

For a square-zero endomorphism d, the boundaries of Mathlib's explicit homology of the short complex M ⟶ M ⟶ M with both maps d are the image of d inside its kernel.

noncomputable def LinearMap.homologyIso {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) : (d.shortComplex hd).homology ≅ ↧(d.homology hd)

For a square-zero endomorphism d, Mathlib's homology of the short complex M ⟶ M ⟶ M with both maps d is the concrete homology ker d ⧸ im d.

Equations

• d.homologyIso hd = (d.shortComplex hd).moduleCatHomologyIso ≪≫ ((d.shortComplex hd).moduleCatToCycles.range.quotEquivOfEq d.boundariesInKer ⋯).toModuleIso

noncomputable def LinearMap.homologyMap {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : d.homology hd →ₗ[S] e.homology he

The map on homology induced by a chain map f from (M, d) to (N, e), that is, a linear map with f ∘ d = e ∘ f: the class of a cycle z goes to the class of f z.

Equations

• LinearMap.homologyMap f hd he hf = d.boundariesInKer.mapQ e.boundariesInKer (f.restrict ⋯) ⋯

@[simp]

theorem LinearMap.homologyMap_mk {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) (z : ↥d.ker) : (homologyMap f hd he hf) (Submodule.Quotient.mk z) = Submodule.Quotient.mk ⟨f ↑z, ⋯⟩

The induced map on homology sends the class of a cycle z to the class of f z.

@[simp]

theorem LinearMap.homologyMap_id {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) : homologyMap id hd hd ⋯ = id

The identity chain map induces the identity map on homology.

@[simp]

theorem LinearMap.homologyMap_zero {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) {N : Type u_3} [AddCommGroup N] [Module S N] (e : N →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) : homologyMap 0 hd he ⋯ = 0

The zero chain map induces the zero map on homology.

@[simp]

theorem LinearMap.homologyMap_neg {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : homologyMap (-f) hd he ⋯ = -homologyMap f hd he hf

The map on homology induced by -f is the negative of the map induced by f.

@[simp]

theorem LinearMap.homologyMap_add {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f g : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) (hg : g ∘ₗ d = e ∘ₗ g) : homologyMap (f + g) hd he ⋯ = homologyMap f hd he hf + homologyMap g hd he hg

The map on homology induced by f + g is the sum of the maps induced by f and g.

@[simp]

theorem LinearMap.homologyMap_sub {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f g : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) (hg : g ∘ₗ d = e ∘ₗ g) : homologyMap (f - g) hd he ⋯ = homologyMap f hd he hf - homologyMap g hd he hg

The map on homology induced by f - g is the difference of the maps induced by f and g.

theorem LinearMap.homologyMap_comp {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} {P : Type u_4} [AddCommGroup P] [Module S P] {q : P →ₗ[S] P} (g : N →ₗ[S] P) (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hq : q ∘ₗ q = 0) (hf : f ∘ₗ d = e ∘ₗ f) (hg : g ∘ₗ e = q ∘ₗ g) : homologyMap (g ∘ₗ f) hd hq ⋯ = homologyMap g he hq hg ∘ₗ homologyMap f hd he hf

The map on homology induced by a composite is the composite of the induced maps.

@[simp]

theorem LinearMap.homologyMap_comp_homologyMap {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} {P : Type u_4} [AddCommGroup P] [Module S P] {q : P →ₗ[S] P} (g : N →ₗ[S] P) (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hq : q ∘ₗ q = 0) (hf : f ∘ₗ d = e ∘ₗ f) (hg : g ∘ₗ e = q ∘ₗ g) : homologyMap g he hq hg ∘ₗ homologyMap f hd he hf = homologyMap (g ∘ₗ f) hd hq ⋯

The composite of two induced maps on homology is the map induced by the composite. This is homologyMap_comp read right to left, the orientation usable by simp: its left-hand side mentions the intermediate differential e, which the left-hand side of homologyMap_comp does not.

@[simp]

theorem LinearMap.homologyMap_homologyMap {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} {P : Type u_4} [AddCommGroup P] [Module S P] {q : P →ₗ[S] P} (g : N →ₗ[S] P) (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hq : q ∘ₗ q = 0) (hf : f ∘ₗ d = e ∘ₗ f) (hg : g ∘ₗ e = q ∘ₗ g) (c : d.homology hd) : (homologyMap g he hq hg) ((homologyMap f hd he hf) c) = (homologyMap (g ∘ₗ f) hd hq ⋯) c

Applying two induced maps on homology in turn is applying the map induced by the composite.

theorem LinearMap.homologyMap_surjective_iff {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : Function.Surjective ⇑(homologyMap f hd he hf) ↔ ∀ n ∈ e.ker, ∃ m ∈ d.ker, n - f m ∈ e.range

The map induced by f on homology is surjective exactly when every cycle of e differs from the image of a cycle of d by a boundary.

theorem LinearMap.homologyMap_injective_iff {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] {d : M →ₗ[S] M} {N : Type u_3} [AddCommGroup N] [Module S N] {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : Function.Injective ⇑(homologyMap f hd he hf) ↔ ∀ m ∈ d.ker, f m ∈ e.range → m ∈ d.range

The map induced by f on homology is injective exactly when every cycle of d whose image under f is a boundary is itself a boundary.

def LinearMap.mappingCone {S : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring S] [AddCommGroup M] [Module S M] [AddCommMonoid N] [Module S N] (d : M →ₗ[S] M) (e : N →ₗ[S] N) (f : M →ₗ[S] N) : M × N →ₗ[S] M × N

The mapping cone of a linear map f : M → N between modules with endomorphisms d and e: the endomorphism (m, n) ↦ (-d m, f m + e n) of M × N. It squares to zero when d and e do and f is a chain map (LinearMap.mappingCone_comp_self).

Equations

• d.mappingCone e f = ((-d) ∘ₗ LinearMap.fst S M N).prod (f.coprod e)

@[simp]

theorem LinearMap.mappingCone_apply {S : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring S] [AddCommGroup M] [Module S M] [AddCommMonoid N] [Module S N] {d : M →ₗ[S] M} {e : N →ₗ[S] N} (f : M →ₗ[S] N) (x : M × N) : (d.mappingCone e f) x = (-d x.1, f x.1 + e x.2)

The mapping cone sends (m, n) to (-d m, f m + e n).

theorem LinearMap.mappingCone_comp_self {S : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring S] [AddCommGroup M] [Module S M] [AddCommMonoid N] [Module S N] {d : M →ₗ[S] M} {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : d.mappingCone e f ∘ₗ d.mappingCone e f = 0

The mapping cone of a chain map between square-zero endomorphisms squares to zero.

theorem LinearMap.ker_le_range_mappingCone_iff {S : Type u_1} {M : Type u_2} {N : Type u_3} [Ring S] [AddCommGroup M] [Module S M] [AddCommGroup N] [Module S N] {d : M →ₗ[S] M} {e : N →ₗ[S] N} (f : M →ₗ[S] N) (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : (d.mappingCone e f).ker ≤ (d.mappingCone e f).range ↔ Function.Bijective ⇑(homologyMap f hd he hf)

A chain map induces a bijection on homology exactly when its mapping cone is exact, that is, when every element killed by the mapping cone is in its image.

Mapping cones of maps between free modules

noncomputable def LinearMap.sumMappingCone {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (e : (κ →₀ S) →ₗ[S] κ →₀ S) (f : (ι →₀ S) →ₗ[S] κ →₀ S) : (ι ⊕ κ →₀ S) →ₗ[S] ι ⊕ κ →₀ S

The mapping cone of a map f : (ι →₀ S) → (κ →₀ S) between free modules with endomorphisms d and e, as an endomorphism of the free module (ι ⊕ κ) →₀ S on the disjoint union of the two bases: LinearMap.mappingCone d e f transported along Finsupp.sumFinsuppLEquivProdFinsupp.

Equations

• d.sumMappingCone e f = (Finsupp.sumFinsuppLEquivProdFinsupp S).symm.conjRingEquiv (d.mappingCone e f)

@[simp]

theorem LinearMap.sumMappingCone_apply {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (e : (κ →₀ S) →ₗ[S] κ →₀ S) (f : (ι →₀ S) →ₗ[S] κ →₀ S) (x : ι ⊕ κ →₀ S) : (d.sumMappingCone e f) x = (Finsupp.sumFinsuppLEquivProdFinsupp S).symm ((d.mappingCone e f) ((Finsupp.sumFinsuppLEquivProdFinsupp S) x))

The mapping cone on (ι ⊕ κ) →₀ S is the mapping cone on (ι →₀ S) × (κ →₀ S) between the two Finsupp sum-product equivalences.

theorem LinearMap.sumMappingCone_single_inl_apply_inl {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (e : (κ →₀ S) →ₗ[S] κ →₀ S) (f : (ι →₀ S) →ₗ[S] κ →₀ S) (i j : ι) (c : S) : ((d.sumMappingCone e f) (Finsupp.single (Sum.inl i) c)) (Sum.inl j) = -(d (Finsupp.single i c)) j

The coefficient of the mapping cone between two generators of ι is minus that of d.

theorem LinearMap.sumMappingCone_single_inl_apply_inr {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (e : (κ →₀ S) →ₗ[S] κ →₀ S) (f : (ι →₀ S) →ₗ[S] κ →₀ S) (i : ι) (k : κ) (c : S) : ((d.sumMappingCone e f) (Finsupp.single (Sum.inl i) c)) (Sum.inr k) = (f (Finsupp.single i c)) k

The coefficient of the mapping cone from a generator of ι to a generator of κ is that of f.

theorem LinearMap.sumMappingCone_single_inr_apply_inl {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (e : (κ →₀ S) →ₗ[S] κ →₀ S) (f : (ι →₀ S) →ₗ[S] κ →₀ S) (k : κ) (i : ι) (c : S) : ((d.sumMappingCone e f) (Finsupp.single (Sum.inr k) c)) (Sum.inl i) = 0

The mapping cone has no coefficient from a generator of κ to a generator of ι.

theorem LinearMap.sumMappingCone_single_inr_apply_inr {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (e : (κ →₀ S) →ₗ[S] κ →₀ S) (f : (ι →₀ S) →ₗ[S] κ →₀ S) (k k' : κ) (c : S) : ((d.sumMappingCone e f) (Finsupp.single (Sum.inr k) c)) (Sum.inr k') = (e (Finsupp.single k c)) k'

The coefficient of the mapping cone between two generators of κ is that of e.

theorem LinearMap.sumMappingCone_comp_self {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] {d : (ι →₀ S) →ₗ[S] ι →₀ S} {e : (κ →₀ S) →ₗ[S] κ →₀ S} {f : (ι →₀ S) →ₗ[S] κ →₀ S} (hd : d ∘ₗ d = 0) (he : e ∘ₗ e = 0) (hf : f ∘ₗ d = e ∘ₗ f) : d.sumMappingCone e f ∘ₗ d.sumMappingCone e f = 0

The mapping cone on (ι ⊕ κ) →₀ S of a chain map between square-zero endomorphisms squares to zero.

theorem LinearMap.ker_le_range_sumMappingCone_iff {S : Type u_1} {ι : Type u_2} {κ : Type u_3} [Ring S] {d : (ι →₀ S) →ₗ[S] ι →₀ S} {e : (κ →₀ S) →ₗ[S] κ →₀ S} {f : (ι →₀ S) →ₗ[S] κ →₀ S} : (d.sumMappingCone e f).ker ≤ (d.sumMappingCone e f).range ↔ (d.mappingCone e f).ker ≤ (d.mappingCone e f).range

The kernel of the mapping cone on (ι ⊕ κ) →₀ S lies in its range exactly when the kernel of the mapping cone on (ι →₀ S) × (κ →₀ S) lies in its range.

Quasi-isomorphisms of one-object complexes

theorem HomologicalComplex.hom_d_comp_hom_d {S : Type u_1} [Ring S] (K : HomologicalComplex (ModuleCat S) (ComplexShape.refl Unit)) : ModuleCat.Hom.hom (K.d () ()) ∘ₗ ModuleCat.Hom.hom (K.d () ()) = 0

The unique differential of a complex of shape ComplexShape.refl Unit squares to zero, as a linear map.

theorem HomologicalComplex.Hom.hom_f_comp_hom_d {S : Type u_1} [Ring S] {K L : HomologicalComplex (ModuleCat S) (ComplexShape.refl Unit)} (φ : K ⟶ L) : ModuleCat.Hom.hom (φ.f ()) ∘ₗ ModuleCat.Hom.hom (K.d () ()) = ModuleCat.Hom.hom (L.d () ()) ∘ₗ ModuleCat.Hom.hom (φ.f ())

The unique component of a morphism of complexes of shape ComplexShape.refl Unit is a chain map in the sense of LinearMap.homologyMap.

theorem HomologicalComplex.quasiIso_iff_bijective_homologyMap {S : Type u_1} [Ring S] {K L : HomologicalComplex (ModuleCat S) (ComplexShape.refl Unit)} (φ : K ⟶ L) : QuasiIso φ ↔ Function.Bijective ⇑(LinearMap.homologyMap (ModuleCat.Hom.hom (φ.f ())) ⋯ ⋯ ⋯)

Quasi-isomorphisms of one-object complexes are detected on ker d ⧸ im d. A morphism of complexes of modules of shape ComplexShape.refl Unit is a quasi-isomorphism exactly when its unique component induces a bijection between the concrete homologies LinearMap.homology.