Commit 2023-07-28 17:34 41b6cc2d

View on Github →

feat: basic right homology API of short complexes (#6008) This PR introduces basic API for the right homology of short complexes, like the definition of ShortComplex.rightHomology.

depends on: #5674

Estimated changes

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

added def CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork

added def CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork

added def CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork

added def CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork

added def CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros

added theorem CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq

added theorem CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq

added theorem CategoryTheory.ShortComplex.f_pOpcycles

added theorem CategoryTheory.ShortComplex.fromOpcycles_naturality

added theorem CategoryTheory.ShortComplex.isIso_pOpcycles

added theorem CategoryTheory.ShortComplex.isIso_rightHomologyι

added theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_hom_inv_id

added theorem CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv_hom_id

added theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_hom_inv_id

added theorem CategoryTheory.ShortComplex.opcyclesIsoX₂_inv_hom_id

added def CategoryTheory.ShortComplex.opcyclesMap'

added theorem CategoryTheory.ShortComplex.opcyclesMap'_comp

added theorem CategoryTheory.ShortComplex.opcyclesMap'_g'

added theorem CategoryTheory.ShortComplex.opcyclesMap'_id

added theorem CategoryTheory.ShortComplex.opcyclesMap'_zero

added theorem CategoryTheory.ShortComplex.opcyclesMap_comp

added theorem CategoryTheory.ShortComplex.opcyclesMap_id

added theorem CategoryTheory.ShortComplex.opcyclesMap_zero

added theorem CategoryTheory.ShortComplex.opcycles_ext

added theorem CategoryTheory.ShortComplex.opcycles_ext_iff

added theorem CategoryTheory.ShortComplex.p_fromOpcycles

added theorem CategoryTheory.ShortComplex.p_opcyclesMap'

added theorem CategoryTheory.ShortComplex.p_opcyclesMap

added def CategoryTheory.ShortComplex.rightHomologyMap'

added theorem CategoryTheory.ShortComplex.rightHomologyMap'_comp

added theorem CategoryTheory.ShortComplex.rightHomologyMap'_id

added theorem CategoryTheory.ShortComplex.rightHomologyMap'_zero

added def CategoryTheory.ShortComplex.rightHomologyMapData

added theorem CategoryTheory.ShortComplex.rightHomologyMap_comp

added theorem CategoryTheory.ShortComplex.rightHomologyMap_id

added theorem CategoryTheory.ShortComplex.rightHomologyMap_zero

added theorem CategoryTheory.ShortComplex.rightHomology_ext

added theorem CategoryTheory.ShortComplex.rightHomology_ext_iff

added theorem CategoryTheory.ShortComplex.rightHomologyι_naturality'

added theorem CategoryTheory.ShortComplex.rightHomologyι_naturality