DerivedBarCoproduct.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.shiftedIterateDiagram line 27
Source documentation
The actual discrete diagram of genuine shifted finite derived tensor iterates.
```
def shiftedIterateDiagram : Discrete ℕ ⥤ DerivedCategory (ModuleCat.{u} D) :=
…
```
def OAI.DerivedBar.ParityBridge.shiftedIterateCountIso line 32
def OAI.DerivedBar.ParityBridge.shiftedIterateCocone line 36
def OAI.DerivedBar.ParityBridge.shiftedIterateIsColimit line 42
Source documentation
Both existence and uniqueness in the derived coproduct universal property hold for the shifted iterates, without assuming a central splitting theorem.
```
def shiftedIterateIsColimit : IsColimit (shiftedIterateCocone k D X N) :=
…
```
Mentions: OAI.DerivedBar.ParityBridge.shiftedIterateCocone
instance OAI.DerivedBar.ParityBridge.hasColimitShiftedIterates line 46
def OAI.DerivedBar.ParityBridge.derivedBarSplitting line 52
Source documentation
Manuscript prop:bar-splitting, eq:bar-splitting: the balanced tensor of D with the verified free A-bar resolution is isomorphic, in the genuine integer derived category, to the actual coproduct of (F^r N)[r].
```
def derivedBarSplitting :
    (integerQ D).obj (tensorBarComplex k A D N (fstHom k D X)) ≅
      colimit (shiftedIterateDiagram k D X N) :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.tensorBarComplex, OAI.DerivedBar.ParityBridge.shiftedIterateDiagram