Commit 2023-04-18 10:45 8accf7ab

View on Github →

feat: port Algebra.Homology.Homology (#3491)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Homology.lean

added def ChainComplex.homologySuccIso

added def ChainComplex.homologyZeroIso

added def CochainComplex.homologySuccIso

added def CochainComplex.homologyZeroIso

added def HomologicalComplex.boundariesIsoImage

added theorem HomologicalComplex.boundaries_eq_bot

added theorem HomologicalComplex.boundaries_eq_imageSubobject

added theorem HomologicalComplex.boundaries_le_cycles

added def HomologicalComplex.cyclesIsoKernel

added theorem HomologicalComplex.cycles_eq_kernelSubobject

added theorem HomologicalComplex.cycles_eq_top

added def HomologicalComplex.homologyIso

added theorem HomologicalComplex.imageToKernel_as_boundariesToCycles

added def boundariesFunctor

added def boundariesToCyclesNatTrans

added theorem boundariesToCycles_naturality

added def cyclesFunctor

added theorem cyclesMap_arrow

added theorem cyclesMap_comp

added theorem cyclesMap_id

added def gradedHomologyFunctor

added def homologyFunctor