OAI/Algebra/Finitistic/Ordinary/OrdinaryTriangularExactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.TriangularExactness.exact_of_diagonal line 17

   Source documentation

   A finite upper triangular differential with exact diagonal complexes is exact. The argument eliminates one coordinate at a time; the modules may be arbitrary.

   theorem exact_of_diagonal
       (d : (∀ i, E i) →ₗ[R] (∀ i, F i)) (e : (∀ i, F i) →ₗ[R] (∀ i, G i))
       (d₀ : ∀ i, E i →ₗ[R] F i) (e₀ : ∀ i, F i →ₗ[R] G i)
       (hzero : e.comp d = 0)
       (hd : ∀ (i : Fin l) (x : E i) (j : Fin l), j.val < i.val → d (Pi.single i x) j = 0)
       (hdi : ∀ (i : Fin l) (x : E i), d (Pi.single i x) i = d₀ i x)
       (he : ∀ (i : Fin l) (z : ∀ j, F j), (∀ j : Fin l, j.val < i.val → z j = 0) →
         e z i = e₀ i (z i))
       (hex : ∀ i, Function.Exact (d₀ i) (e₀ i)) : Function.Exact d e := by
   …