OAI/Algebra/Finitistic/Bar/LeadingBarSuffix.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.ParityBridge.outerCast line 23

   Source documentation

   Retain the exterior D coefficient while applying an exact degree transport.

   def outerCast {a b : ℕ} (h : a=b) :
       D ⊗[k] term k A N a →ₗ[D] D ⊗[k] term k A N b :=
   …

   Mentions: OAI.DerivedBar.term

2. theorem OAI.DerivedBar.ParityBridge.outerCast_refl line 27
3. theorem OAI.DerivedBar.ParityBridge.outerCast_trans line 31
4. theorem OAI.DerivedBar.ParityBridge.twoSidedParity_outerCast line 37
5. def OAI.DerivedBar.ParityBridge.outerBarSuffix line 45

   Source documentation

   The exterior free D bar uses its actual categorical coordinates.

   def outerBarSuffix (V : ModuleCat.{u} D) (s i : ℕ)
       (e : V →ₗ[k] term k A N s) :
       ((DB).obj V).X i →ₗ[D] D ⊗[k] term k A N (s+i) :=
   …

   Mentions: OAI.DerivedBar.term

6. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_map line 50
7. theorem OAI.DerivedBar.ParityBridge.parity_outerBarSuffix line 61
8. theorem OAI.DerivedBar.ParityBridge.parity_outerBarSuffix_zero line 78
9. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_neg line 88
10. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_zero line 102
11. def OAI.DerivedBar.ParityBridge.outerBaseEmbed line 116
12. theorem OAI.DerivedBar.ParityBridge.coefficient_baseEmbed line 119
13. theorem OAI.DerivedBar.ParityBridge.parity_outerBaseEmbed line 128
14. theorem OAI.DerivedBar.ParityBridge.outerSuffixEmbed_id line 140
15. theorem OAI.DerivedBar.ParityBridge.parity_outerBarSuffix_terminal line 149