OAI/Algebra/Finitistic/Bar/IndexedAssemblyComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.assembly_eq line 11
2. def OAI.DerivedBar.ParityBridge.shapeAssembly line 40
3. theorem OAI.DerivedBar.ParityBridge.shapeAssembly_injective line 45
4. theorem OAI.DerivedBar.ParityBridge.shapeAssembly_lof line 49
5. theorem OAI.DerivedBar.ParityBridge.outerInclusion_eqToHom line 60
6. theorem OAI.DerivedBar.ParityBridge.reindexedModuleSummand_assembly line 67
7. theorem OAI.DerivedBar.ParityBridge.moduleFlatCoordinates_inv_flatEmbedding line 78

   Source documentation

   The new embedding is exactly the old Shape assembly after the old inverse coordinates. No new differential or replacement coordinate system is used.

   theorem moduleFlatCoordinates_inv_flatEmbedding (r n : ℕ) :
       (moduleFlatCoordinates k D X N r n).inv ≫ flatEmbedding k D X N r n =
         shapeAssembly k D X N r n := by
   …

   Mentions: OAI.DerivedBar.ParityBridge.flatEmbedding, OAI.DerivedBar.ParityBridge.shapeAssembly

8. theorem OAI.DerivedBar.ParityBridge.flatEmbedding_coordinates line 93