OAI/Algebra/Finitistic/Bar/ProjectiveTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DerivedBar.ProjectiveTail.cyclesSequence line 12
2. def OAI.DerivedBar.ProjectiveTail.cyclesSequenceKernel line 17
3. theorem OAI.DerivedBar.ProjectiveTail.cyclesSequence_exact line 29
4. theorem OAI.DerivedBar.ProjectiveTail.cyclesSequence_shortExact line 32
5. theorem OAI.DerivedBar.ProjectiveTail.cycles_projective line 51

   Source documentation

   In an exact tail of projective terms, projective dimension drops by one at each successive cycle. This does not identify free terms with finite length.

   theorem cycles_projective (a g : ℕ)
       (he : ∀ i, a ≤ i → K.ExactAt i)
       (hp : ∀ i, Projective (K.X i))
       (hd : HasProjectiveDimensionLE (K.cycles a) g) :
       Projective (K.cycles (a+g)) := by
   …