DerivedTensorBarSplitting.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.homotopyToIntegerDerived line 17
Source documentation
Extension of the nonnegative homotopy category followed by the genuine integer derived localization.
```
abbrev homotopyToIntegerDerived : HomotopyCategory (ModuleCat.{u} D) (.down ℕ) ⥤
    DerivedCategory (ModuleCat.{u} D) :=
…
```
def OAI.DerivedBar.homotopyToIntegerDerivedIso line 21
abbrev OAI.DerivedBar.derivedBaseChange line 31
Source documentation
The actual left-derived balanced base-change functor on modules, viewed in the integer derived category.
```
abbrev derivedBaseChange : ModuleCat.{u} A ⥤ DerivedCategory (ModuleCat.{u} D) :=
…
```
def OAI.DerivedBar.derivedBaseChangeBarIso line 34
def OAI.DerivedBar.ParityBridge.derivedTensorBarSplitting line 60
Source documentation
The actual left-derived D tensor over A is the actual categorical coproduct of genuine shifted derived iterates. This proves the manuscript's bar-splitting proposition; projective-dimension detection is a separate result.
```
def derivedTensorBarSplitting :
    (derivedBaseChange D (fstHom k D X)).obj (ModuleCat.of A N) ≅
      colimit (shiftedIterateDiagram k D X N) :=
…
```
Mentions: OAI.DerivedBar.derivedBaseChange, OAI.DerivedBar.ParityBridge.shiftedIterateDiagram