OAI/Algebra/Finitistic/Dimension/PDLowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.PDTensor.tor_zero_of_pdLT line 14

   Source documentation

   Any right module detects a lower bound through nonzero Tor; it need not be flat, finite-dimensional, or annihilated by the radical.

   theorem tor_zero_of_pdLT (n : ℕ) (h : HasProjectiveDimensionLT M.cat n) :
       IsZero (Tor (k := k) U M.cat n) := by
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Tor

2. theorem OAI.LittleFinitistic.PDTensor.le_projectiveDimension_of_nonzero_Tor line 27
3. theorem OAI.LittleFinitistic.PDTensor.lower_bound_of_nonzero_Tor line 32
4. theorem OAI.LittleFinitistic.PDTensor.projectiveDimension_lt_top_of_bounded_residueTor line 37

   Source documentation

   Bounded radical-quotient Tor gives finite numerical projective dimension.

   theorem projectiveDimension_lt_top_of_bounded_residueTor
       (h : ∃ b : ℕ, ∀ n, b < n → IsZero (Tor (k := k) (Residue (A := A)) M.cat n)) :
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue