DerivedCountShift.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.integerIndexedWeightShiftIso line 36
Source documentation
Identification with the original count subcomplex, using the actual integer cochain shift and the already verified component sign involution.
```
def integerIndexedWeightShiftIso (r : ℕ) :
    ((integerExtension D).obj (indexedMultibar k D X N r))⟦(r:ℤ)⟧ ≅
      (integerExtension D).obj (SquareZero.twoSidedWeightComplex k D X N (inflated_ideal_zero D X N) r) :=
…
```
Mentions: OAI.DerivedBar.integerExtension, OAI.DerivedBar.SquareZero.twoSidedWeightComplex, OAI.DerivedBar.ParityBridge.inflated_ideal_zero
def OAI.DerivedBar.ParityBridge.derivedIterateWeightShiftIso line 47
Source documentation
Each original count summand is the genuine [r] shift of the constructed finite derived tensor iterate.
```
def derivedIterateWeightShiftIso (r : ℕ) :
    ((chainToIntegerDerived D).obj
      ((derivedTensorIterate k D X r).obj ((chainQ D).obj Z)))⟦(r:ℤ)⟧ ≅
    (integerQ D).obj (SquareZero.twoSidedWeightComplex k D X N (inflated_ideal_zero D X N) r) :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.integerQ, OAI.DerivedBar.SquareZero.twoSidedWeightComplex, OAI.DerivedBar.ParityBridge.inflated_ideal_zero