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
.