OAI/Algebra/Finitistic/Bar/LeadingTotalDifferential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_d₁ line 28
2. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_d₂ line 40
3. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_d₁_zero line 58

   Source documentation

   Both total faces vanish at the respective zero degree by the actual chain shape.

   theorem leadingTotalEmbedding_d₁_zero (r n q : ℕ) :
       (K (I r)).d₁ c 0 q n ≫ leadingTotalEmbedding k D X N r n = 0 := by
   …

   Mentions: OAI.DerivedBar.ParityBridge.leadingTotalEmbedding

4. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_d₂_zero line 62
5. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_ι_d line 66