ModuleMultibarCoordinates.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.RecursiveTotal.moduleShape_toList line 15
Source documentation
The supported index change preserves the literal D/X word.
```
theorem moduleShape_toList (r n : ℕ)
    (t : {t : Index (r+1) n // inputDegree (r+1) t=0}) :
    Multibar.Indexed.toList (moduleShapeEquiv r n t) = leadingPattern r n t.val := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.Multibar.Indexed.toList, OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv, OAI.DerivedBar.RecursiveTotal.leadingPattern

theorem OAI.DerivedBar.RecursiveTotal.summand_isZero line 26

Source documentation

A zero input term remains zero through every additive bar degree functor.

theorem summand_isZero
    (B : ℕ → ModuleCat.{u} D ⥤ ChainComplex (ModuleCat.{u} D) ℕ)
    [∀ r, (B r).Additive] (Z : ChainComplex (ModuleCat.{u} D) ℕ)
    (r n : ℕ) (t : Index r n) (h : IsZero (Z.X (inputDegree r t))) :
    IsZero (summand B Z r n t) := by
…

Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.summand

theorem OAI.DerivedBar.RecursiveTotal.moduleSummand_isZero line 49
Source documentation
Positive final input degrees contribute zero, without any assumption on X.
```
theorem moduleSummand_isZero (r n : ℕ) (t : Index (r+1) n)
    (h : inputDegree (r+1) t ≠ 0) :
    IsZero (summand (leadingBarSequence k D X r) Z (r+1) n t) :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.leadingBarSequence
def OAI.DerivedBar.RecursiveTotal.moduleSummandIso line 56
Source documentation
Each surviving recursive-total summand is the exact previously indexed block tensor in degree r+n; the input is the original D-module.
```
def moduleSummandIso (r n : ℕ)
    (t : {t : Index (r+1) n // inputDegree (r+1) t=0}) :
    summand (leadingBarSequence k D X r) Z (r+1) n t.val ≅
      ModuleCat.of D (Multibar.Indexed.outerTensor k D X N (moduleShapeEquiv r n t)) := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv
def OAI.DerivedBar.RecursiveTotal.reindexedModuleSummandIso line 74
Source documentation
The exact block tensor after reindexing supported summands by Shape.
```
def reindexedModuleSummandIso (r n : ℕ) (p : Multibar.Indexed.Shape (r+n) r) :
    summand (leadingBarSequence k D X r) Z (r+1) n ((moduleShapeEquiv r n).symm p).val ≅
      ModuleCat.of D (Multibar.Indexed.outerTensor k D X N p) := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv, OAI.DerivedBar.Multibar.Indexed.outerTensor
def OAI.DerivedBar.RecursiveTotal.moduleFlatCoordinates line 84
Source documentation
All recursive-total terms are identified with the manuscript's exact finite sum of tensor blocks. This includes discarding only proved zero input-degree terms.
```
def moduleFlatCoordinates (r n : ℕ) :
    (flatLeadingMultibar k D X Z r).X n ≅
      ModuleCat.of D (⨁ p : Multibar.Indexed.Shape (r+n) r,
        Multibar.Indexed.outerTensor k D X N p) := by
…
```
Mentions: OAI.DerivedBar.flatLeadingMultibar, OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor
def OAI.DerivedBar.RecursiveTotal.leadingModuleCoordinates line 97
Source documentation
The degreewise tensor-block isomorphism for the actual recursive leading total.
```
def leadingModuleCoordinates (r n : ℕ) :
    (barTotal k D (explicitMultibar k D X r Z)).X n ≅
      ModuleCat.of D (⨁ p : Multibar.Indexed.Shape (r+n) r,
        Multibar.Indexed.outerTensor k D X N p) :=
…
```
Mentions: OAI.DerivedBar.barTotal, OAI.DerivedBar.explicitMultibar, OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor