OAI/Algebra/Finitistic/Localization/BoundedHomotopy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.BoundedHomotopy.boundedComplex line 12

    Source documentation

    Strict boundedness of the underlying complex, at both ends.

    def boundedComplex : ObjectProperty (CochainComplex C ℤ) :=
…
  2. abbrev OAI.LittleFinitistic.BoundedHomotopy.Complex line 16

    Source documentation

    The actual category of bounded cochain complexes, with chain maps.

    abbrev Complex := (boundedComplex C).FullSubcategory

    Mentions: OAI.LittleFinitistic.BoundedHomotopy.boundedComplex

  3. def OAI.LittleFinitistic.BoundedHomotopy.bounded line 19

    Source documentation

    Bounded representatives, with homotopy classes of chain maps.

    def bounded : ObjectProperty (HomotopyCategory C (.up ℤ)) :=
…
  4. theorem OAI.LittleFinitistic.BoundedHomotopy.bounded_quotient_obj_iff line 22
  5. instance OAI.LittleFinitistic.BoundedHomotopy.(instance at line 30) line 30
  6. instance OAI.LittleFinitistic.BoundedHomotopy.(instance at line 36) line 36
  7. theorem OAI.LittleFinitistic.BoundedHomotopy.bounded_mappingCone line 49
  8. instance OAI.LittleFinitistic.BoundedHomotopy.(instance at line 64) line 64
  9. instance OAI.LittleFinitistic.BoundedHomotopy.(instance at line 77) line 77
  10. abbrev OAI.LittleFinitistic.BoundedHomotopy.K line 81

    Source documentation

    The homotopy category Kᵇ(C); boundedness is part of each object.

    abbrev K := (bounded C).FullSubcategory

    Mentions: OAI.LittleFinitistic.BoundedHomotopy.bounded

  11. def OAI.LittleFinitistic.BoundedHomotopy.quotient line 84

    Source documentation

    Pass from bounded chain maps to their homotopy classes.

    def quotient : Complex C ⥤ K C :=
…

    Mentions: OAI.LittleFinitistic.BoundedHomotopy.Complex, OAI.LittleFinitistic.BoundedHomotopy.K

  12. instance OAI.LittleFinitistic.BoundedHomotopy.(instance at line 88) line 88