OAI/Algebra/Finitistic/Bar/LeadingTotalComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.outerCast_smul line 28
2. theorem OAI.DerivedBar.ParityBridge.leadingTotalComparison_positive line 34
3. theorem OAI.DerivedBar.ParityBridge.leadingTotalComparison_bottom line 85
4. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_differential line 118

   Source documentation

   The canonical leading total embedding intertwines its original total horizontal/vertical differential with the literal square-zero-extension faces.

   theorem leadingTotalEmbedding_differential (r n : ℕ) :
       leadingTotalEmbedding k D X N r (n+1) ≫
         ModuleCat.ofHom (SquareZero.multibarTwoSidedDifferential k D X N (r+n)) =
       (barTotal k D (I r)).d (n+1) n ≫ leadingTotalEmbedding k D X N r n := by
   …

   Mentions: OAI.DerivedBar.ParityBridge.leadingTotalEmbedding, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.barTotal