OAI/Algebra/Finitistic/Localization/BoundedRepresentatives.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BoundedHomotopy.representative line 10

   Source documentation

   An actual bounded representative of each homotopy-category object.

   def representative (X : K C) : Complex C :=
   …

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

2. theorem OAI.LittleFinitistic.BoundedHomotopy.quotient_representative line 13
3. def OAI.LittleFinitistic.BoundedHomotopy.representativeMap line 20

   Source documentation

   A bounded chain-map representative of a homotopy-category morphism.

   def representativeMap {X Y : K C} (f : X ⟶ Y) :
       representative C X ⟶ representative C Y :=
   …

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

4. theorem OAI.LittleFinitistic.BoundedHomotopy.quotient_representativeMap line 24
5. def OAI.LittleFinitistic.BoundedHomotopy.nullHomotopy line 29

   Source documentation

   Zero in K means a genuine right-linear null-homotopy of the chain representative.

   def nullHomotopy {X Y : Complex C} (f : X ⟶ Y) (hf : (quotient C).map f = 0) :
       Homotopy f.hom 0 :=
   …

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