OAI/Algebra/Finitistic/Localization/FiniteDerivedEvaluation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluationAdditive line 15
  2. instance OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluationLifting line 19
  3. instance OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluationShift line 24
  4. instance OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluationFactorsShift line 28
  5. instance OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluationTriangulated line 34
  6. abbrev OAI.LittleFinitistic.QuadraticEncoding.FiniteVectorDerived line 41

    Source documentation

    The full subcategory of the canonical derived category represented by bounded finite-dimensional complexes. Over a field all its terms are projective.

    abbrev FiniteVectorDerived := (derivedEmbedding.{u,max u v} k).EssImageSubcategory
  7. instance OAI.LittleFinitistic.QuadraticEncoding.derivedToEssImageShift line 43
  8. instance OAI.LittleFinitistic.QuadraticEncoding.derivedToEssImageTriangulated line 46
  9. def OAI.LittleFinitistic.QuadraticEncoding.derivedEvaluation line 50
  10. def OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluation line 53
  11. def OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluationFactors line 56
  12. instance OAI.LittleFinitistic.QuadraticEncoding.derivedEvaluationShift line 61
  13. instance OAI.LittleFinitistic.QuadraticEncoding.derivedEvaluationTriangulated line 64
  14. instance OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluationShift line 67
  15. instance OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluationTriangulated line 70