IntegerDerivedMultibar.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.integerExtension line 18
Source documentation
Nonnegative homological degree n is genuine integer cochain degree -n; positive cochain degrees are extended by zero.
```
abbrev integerExtension : ChainComplex (ModuleCat.{u} D) ℕ ⥤
    CochainComplex (ModuleCat.{u} D) ℤ :=
…
```
def OAI.DerivedBar.integerQ line 23
Source documentation
The actual integer derived-category value of a nonnegative chain complex.
```
def integerQ : ChainComplex (ModuleCat.{u} D) ℕ ⥤ DerivedCategory (ModuleCat.{u} D) :=
…
```
theorem OAI.DerivedBar.integerQ_inverts line 26
def OAI.DerivedBar.chainToIntegerDerived line 34
Source documentation
Comparison from the nonnegative-chain localization into the genuine integer cochain derived category, obtained by its localization universal property.
```
def chainToIntegerDerived : chainDerived D ⥤ DerivedCategory (ModuleCat.{u} D) :=
…
```
Mentions: OAI.DerivedBar.chainDerived
def OAI.DerivedBar.chainToIntegerDerivedIso line 37
def OAI.DerivedBar.integerExtensionHomologyIso line 41
Source documentation
Exact homology-degree comparison for the integer construction.
```
def integerExtensionHomologyIso (Z : ChainComplex (ModuleCat.{u} D) ℕ) (n : ℕ) :
    ((integerExtension D).obj Z).homology (-(n : ℤ)) ≅ Z.homology n :=
…
```
Mentions: OAI.DerivedBar.integerExtension
def OAI.DerivedBar.integerDerivedIterateIndexedIso line 54
Source documentation
The constructed finite derived iterate, now viewed in the actual integer cochain derived category, is represented by the exact indexed block complex. This does not assert an extension of the tensor functor to arbitrary integer inputs.
```
def integerDerivedIterateIndexedIso (r : ℕ) :
    (chainToIntegerDerived D).obj
      ((derivedTensorIterate k D X r).obj ((chainQ D).obj Z)) ≅
    DerivedCategory.Q.obj
      ((integerExtension D).obj (RecursiveTotal.indexedMultibar k D X N r)) :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.integerExtension, OAI.DerivedBar.RecursiveTotal.indexedMultibar
def OAI.DerivedBar.integerIndexedLeadingIso line 63
Source documentation
The entire leading-bar chain isomorphism survives in the integer derived category.
```
def integerIndexedLeadingIso (r : ℕ) :
    (integerQ D).obj (RecursiveTotal.indexedMultibar k D X N r) ≅
      (integerQ D).obj (barTotal k D (explicitMultibar k D X r Z)) :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.RecursiveTotal.indexedMultibar, OAI.DerivedBar.barTotal, OAI.DerivedBar.explicitMultibar