OAI/Algebra/AuslanderReiten/Bar/TwistedBar.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.AbsoluteBar.twistEnveloping line 13
  2. def OAI.ArExplicit.AbsoluteBar.twistedModule line 16
  3. def OAI.ArExplicit.AbsoluteBar.twistedObject line 20
  4. instance OAI.ArExplicit.AbsoluteBar.twistedBaseModule line 24
  5. instance OAI.ArExplicit.AbsoluteBar.twistedModuleTower line 27
  6. instance OAI.ArExplicit.AbsoluteBar.twistInvPair line 35
  7. instance OAI.ArExplicit.AbsoluteBar.twistInvPairSymm line 39
  8. def OAI.ArExplicit.AbsoluteBar.twistedEquiv line 43
  9. theorem OAI.ArExplicit.AbsoluteBar.twistedFree line 52
  10. theorem OAI.ArExplicit.AbsoluteBar.twistedProjective line 57
  11. theorem OAI.ArExplicit.AbsoluteBar.twistedFinite line 62
  12. def OAI.ArExplicit.AbsoluteBar.twistedToOrdinary line 67
  13. def OAI.ArExplicit.AbsoluteBar.casimirInsertionMap line 84
  14. def OAI.ArExplicit.AbsoluteBar.twistedDifferential line 90
  15. def OAI.ArExplicit.AbsoluteBar.twistedComplex line 97
  16. theorem OAI.ArExplicit.AbsoluteBar.twistedComplex_d line 106
  17. theorem OAI.ArExplicit.AbsoluteBar.twistedDifferential_exact line 113
  18. def OAI.ArExplicit.AbsoluteBar.twistedAugmentation line 120
  19. theorem OAI.ArExplicit.AbsoluteBar.twistedAugmentation_zero line 130
  20. theorem OAI.ArExplicit.AbsoluteBar.twistedComplex_exactAt line 135
  21. def OAI.ArExplicit.AbsoluteBar.twistedResolution line 144
  22. theorem OAI.ArExplicit.AbsoluteBar.casimirInsertionMap_boundary line 171
  23. theorem OAI.ArExplicit.AbsoluteBar.casimirInsertionMap_boundary_zero line 181