IndexedMultibarTotal.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.RecursiveTotal.indexedModule line 21
def OAI.DerivedBar.RecursiveTotal.indexedDifferential line 28
Source documentation
The independently recursive multibar faces in the exact Shape coordinates. This uses the horizontal/vertical differential of RecursiveTotal, not the count complex differential.
```
def indexedDifferential (r n : ℕ) : indexedModule k D X N r (n+1) ⟶ indexedModule k D X N r n :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.indexedModule
theorem OAI.DerivedBar.RecursiveTotal.indexedDifferential_sq line 32
def OAI.DerivedBar.RecursiveTotal.indexedMultibar line 39
Source documentation
Exact tensor-block coordinates, with the unshifted multibar total degree n.
```
def indexedMultibar (r : ℕ) : ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
def OAI.DerivedBar.RecursiveTotal.indexedFlatIso line 44
Source documentation
Chain isomorphism from the exact tensor-block direct sum to the recursive flat model.
```
def indexedFlatIso (r : ℕ) : indexedMultibar k D X N r ≅ F r :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.indexedMultibar
def OAI.DerivedBar.RecursiveTotal.indexedLeadingIso line 58
Source documentation
Actual chain isomorphism flattening the recursive leading total into the same Shape-indexed block tensors as the square-zero count decomposition.
```
def indexedLeadingIso (r : ℕ) : indexedMultibar k D X N r ≅
    barTotal k D (explicitMultibar k D X r Z) :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.indexedMultibar, OAI.DerivedBar.barTotal, OAI.DerivedBar.explicitMultibar
theorem OAI.DerivedBar.RecursiveTotal.indexedDifferential_on_generator line 64
Source documentation
Exact signed differential formula on a recursive generator, now in the literal Shape-indexed block coordinates. The vertical face includes (-1)^i.
```
theorem indexedDifferential_on_generator (r n i q : ℕ) (h : i+q=n+1) (t : Index r q) :
    lof (B r) Z (r+1) (n+1) ⟨⟨⟨i,q⟩,h⟩,t⟩ ≫
      (moduleFlatCoordinates k D X N r (n+1)).hom ≫ indexedDifferential k D X N r n =
    (horizontal (B r) Z r n i q h t +
      vertical (B r) Z r n i q h t (differential (B r) Z r)) ≫
        (moduleFlatCoordinates k D X N r n).hom := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.lof, OAI.DerivedBar.RecursiveTotal.moduleFlatCoordinates, OAI.DerivedBar.RecursiveTotal.indexedDifferential, OAI.DerivedBar.RecursiveTotal.horizontal, OAI.DerivedBar.RecursiveTotal.vertical, OAI.DerivedBar.RecursiveTotal.differential
def OAI.DerivedBar.RecursiveTotal.derivedIterateIndexedIso line 79
Source documentation
Genuine derived tensor iteration represented by the exact indexed block complex. No count splitting or projective-dimension statement is assumed.
```
def derivedIterateIndexedIso (r : ℕ) :
    (derivedTensorIterate k D X r).obj ((chainQ D).obj Z) ≅
      (chainQ D).obj (indexedMultibar k D X N r) :=
…
```
Mentions: OAI.DerivedBar.derivedTensorIterate, OAI.DerivedBar.chainQ, OAI.DerivedBar.RecursiveTotal.indexedMultibar