OAI/Algebra/Finitistic/Localization/ProjectiveComplexes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ProjectiveComplexes.RightModule line 15

   Source documentation

   Right B-modules are left modules over the opposite ring.

   abbrev RightModule := ModuleCat.{u} Bᵐᵒᵖ

2. def OAI.LittleFinitistic.ProjectiveComplexes.finiteProjective line 17
3. instance OAI.LittleFinitistic.ProjectiveComplexes.(instance at line 20) line 20
4. instance OAI.LittleFinitistic.ProjectiveComplexes.(instance at line 27) line 27
5. instance OAI.LittleFinitistic.ProjectiveComplexes.(instance at line 31) line 31
6. instance OAI.LittleFinitistic.ProjectiveComplexes.(instance at line 48) line 48
7. abbrev OAI.LittleFinitistic.ProjectiveComplexes.Proj line 51

   Source documentation

   The additive category of finitely generated projective right B-modules.

   abbrev Proj := (finiteProjective B).FullSubcategory

   Mentions: OAI.LittleFinitistic.ProjectiveComplexes.finiteProjective

8. instance OAI.LittleFinitistic.ProjectiveComplexes.(instance at line 53) line 53
9. abbrev OAI.LittleFinitistic.ProjectiveComplexes.Complex line 56

   Source documentation

   The actual category of bounded complexes of finitely generated projectives.

   abbrev Complex := BoundedHomotopy.Complex (Proj B)

   Mentions: OAI.LittleFinitistic.BoundedHomotopy.Complex, OAI.LittleFinitistic.ProjectiveComplexes.Proj

10. abbrev OAI.LittleFinitistic.ProjectiveComplexes.K line 59

    Source documentation

    Section 3's K = Kᵇ(proj-B), with homotopy classes of chain maps.

    abbrev K := BoundedHomotopy.K (Proj B)

    Mentions: OAI.LittleFinitistic.BoundedHomotopy.K, OAI.LittleFinitistic.ProjectiveComplexes.Proj

11. example OAI.LittleFinitistic.ProjectiveComplexes.(example at line 61) line 61
12. example OAI.LittleFinitistic.ProjectiveComplexes.(example at line 62) line 62
13. abbrev OAI.LittleFinitistic.ProjectiveComplexes.quotient line 65

    Source documentation

    The passage from bounded projective complexes to their homotopy category.

    abbrev quotient : Complex B ⥤ K B := BoundedHomotopy.quotient (Proj B)
    …

    Mentions: OAI.LittleFinitistic.ProjectiveComplexes.Complex, OAI.LittleFinitistic.ProjectiveComplexes.K, OAI.LittleFinitistic.BoundedHomotopy.quotient, OAI.LittleFinitistic.ProjectiveComplexes.Proj