SplitProjectiveTail.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ProjectiveTail.exact_of_local_contraction line 13
Source documentation
A local contracting identity forces exactness, without assumptions on the first or third term.
```
theorem exact_of_local_contraction (S : ShortComplex C)
    (a : S.X₂ ⟶ S.X₁) (b : S.X₃ ⟶ S.X₂)
    (h : a ≫ S.f + S.g ≫ b = 𝟙 _) : S.Exact := by
…
```

theorem OAI.DerivedBar.ProjectiveTail.contraction_of_splittings line 30

Source documentation

Three adjacent split cycle sequences contract the middle degree.

theorem contraction_of_splittings (n : ℕ)
    (s0 : (cyclesSequence K n).Splitting)
    (s1 : (cyclesSequence K (n+1)).Splitting)
    (s2 : (cyclesSequence K (n+2)).Splitting) :
    (s1.r ≫ s2.s) ≫ K.d (n+3) (n+2) +
      K.d (n+2) (n+1) ≫ (s0.r ≫ s1.s) = 𝟙 (K.X (n+2)) := by
…

Mentions: OAI.DerivedBar.ProjectiveTail.cyclesSequence

theorem OAI.DerivedBar.ProjectiveTail.map_exact_of_splittings line 52

Source documentation

Every additive functor preserves exactness in such a split tail.

theorem map_exact_of_splittings (F : C ⥤ E) [F.Additive] (n : ℕ)
    (s0 : (cyclesSequence K n).Splitting)
    (s1 : (cyclesSequence K (n+1)).Splitting)
    (s2 : (cyclesSequence K (n+2)).Splitting) :
    ((F.mapHomologicalComplex (.down ℕ)).obj K).ExactAt (n+2) := by
…

Mentions: OAI.DerivedBar.ProjectiveTail.cyclesSequence

theorem OAI.DerivedBar.ProjectiveTail.map_exact_tail line 68

Source documentation

A global dimension bound makes the exact projective tail split, uniformly for every additive functor. The harmless two-degree allowance avoids boundary conventions and suffices for finite cohomological amplitude.

theorem map_exact_tail (F : C ⥤ E) [F.Additive] (a g : ℕ)
    (he : ∀ i, a ≤ i → K.ExactAt i)
    (hp : ∀ i, Projective (K.X i))
    (hg : ∀ M : C, HasProjectiveDimensionLE M g)
    (n : ℕ) (hn : a+g+2 ≤ n) :
    ((F.mapHomologicalComplex (.down ℕ)).obj K).ExactAt n := by
…