OrdinaryShiftSign.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.unsignedShift line 11
Source documentation
Reindex P by b, retaining the original differential. This is what the resolution computes.
```
def unsignedShift (P : CochainComplex C ℤ) (b : ℤ) : CochainComplex C ℤ where
…
```
def OAI.LittleFinitistic.OrdinarySimulation.integerUnitIso line 21
Source documentation
Multiplication by an integer unit is an actual isomorphism in any additive category.
```
def integerUnitIso (X : C) (u : ℤˣ) : X ≅ X where
…
```
def OAI.LittleFinitistic.OrdinarySimulation.shiftSignIso line 32
Source documentation
The source's degree-n sign (-1)^(b*n), for all integers b and n.
```
def shiftSignIso (P : CochainComplex C ℤ) (b : ℤ) : unsignedShift P b ≅ P⟦b⟧ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.unsignedShift