OAI/Algebra/Finitistic/Localization/BoundedDerivedEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.underlyingKProjective line 13
  2. def OAI.LittleFinitistic.FiniteProjectiveHomotopy.derivedEmbedding line 23

    Source documentation

    The canonical derived-category functor on the actual bounded projective source.

    def derivedEmbedding : K.{u,v} R ⥤ DerivedCategory (ModuleCat.{v} R) :=
…
  3. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.derivedEmbeddingFaithful line 26
  4. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.derivedEmbeddingFull line 31
  5. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.derivedEmbeddingShift line 39
  6. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.derivedEmbeddingTriangulated line 41
  7. def OAI.LittleFinitistic.FiniteProjectiveHomotopy.boundedDerivedEquivalence line 45

    Source documentation

    Bounded complexes of f.g. projectives form a full subcategory of the actual derived category.

    def boundedDerivedEquivalence : K.{u,v} R ≌ (derivedEmbedding.{u,v} R).EssImageSubcategory :=
…