SelectedPDBarConsumer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.SelectedPDDetection.baseBar line 11
Source documentation
The literal two-sided bar over the one fixed square-zero algebra.
```
abbrev baseBar (Y : FiniteSelectionFamily.S.{0}) :=
…
```
def OAI.LittleFinitistic.SelectedPDDetection.torIsoBaseBar line 15
Source documentation
Actual Tor at the native bar model, using the canonical augmentation.
```
def torIsoBaseBar (Y : FiniteSelectionFamily.S.{0}) (n : ℕ) :
    PDTensor.Tor (k := ℂ) (PDBarQuotient.RightBase augmentation) (module Y) n ≅
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDBarQuotient.RightBase
theorem OAI.LittleFinitistic.SelectedPDDetection.lower_bound_of_base_bar line 21

theorem OAI.LittleFinitistic.SelectedPDDetection.lower_bound_of_base_derived_bar line 31

Source documentation

Native supplies its actual D-linear derived splitting and the surviving summand's cohomology. The detector constructs the projective-dimension bound.

theorem lower_bound_of_base_derived_bar (Y : FiniteSelectionFamily.S.{0})
    (Z T : DerivedCategory (ModuleCat.{0} D))
    (e : PDBarQuotient.baseDerived augmentation (Inflated Y) ≅ Z)
    (i : T ⟶ Z) (p : Z ⟶ T) (hip : i ≫ p = 𝟙 T)
    (r n : ℕ) (hrn : r ≤ n)
    (h : ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj T)) :
    r ≤ projectiveDimension (module Y) :=
…

Mentions: OAI.LittleFinitistic.PDBarQuotient.baseDerived