Commit 2024-01-05 14:50 710ecf07
View on Github →feat(Algebra/Homology): left shifting cochains (#9054)
In this PR, we study the behaviour of cochains (of the complex of homomorphisms) with respect to shifts on the source. In particular, we obtain an additive equivalence leftShiftAddEquiv K L n a n' h : Cochain K L n ≃+ Cochain K⟦a⟧ L n' when h : n + a = n'.