BimoduleResolutionBarAPI.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleTotal.ofNonpositiveResolution line 19
Source documentation
Package exactly the ordinary worker's actual bounded bimodule resolution API. Augmentation, quasi-isomorphism, projectivity and support are all explicit.
```
def ofNonpositiveResolution : AugmentedProjective k B P X where
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.AugmentedProjective
def OAI.LittleFinitistic.BimoduleTotal.nonpositiveResolutionBarIso line 28
Source documentation
Integration API for Q_X: the native integer-derived functor agrees naturally with the genuine bar-derived functor after chainToIntegerDerived.
```
def nonpositiveResolutionBarIso :
    DerivedBar.chainToIntegerDerived B ⋙ (R).data.derived ≅
      DerivedBar.derivedTensor k B (barModule (X := X)) ⋙ DerivedBar.chainToIntegerDerived B :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensor, OAI.LittleFinitistic.BimoduleTotal.barModule
def OAI.LittleFinitistic.BimoduleTotal.nonpositiveResolutionPowerIso line 36
Source documentation
Exact source-style F^r applied to a native degree-zero module, represented by the genuine Section 6 indexed multibar. All comparison data is constructed.
```
def nonpositiveResolutionPowerIso (N : ModuleCat.{u} B) (r : ℕ) :
    ((R).data.derived.obj^[r]) (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.singleInput, OAI.DerivedBar.integerExtension, OAI.DerivedBar.RecursiveTotal.indexedMultibar, OAI.LittleFinitistic.BimoduleTotal.barModule