OAI/Algebra/AuslanderReiten/Complete/TateKoszul.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.TateKoszul.degreeEquiv line 13
  2. structure OAI.ArExplicit.TateKoszul.Model line 19
  3. def OAI.ArExplicit.TateKoszul.positiveAt line 45
  4. def OAI.ArExplicit.TateKoszul.negativeAt line 49
  5. def OAI.ArExplicit.TateKoszul.row line 53
  6. def OAI.ArExplicit.TateKoszul.column line 55
  7. theorem OAI.ArExplicit.TateKoszul.row_apply line 58
  8. theorem OAI.ArExplicit.TateKoszul.column_apply line 61
  9. theorem OAI.ArExplicit.TateKoszul.positive_row line 64
  10. theorem OAI.ArExplicit.TateKoszul.positive_column line 74
  11. theorem OAI.ArExplicit.TateKoszul.negative_row line 85
  12. theorem OAI.ArExplicit.TateKoszul.negative_column line 95
  13. theorem OAI.ArExplicit.TateKoszul.surjective_of_chart line 113
  14. theorem OAI.ArExplicit.TateKoszul.injective_of_chart line 122
  15. theorem OAI.ArExplicit.TateKoszul.exact_of_charts line 131
  16. theorem OAI.ArExplicit.TateKoszul.row_surjective line 159
  17. theorem OAI.ArExplicit.TateKoszul.column_injective line 182
  18. theorem OAI.ArExplicit.TateKoszul.range_column_eq_ker_row line 205