Theorems · Definition · category theory
CategoryTheory.ShortComplex.abLeftHomologyData
(S : CategoryTheory.ShortComplex Ab) → S.LeftHomologyData
The explicit left homology data of a short complex of abelian group that is
given by a kernel and a quotient given by the AddMonoidHom API.
- Defined in
- Mathlib.Algebra.Homology.ShortComplex.Ab
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- HasQuotient.Quotientproof · cited by 2,301
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- CategoryTheory.ShortComplex.X₂proof · cited by 1,115
- CategoryTheory.ShortComplex.gproof · cited by 658
- AddCommGrpCat.carrierproof · cited by 407
- CategoryTheory.ShortComplex.LeftHomologyDatastatement · cited by 212
- Abstatement and proof · cited by 198
- AddMonoidHom.kerproof · cited by 158
- AddMonoidHom.rangeproof · cited by 142
- AddCommGrpCat.ofproof · cited by 97
- AddSubgroup.subtypeproof · cited by 82
- AddCommGrpCat.Hom.homproof · cited by 72
Cited by9
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.abCyclesIsoproof · cited by 2
- CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCyclesproof · cited by 1
- CategoryTheory.ShortComplex.abLeftHomologyData_f'statement · cited by 1
- CategoryTheory.ShortComplex.exact_iff_surjective_abToCyclesproof · cited by 1
- CategoryTheory.ShortComplex.abHomologyIsoproof · cited by 0
- CategoryTheory.ShortComplex.abLeftHomologyData_H_coestatement and proof · cited by 0
- CategoryTheory.ShortComplex.abLeftHomologyData_K_coestatement and proof · cited by 0
- CategoryTheory.ShortComplex.abLeftHomologyData_istatement and proof · cited by 0
- CategoryTheory.ShortComplex.abLeftHomologyData_πstatement and proof · cited by 0