SelectedPDConclusion.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.SelectedPDConclusion.baseTorIso line 15
Source documentation
The canonical base-change Tor is computed by the actual selected bar, independently of which compatible field-scalar instance presents that bar.
```
def baseTorIso (Y : FiniteSelectionFamily.S.{0}) (n : ℕ) :
    ((DerivedBar.Balanced.tensorFunctor augmentation).leftDerived n).obj (module Y) ≅
      (SelectedPDDetection.baseBar Y).homology n :=
…
```
Mentions: OAI.DerivedBar.Balanced.tensorFunctor, OAI.LittleFinitistic.SelectedPDDetection.baseBar
theorem OAI.LittleFinitistic.SelectedPDConclusion.finite_pd_of_extinction line 24
Source documentation
Actual tensor extinction implies finite projective dimension over the one fixed square-zero algebra A. The bar bounds and minimal detector are proved.
```
theorem finite_pd_of_extinction (Y : FiniteSelectionFamily.S.{0}) (t : ℕ)
    (h : IsZero (SelectedBaseIterates.object Y t)) :
    projectiveDimension (module Y) < ⊤ := by
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object
theorem OAI.LittleFinitistic.SelectedPDConclusion.lower_bound_of_survival line 37
Source documentation
A surviving actual derived iterate supplies a nonzero original count class and hence the manuscript's projective-dimension lower bound.
```
theorem lower_bound_of_survival (Y : FiniteSelectionFamily.S.{0}) (r : ℕ)
    (h : ¬ IsZero (SelectedBaseIterates.object Y r)) :
    (r : WithBot ℕ∞) ≤ projectiveDimension (module Y) := by
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object
theorem OAI.LittleFinitistic.SelectedPDConclusion.detection line 49
Source documentation
Both conclusions of the manuscript's projective-dimension detector for the actual finite selected family; no bar comparison or pd bound is a premise.
```
theorem detection (Y : FiniteSelectionFamily.S.{0}) :
    (∀ t, IsZero (SelectedBaseIterates.object Y t) → projectiveDimension (module Y) < ⊤) ∧
    (∀ r, ¬ IsZero (SelectedBaseIterates.object Y r) →
      (r : WithBot ℕ∞) ≤ projectiveDimension (module Y)) :=
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object