Commit 2024-11-30 00:02 9bdc1af7

View on Github →

feat(Algebra/Homology/Embedding): the left homology of an extension of homological complexes (#18502) Given an embedding e : c.Embedding c', K : HomologicalComplex C c, and degrees such that e.f j = j', we construct a left homology data for K.extend e in degree j' from a left homology data for K in degree j.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean

added theorem HomologicalComplex.extend.comp_d_eq_zero_iff

added theorem HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff'

added theorem HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

added def CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff'

added def CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff

added def CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff'

added def CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff