ChainSplitting.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.directSumComplex line 12
Source documentation
The direct sum of module chain complexes, with the componentwise actual differential.
```
def directSumComplex {R : Type u} [Ring R] (C : ℕ → ChainComplex (ModuleCat R) ℕ) :
    ChainComplex (ModuleCat R) ℕ :=
…
```
def OAI.DerivedBar.SquareZero.countSplitting line 36
Source documentation
Chain-level count splitting of the actual two-sided absolute bar complex. This is the first chain isomorphism in the proof of manuscript prop:bar-splitting. Identification of these summands with derived tensor iterates is a separate dependency.
```
def countSplitting :
    directSumComplex (twoSidedWeightComplex k D X N hN) ≅
      twoSidedComplex k (TrivSqZeroExt D X) D N (fstHom k D X) :=
…
```
Mentions: OAI.DerivedBar.directSumComplex, OAI.DerivedBar.SquareZero.twoSidedWeightComplex, OAI.DerivedBar.twoSidedComplex