OAI/Algebra/Finitistic/Localization/ConcreteChainRepresentatives.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ConcreteChainRepresentatives.representative line 13
2. theorem OAI.LittleFinitistic.ConcreteChainRepresentatives.representative_bounded line 15
3. theorem OAI.LittleFinitistic.ConcreteChainRepresentatives.quadratic_representatives line 21

   Source documentation

   The lifted source diagram has genuine bounded projective chain representatives and a specified null-homotopy for every relation; no chain representatives are assumed.

   theorem quadratic_representatives (na nb nr : ℕ) (X₀ X₁ X₂ : K P)
       (a : Fin na → (X₀ ⟶ X₁)) (b : Fin nb → (X₁ ⟶ X₂))
       (c : Fin nr → Fin na → Fin nb → k)
       (hc : ∀ r, ∑ i, ∑ j, c r i j • (a i ≫ b j) = 0) :
       ∃ (f : Fin na → (representative P X₀ ⟶ representative P X₁))
         (g : Fin nb → (representative P X₁ ⟶ representative P X₂)),
         (∀ i, (HomotopyCategory.quotient (Proj P) (.up ℤ)).map (f i) = (a i).hom) ∧
         (∀ j, (HomotopyCategory.quotient (Proj P) (.up ℤ)).map (g j) = (b j).hom) ∧
         Nonempty (∀ r, Homotopy (∑ i, ∑ j, c r i j • (f i ≫ g j)) 0) := by
   …

   Mentions: OAI.LittleFinitistic.ConcreteChainRepresentatives.representative