OAI/Algebra/AuslanderReiten/Fibers/FiniteEvaluatedFiber.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.FiniteLeftModule.pairModule line 15
  2. def OAI.ArExplicit.FiniteLeftModule.fiberReassociate line 23
  3. def OAI.ArExplicit.FiniteLeftModule.fiberPairProjection line 32
  4. def OAI.ArExplicit.FiniteLeftModule.fiberPairStableIso line 37
  5. theorem OAI.ArExplicit.FiniteLeftModule.fiberPairStableIso_hom line 43
  6. def OAI.ArExplicit.FiniteLeftModule.evaluatedPairEquiv line 55
  7. def OAI.ArExplicit.FiniteLeftModule.middlePairMap line 59
  8. def OAI.ArExplicit.FiniteLeftModule.evaluatedMiddleStableIso line 64
  9. theorem OAI.ArExplicit.FiniteLeftModule.evaluatedMiddleStableIso_hom line 70
  10. theorem OAI.ArExplicit.FiniteLeftModule.middlePairMap_fiberInclusion line 79
  11. theorem OAI.ArExplicit.FiniteLeftModule.fiberFunctionExact line 88
  12. def OAI.ArExplicit.FiniteLeftModule.evaluatedFiberTriangle line 99
  13. theorem OAI.ArExplicit.FiniteLeftModule.evaluatedFiberTriangle_distinguished line 105