PDResolutionDetection.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDTensor.bounded_residueTor_of_finite_pd line 11
theorem OAI.LittleFinitistic.PDTensor.finite_pd_iff_bounded_residueTor line 20
Source documentation
Finite projective dimension is equivalent to bounded actual residue Tor.
```
theorem finite_pd_iff_bounded_residueTor :
    projectiveDimension M.cat ≠ ⊤ ↔
      ∃ b : ℕ, ∀ n, b < n → IsZero (Tor (k := k) (Residue (A := A)) M.cat n) := by
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDTensor.finite_pd_of_resolution line 28
Source documentation
The upper detector accepts any actual projective resolution, including a bar resolution once its exactness and projectivity have been proved.
```
theorem finite_pd_of_resolution
    (P : ProjectiveResolution M.cat)
    (h : ∃ b : ℕ, ∀ n, b < n → IsZero
      (((tensorFunctor k A (Residue (A := A))).mapHomologicalComplex _).obj P.complex |>.homology n)) :
…
```
Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor, OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDTensor.lower_bound_of_resolution line 42
Source documentation
The lower detector also accepts any actual projective resolution. The nonzero class can be supplied by a summand of the bar decomposition.
```
theorem lower_bound_of_resolution (P : ProjectiveResolution M.cat) (r n : ℕ) (hrn : r ≤ n)
    (h : ¬ IsZero (((tensorFunctor k A U).mapHomologicalComplex _).obj P.complex |>.homology n)) :
    r ≤ projectiveDimension M.cat := by
…
```
Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor