PDDetection.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDTensor.residueTensor_subsingleton_iff line 13
Source documentation
Nakayama detects zero modules using the actual radical-quotient tensor.
```
theorem residueTensor_subsingleton_iff
    (N : Type u) [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N]
    [Module.Finite A N] :
    Subsingleton (BalancedTensor.Tensor k A (Residue (A := A)) N) ↔ Subsingleton N := by
…
```
Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDTensor.residueTor_zero_iff_term line 32
Source documentation
For the semisimple quotient S, the n-th Tor is zero exactly when the n-th term of the constructed minimal projective resolution is zero.
```
theorem residueTor_zero_iff_term (n : ℕ) :
    IsZero (Tor (k := k) (Residue (A := A)) M.cat n) ↔
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDTensor.pdLE_iff_residueTor_zero line 47
Source documentation
Projective dimension of a finite-dimensional module over an actual finite-dimensional algebra is detected by its derived tensor with A/rad A. No detection theorem is assumed: the proof constructs minimal resolutions.
```
theorem pdLE_iff_residueTor_zero (n : ℕ) :
    HasProjectiveDimensionLE M.cat n ↔
      IsZero (Tor (k := k) (Residue (A := A)) M.cat (n+1)) := by
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDTensor.finite_pd_of_bounded_residueTor line 53
Source documentation
The finite-projective-dimension implication used in cor:pd-detection.
```
theorem finite_pd_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
theorem OAI.LittleFinitistic.PDTensor.projectiveDimension_le_of_residueTor_zero line 60
Source documentation
The conclusion uses mathlib's actual numerical projective dimension.
```
theorem projectiveDimension_le_of_residueTor_zero (n : ℕ)
    (h : IsZero (Tor (k := k) (Residue (A := A)) M.cat (n+1))) :
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue