OAI/Algebra/AuslanderReiten/Bar/ModuleBar.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.ModuleBar.object line 14
  2. def OAI.ArExplicit.ModuleBar.left line 18
  3. theorem OAI.ArExplicit.ModuleBar.left_zero line 22
  4. theorem OAI.ArExplicit.ModuleBar.left_tmul line 23
  5. theorem OAI.ArExplicit.ModuleBar.left_one line 26
  6. theorem OAI.ArExplicit.ModuleBar.left_mul line 30
  7. def OAI.ArExplicit.ModuleBar.boundary line 35
  8. theorem OAI.ArExplicit.ModuleBar.boundary_zero_tmul line 39
  9. theorem OAI.ArExplicit.ModuleBar.boundary_succ_tmul line 41
  10. theorem OAI.ArExplicit.ModuleBar.boundary_left line 45
  11. def OAI.ArExplicit.ModuleBar.leftModule line 56
  12. def OAI.ArExplicit.ModuleBar.moduleObject line 59
  13. instance OAI.ArExplicit.ModuleBar.baseModule line 63
  14. instance OAI.ArExplicit.ModuleBar.moduleTower line 64
  15. def OAI.ArExplicit.ModuleBar.differential line 70
  16. theorem OAI.ArExplicit.ModuleBar.free line 74
  17. theorem OAI.ArExplicit.ModuleBar.finiteBase line 88
  18. theorem OAI.ArExplicit.ModuleBar.finite line 97
  19. theorem OAI.ArExplicit.ModuleBar.double_zero line 104

    Also declared: OAI/Algebra/AuslanderReiten/Bar/ModuleBarSuffix.lean:36 (same declaration text).

  20. theorem OAI.ArExplicit.ModuleBar.boundary_squared line 108
  21. def OAI.ArExplicit.ModuleBar.contraction line 125
  22. theorem OAI.ArExplicit.ModuleBar.contraction_identity line 128
  23. theorem OAI.ArExplicit.ModuleBar.augmentation_contraction line 136
  24. theorem OAI.ArExplicit.ModuleBar.differential_exact line 139
  25. def OAI.ArExplicit.ModuleBar.complex line 151
  26. theorem OAI.ArExplicit.ModuleBar.complex_d line 160
  27. def OAI.ArExplicit.ModuleBar.augmentation line 166
  28. theorem OAI.ArExplicit.ModuleBar.augmentation_zero line 176
  29. theorem OAI.ArExplicit.ModuleBar.complex_exactAt line 180
  30. def OAI.ArExplicit.ModuleBar.resolution line 188