OAI/Algebra/Finitistic/Dimension/PDDimension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.PDMinimal.cover_subsingleton line 11
2. lemma OAI.LittleFinitistic.PDMinimal.cover_injective line 20
3. lemma OAI.LittleFinitistic.PDMinimal.next_subsingleton_of_projective line 37
4. theorem OAI.LittleFinitistic.PDMinimal.pdLT_of_term_zero line 46

   Source documentation

   Vanishing of a term of the constructed resolution gives the standard categorical projective-dimension bound.

   theorem pdLT_of_term_zero (M : FiniteModule k A) (n i : ℕ)
       (hz : Subsingleton (term M (i+n))) :
       HasProjectiveDimensionLT (syzygy M i).cat n := by
   …

   Mentions: OAI.LittleFinitistic.PDMinimal.FiniteModule, OAI.LittleFinitistic.PDMinimal.term, OAI.LittleFinitistic.PDMinimal.syzygy

5. lemma OAI.LittleFinitistic.PDMinimal.syzygy_projective line 62
6. theorem OAI.LittleFinitistic.PDMinimal.term_zero_of_pdLE line 75

   Source documentation

   Finite projective dimension forces the minimal resolution to terminate.

   theorem term_zero_of_pdLE (M : FiniteModule k A) (n : ℕ)
       (h : HasProjectiveDimensionLE M.cat n) : Subsingleton (term M (n+1)) := by
   …

   Mentions: OAI.LittleFinitistic.PDMinimal.FiniteModule, OAI.LittleFinitistic.PDMinimal.term

7. theorem OAI.LittleFinitistic.PDMinimal.pdLE_iff_term_zero line 86

   Source documentation

   The actual minimal-resolution term criterion, proved from covers and short-exact-sequence dimension shifting.

   theorem pdLE_iff_term_zero (M : FiniteModule k A) (n : ℕ) :
       HasProjectiveDimensionLE M.cat n ↔ Subsingleton (term M (n+1)) :=
   …

   Mentions: OAI.LittleFinitistic.PDMinimal.FiniteModule, OAI.LittleFinitistic.PDMinimal.term