MultibarFlattenDerived.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.leadingBarSequence line 16
Source documentation
The actual sequence of two-sided X bars, ending in one leading free D bar.
```
def leadingBarSequence (r j : ℕ) :
    ModuleCat.{u} D ⥤ ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
instance OAI.DerivedBar.leadingBarSequence_additive line 20
theorem OAI.DerivedBar.leadingBarSequence_prefix line 28
Source documentation
Before the final D bar, the actual recursive complexes agree.
```
theorem leadingBarSequence_prefix (r n : ℕ) (h : n≤r) :
    RecursiveTotal.iter (leadingBarSequence k D X r) Z n = explicitMultibar k D X n Z := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.explicitMultibar
theorem OAI.DerivedBar.leadingBarSequence_total line 39
Source documentation
The final recursive total is precisely the manuscript's leading D bar.
```
theorem leadingBarSequence_total (r : ℕ) :
    RecursiveTotal.iter (leadingBarSequence k D X r) Z (r+1) =
      barTotal k D (explicitMultibar k D X r Z) := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.barTotal, OAI.DerivedBar.explicitMultibar
def OAI.DerivedBar.flatLeadingMultibar line 48
Source documentation
Literal finite direct sums, equipped with the independently recursive bar faces. No count differential or derived comparison is used in this definition.
```
def flatLeadingMultibar (r : ℕ) : ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
def OAI.DerivedBar.flatLeadingMultibarIso line 52
Source documentation
Chain isomorphism distributing all recursive X and leading-D totals.
```
def flatLeadingMultibarIso (r : ℕ) : flatLeadingMultibar k D X Z r ≅
    barTotal k D (explicitMultibar k D X r Z) :=
…
```
Mentions: OAI.DerivedBar.flatLeadingMultibar, OAI.DerivedBar.barTotal, OAI.DerivedBar.explicitMultibar
def OAI.DerivedBar.derivedIterateFlatIso line 59
Source documentation
The flattened complex represents actual finite iteration of the constructed left derived tensor. This uses the previously proved derived universal property.
```
def derivedIterateFlatIso (r : ℕ) :
    (derivedTensorIterate k D X r).obj ((chainQ D).obj Z) ≅
      (chainQ D).obj (flatLeadingMultibar k D X Z r) :=
…
```
Mentions: OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.flatLeadingMultibar