CountRetracts.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.directSumComplexProjection line 12
Source documentation
Projection from the original chain direct sum to its r-th complex.
```
def directSumComplexProjection (S : ℕ → ChainComplex (ModuleCat.{u} D) ℕ) (r : ℕ) :
    directSumComplex S ⟶ S r where
…
```
Mentions: OAI.DerivedBar.directSumComplex
theorem OAI.DerivedBar.directSumComplex_inclusion_projection line 25
theorem OAI.DerivedBar.ParityBridge.mapped_retract line 36
def OAI.DerivedBar.ParityBridge.countTensorBarInclusion line 64
Source documentation
The original count subcomplex included into the actual balanced tensor bar.
```
def countTensorBarInclusion (r : ℕ) : S r ⟶ T :=
…
```
def OAI.DerivedBar.ParityBridge.countTensorBarProjection line 68
theorem OAI.DerivedBar.ParityBridge.countTensorBar_retract line 72
def OAI.DerivedBar.ParityBridge.shiftedIterateInclusion line 78
Source documentation
The genuine shifted iterate included into actual left-derived base change.
```
def shiftedIterateInclusion (r : ℕ) :
    (shiftedIterateDiagram k D X N).obj ⟨r⟩ ⟶
      (derivedBaseChange D (fstHom k D X)).obj (ModuleCat.of A N) :=
…
```
Mentions: OAI.DerivedBar.ParityBridge.shiftedIterateDiagram, OAI.DerivedBar.derivedBaseChange
def OAI.DerivedBar.ParityBridge.shiftedIterateProjection line 85
theorem OAI.DerivedBar.ParityBridge.shiftedIterate_retract line 92