OAI/Algebra/Finitistic/Localization/FiniteProjectiveHomotopy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.FiniteProjectiveHomotopy.ComplexProperty line 17

   Source documentation

   Actual bounded complexes of finitely generated projective right/left modules, according to the chosen scalar ring R.

   def ComplexProperty (K : CochainComplex (ModuleCat.{v} R) ℤ) : Prop :=
   …

   Mentions: OAI.LittleFinitistic.FiniteProjectiveHomotopy.K

2. def OAI.LittleFinitistic.FiniteProjectiveHomotopy.objects line 21
3. theorem OAI.LittleFinitistic.FiniteProjectiveHomotopy.objects_quotient line 24
4. lemma OAI.LittleFinitistic.FiniteProjectiveHomotopy.finite_of_iso line 27
5. lemma OAI.LittleFinitistic.FiniteProjectiveHomotopy.finite_biprod line 30
6. lemma OAI.LittleFinitistic.FiniteProjectiveHomotopy.mappingCone_property line 34
7. lemma OAI.LittleFinitistic.FiniteProjectiveHomotopy.finite_projective_of_isZero line 52
8. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.objectsZero line 57
9. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.objectsShift line 64
10. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.objectsClosed₃ line 78
11. instance OAI.LittleFinitistic.FiniteProjectiveHomotopy.objectsTriangulated line 89
12. abbrev OAI.LittleFinitistic.FiniteProjectiveHomotopy.K line 93

    Source documentation

    K^b(proj-R), as a full subcategory with actual bounded f.g. projective representatives.

    abbrev K := (objects.{u,v} R).FullSubcategory

13. abbrev OAI.LittleFinitistic.FiniteProjectiveHomotopy.inclusion line 96

    Source documentation

    Its full and faithful inclusion into the ambient homotopy category.

    abbrev inclusion : K.{u,v} R ⥤ HomotopyCategory (ModuleCat.{v} R) (.up ℤ) := (objects R).ι
    …

    Mentions: OAI.LittleFinitistic.FiniteProjectiveHomotopy.objects