IntegerCountShift.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.shapeCount_le line 32
theorem OAI.DerivedBar.ParityBridge.signedBlock_isZero_of_lt line 35
theorem OAI.DerivedBar.ParityBridge.deshiftedCount_isZero_positive line 43
Source documentation
The actual -r-shifted count complex is strictly zero in positive cochain degrees, including the range cut off by the lower count bound.
```
theorem deshiftedCount_isZero_positive (r : ℕ) (j : ℤ) (hj : 0<j) :
    IsZero ((deshiftedCount k D X N r).X j) := by
…
```
Mentions: OAI.DerivedBar.ParityBridge.deshiftedCount
instance OAI.DerivedBar.ParityBridge.deshiftedCount_strictSupport line 61
def OAI.DerivedBar.ParityBridge.integerIndexedDeshiftedCountIso line 72
Source documentation
Extension of the genuine recursive complex is the actual -r shift of the count complex. Strict support, not truncation by assumption, supplies the inverse.
```
def integerIndexedDeshiftedCountIso (r : ℕ) :
    (integerExtension D).obj (indexedMultibar k D X N r) ≅ deshiftedCount k D X N r :=
…
```
Mentions: OAI.DerivedBar.integerExtension, OAI.DerivedBar.ParityBridge.deshiftedCount
def OAI.DerivedBar.ParityBridge.integerIndexedCountShiftIso line 79
Source documentation
The manuscript's actual [r] cochain shift of the indexed recursive bar is isomorphic to the entire signed count complex.
```
def integerIndexedCountShiftIso (r : ℕ) :
    ((integerExtension D).obj (indexedMultibar k D X N r))⟦(r:ℤ)⟧ ≅
      (integerExtension D).obj (K r) :=
…
```
Mentions: OAI.DerivedBar.integerExtension