OAI/Algebra/Finitistic/Localization/UnderlyingRepresentatives.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.UnderlyingRepresentatives.forget line 13
2. abbrev OAI.LittleFinitistic.UnderlyingRepresentatives.complex line 16
3. theorem OAI.LittleFinitistic.UnderlyingRepresentatives.projective line 19
4. theorem OAI.LittleFinitistic.UnderlyingRepresentatives.finite line 23
5. theorem OAI.LittleFinitistic.UnderlyingRepresentatives.finiteDimensional line 29
6. theorem OAI.LittleFinitistic.UnderlyingRepresentatives.bounded line 36

   Source documentation

   Genuine boundedness after forgetting the projective subcategory.

   theorem bounded (X : K P) :
       ∃ lo hi : ℤ, ∀ n, n < lo ∨ hi < n → IsZero ((complex P X).X n) := by
   …

   Mentions: OAI.LittleFinitistic.UnderlyingRepresentatives.complex

7. def OAI.LittleFinitistic.UnderlyingRepresentatives.relationHomotopy line 48

   Source documentation

   The actual chain-representative relation homotopies survive the forgetful functor.

   def relationHomotopy (na nb nr : ℕ) (X₀ X₁ X₂ : K P)
       (f : Fin na → (representative P X₀ ⟶ representative P X₁))
       (g : Fin nb → (representative P X₁ ⟶ representative P X₂))
       (c : Fin nr → Fin na → Fin nb → k)
       (H : ∀ r, Homotopy (∑ i, ∑ j, c r i j • (f i ≫ g j)) 0) (r : Fin nr) :
       Homotopy
         (∑ i, ∑ j, c r i j •
           (((forget P).mapHomologicalComplex (.up ℤ)).map (f i) ≫
             ((forget P).mapHomologicalComplex (.up ℤ)).map (g j))) 0 := by
   …

   Mentions: OAI.LittleFinitistic.UnderlyingRepresentatives.forget