OAI/Algebra/AuslanderReiten/Resolutions/CProjectiveResolution.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.Resolution.Simple line 19
  2. def OAI.ArExplicit.Resolution.objects line 21
  3. def OAI.ArExplicit.Resolution.differential line 25
  4. theorem OAI.ArExplicit.Resolution.differential_comp line 29
  5. def OAI.ArExplicit.Resolution.complex line 40
  6. instance OAI.ArExplicit.Resolution.complex_projective line 43
  7. instance OAI.ArExplicit.Resolution.complex_scalar line 46
  8. instance OAI.ArExplicit.Resolution.complex_finite line 51
  9. def OAI.ArExplicit.Resolution.NoPositivePowerOne line 56
  10. theorem OAI.ArExplicit.Resolution.denominator_power_ne line 59
  11. theorem OAI.ArExplicit.Resolution.differential_exact line 64
  12. theorem OAI.ArExplicit.Resolution.complex_exactAt_succ line 76
  13. def OAI.ArExplicit.Resolution.augmentation line 83
  14. instance OAI.ArExplicit.Resolution.augmentation_epi line 86
  15. theorem OAI.ArExplicit.Resolution.differential_augmentation line 89
  16. def OAI.ArExplicit.Resolution.toSimple line 94
  17. theorem OAI.ArExplicit.Resolution.toSimple_zero line 97
  18. theorem OAI.ArExplicit.Resolution.augmentation_exact line 100
  19. theorem OAI.ArExplicit.Resolution.toSimple_quasiIso line 106
  20. def OAI.ArExplicit.Resolution.projectiveResolution line 123
  21. theorem OAI.ArExplicit.Resolution.baseField_noPositivePowerOne line 129
  22. def OAI.ArExplicit.Resolution.baseFieldProjectiveResolution line 133