OAI/Algebra/AuslanderReiten/Fibers/ConcreteFiberEvaluation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.T.evaluatedFiber line 18
  2. abbrev OAI.ArExplicit.T.evaluatedMiddle line 20
  3. def OAI.ArExplicit.T.evaluatedTwistPairEquiv line 22
  4. def OAI.ArExplicit.T.middleToSimplePair line 27
  5. def OAI.ArExplicit.T.middleSimpleStableIso line 31
  6. theorem OAI.ArExplicit.T.middleSimpleStableIso_hom line 36
  7. def OAI.ArExplicit.T.evaluatedRho₁ line 43
  8. def OAI.ArExplicit.T.evaluatedRho₂ line 47
  9. def OAI.ArExplicit.T.evaluatedFiberInclusion line 51
  10. theorem OAI.ArExplicit.T.middleToSimplePair_fiberInclusion line 56
  11. theorem OAI.ArExplicit.T.fiberTarget_right_projective line 63
  12. def OAI.ArExplicit.T.fiberEvaluationTriangle line 70
  13. theorem OAI.ArExplicit.T.fiberEvaluationTriangle_distinguished line 76