DirectSumCoproduct.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.moduleSumCocone line 13
Source documentation
The native algebraic direct sum, with its actual coproduct maps.
```
def moduleSumCocone (F : Discrete ℕ ⥤ ModuleCat.{u} D) : Cocone F where
…
```
def OAI.DerivedBar.moduleSumIsColimit line 17
def OAI.DerivedBar.directSumComplexInclusion line 40
Source documentation
The canonical summand map into the already constructed chain direct sum.
```
def directSumComplexInclusion (S : ℕ → ChainComplex (ModuleCat.{u} D) ℕ) (r : ℕ) :
    S r ⟶ directSumComplex S where
…
```
Mentions: OAI.DerivedBar.directSumComplex
def OAI.DerivedBar.directSumComplexCocone line 56
def OAI.DerivedBar.directSumComplexIsColimit line 62
Source documentation
The native componentwise chain direct sum is the actual categorical coproduct.
```
def directSumComplexIsColimit (S : ℕ → ChainComplex (ModuleCat.{u} D) ℕ) :
    IsColimit (directSumComplexCocone D S) := by
…
```
Mentions: OAI.DerivedBar.directSumComplexCocone