Commit 2023-06-21 01:19 d57027b2

View on Github →

feat: basic API for the right homology of short complexes (#5250) This PR introduces the basic API for the right homology of short complexes.

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

added theorem CategoryTheory.ShortComplex.HasRightHomology.mk'

added def CategoryTheory.ShortComplex.RightHomologyData.descH

added def CategoryTheory.ShortComplex.RightHomologyData.descQ

added def CategoryTheory.ShortComplex.RightHomologyData.g'

added def CategoryTheory.ShortComplex.RightHomologyData.hι'

added theorem CategoryTheory.ShortComplex.RightHomologyData.isIso_p

added theorem CategoryTheory.ShortComplex.RightHomologyData.isIso_ι

added def CategoryTheory.ShortComplex.RightHomologyData.liftH

added theorem CategoryTheory.ShortComplex.RightHomologyData.liftH_ι

added def CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork

added theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_g'

added def CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork

added theorem CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_g'

added def CategoryTheory.ShortComplex.RightHomologyData.ofZeros

added theorem CategoryTheory.ShortComplex.RightHomologyData.ofZeros_g'

added theorem CategoryTheory.ShortComplex.RightHomologyData.p_descQ

added theorem CategoryTheory.ShortComplex.RightHomologyData.p_g'

added theorem CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary

added theorem CategoryTheory.ShortComplex.RightHomologyData.ι_g'