IntegerCountRestriction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.deshiftedCount line 39
Source documentation
The actual integer cochain count complex shifted by -r.
```
def deshiftedCount (r : ℕ) : CochainComplex C ℤ :=
…
```
def OAI.DerivedBar.ParityBridge.deshiftedCountRestriction line 42
def OAI.DerivedBar.ParityBridge.deshiftedCountXIso line 45
theorem OAI.DerivedBar.ParityBridge.units_hom_apply line 50
theorem OAI.DerivedBar.ParityBridge.deshiftedCount_sign line 56
Source documentation
The standard unit-valued cochain shift sign is the proved count sign.
```
theorem deshiftedCount_sign (r n : ℕ) :
    (-(r:ℤ)).negOnePow • (K r).d (r+(n+1)) (r+n) = indexedDifferential k D X N r n := by
…
```
theorem OAI.DerivedBar.ParityBridge.deshiftedCount_d line 82
def OAI.DerivedBar.ParityBridge.indexedDeshiftedCountIso line 96
Source documentation
A genuine chain isomorphism using the standard integer shift differential, not a newly stipulated shift or transported count differential.
```
def indexedDeshiftedCountIso (r : ℕ) : indexedMultibar k D X N r ≅
    deshiftedCountRestriction k D X N r :=
…
```
Mentions: OAI.DerivedBar.ParityBridge.deshiftedCountRestriction