BimoduleBarStalk.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleTotal.zeroDegreeIndex line 17
Source documentation
A support interval containing degree zero supplies the finite-total index; this is automatic for the ordinary resolution's interval [-length,0].
```
def zeroDegreeIndex (hlo : res.data.lower ≤ 0) (hhi : 0 ≤ res.data.upper) :
    Fin ((res.data.upper-res.data.lower).toNat+1) :=
…
```
theorem OAI.LittleFinitistic.BimoduleTotal.zeroDegreeIndex_eq line 21
def OAI.LittleFinitistic.BimoduleTotal.integerSingleIso line 26
Source documentation
The chain stalk's integer extension is the native integer stalk.
```
def integerSingleIso (N : ModuleCat.{u} B) :
    (DerivedBar.integerQ B).obj ((ChainComplex.single₀ _).obj N) ≅
      DerivedCategory.Q.obj (singleInput B N) :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.LittleFinitistic.BimoduleTotal.singleInput
def OAI.LittleFinitistic.BimoduleTotal.nativeStalkIndexedIso line 34
Source documentation
Genuine native iteration on the native integer stalk, identified with the actual Section 6 indexed multibar. No bar comparison is supplied as a premise.
```
def nativeStalkIndexedIso (hlo : res.data.lower ≤ 0) (hhi : 0 ≤ res.data.upper)
    (N : ModuleCat.{u} B) (r : ℕ) :
    (nativeIterate res r).obj (DerivedCategory.Q.obj (singleInput B N)) ≅
      DerivedCategory.Q.obj ((DerivedBar.integerExtension B).obj
        (DerivedBar.RecursiveTotal.indexedMultibar k B (barModule (X := X)) N r)) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.nativeIterate, OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.DerivedBar.integerExtension, OAI.DerivedBar.RecursiveTotal.indexedMultibar, OAI.LittleFinitistic.BimoduleTotal.barModule
theorem OAI.LittleFinitistic.BimoduleTotal.nativeIterate_obj line 45
Source documentation
Functor iteration here is the usual repeated application of the native integer-derived tensor on objects.
```
theorem nativeIterate_obj (r : ℕ) (Y : DerivedCategory (ModuleCat.{u} B)) :
    (nativeIterate res r).obj Y = (res.data.derived.obj^[r]) Y := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.nativeIterate