Theorems · Definition · category theory

CategoryTheory.ShortComplex.moduleCatLeftHomologyData

{R : Type u} → [inst : Ring R] → (S : CategoryTheory.ShortComplex (ModuleCat R)) → S.LeftHomologyData

The explicit left homology data of a short complex of modules that is given by a kernel and a quotient given by the LinearMap API. The projections to K and H are not simp lemmas because the generic lemmas about LeftHomologyData are more useful here.

Defined in

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Cited by

106 results in Mathlib

Foundations

Depth 91 from the axioms, rests on 1,590 definitions · uses propext, Classical.choice, Quot.sound

Assumes

Ring