BlockCoordinateGenerators.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.RecursiveTotal.congrLinearEquiv_symm_lof line 14
theorem OAI.DerivedBar.RecursiveTotal.moduleFlatCoordinates_inv_lof line 37
Source documentation
The inverse coordinate map on a literal block generator is exactly its recursive tensor inclusion, with the proved tensor-coordinate isomorphism.
```
theorem moduleFlatCoordinates_inv_lof (r n : ℕ) (p : Multibar.Indexed.Shape (r+n) r) :
    ModuleCat.ofHom (DirectSum.lof D (Multibar.Indexed.Shape (r+n) r)
      (Multibar.Indexed.outerTensor k D X N) p) ≫ (moduleFlatCoordinates k D X N r n).inv =
    (reindexedModuleSummandIso k D X N r n p).inv ≫
      lof (leadingBarSequence k D X r) Z (r+1) n ((moduleShapeEquiv r n).symm p).val := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.RecursiveTotal.moduleFlatCoordinates, OAI.DerivedBar.RecursiveTotal.reindexedModuleSummandIso, OAI.DerivedBar.RecursiveTotal.lof, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv
theorem OAI.DerivedBar.RecursiveTotal.leadingModuleCoordinates_inv_lof line 60
Source documentation
The same inverse map into the actual leading total; this is the concrete map to use when comparing the literal parity faces with the recursive total.
```
theorem leadingModuleCoordinates_inv_lof (r n : ℕ) (p : Multibar.Indexed.Shape (r+n) r) :
    ModuleCat.ofHom (DirectSum.lof D (Multibar.Indexed.Shape (r+n) r)
      (Multibar.Indexed.outerTensor k D X N) p) ≫ (moduleFlatCoordinates k D X N r n).inv ≫
      assemble (leadingBarSequence k D X r) Z (r+1) n =
    (reindexedModuleSummandIso k D X N r n p).inv ≫
      inclusion (leadingBarSequence k D X r) Z (r+1) n ((moduleShapeEquiv r n).symm p).val := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.RecursiveTotal.moduleFlatCoordinates, OAI.DerivedBar.RecursiveTotal.assemble, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.RecursiveTotal.reindexedModuleSummandIso, OAI.DerivedBar.RecursiveTotal.inclusion, OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv
theorem OAI.DerivedBar.RecursiveTotal.indexedDifferential_on_block line 70
Source documentation
Full horizontal-plus-signed-vertical formula on each actual Shape summand. The index is obtained by the proved inverse parsing, not an assumed correspondence.
```
theorem indexedDifferential_on_block (r n : ℕ)
    (p : Multibar.Indexed.Shape (r+(n+1)) r) :
    let t := ((moduleShapeEquiv r (n+1)).symm p).val
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv