SelectedPDUpperConsumer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.SelectedPDDetection.tensorBarDerivedIso line 16
Source documentation
Exact scalar/action-preserving identification with the source of the bar worker's actual derived splitting.
```
def tensorBarDerivedIso (Y : FiniteSelectionFamily.S.{0}) :
    (DerivedBar.integerQ D).obj
      (DerivedBar.tensorBarComplex ℂ A D (Inflated Y) augmentation) ≅
        PDBarQuotient.baseDerived augmentation (Inflated Y) :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.tensorBarComplex, OAI.LittleFinitistic.PDBarQuotient.baseDerived
theorem OAI.LittleFinitistic.SelectedPDDetection.finite_pd_of_bounded_base_bar line 25
Source documentation
For the fixed actual A and Inflated Y, bounded actual D-bar homology implies finite projective dimension, using the proved global dimension of D.
```
theorem finite_pd_of_bounded_base_bar (Y : FiniteSelectionFamily.S.{0})
    (h : ∃ b : ℕ, ∀ n, b < n → IsZero
      ((DerivedBar.twoSidedComplex ℂ A D (Inflated Y) augmentation).homology n)) :
    projectiveDimension (module Y) < ⊤ :=
…
```
Mentions: OAI.DerivedBar.twoSidedComplex

theorem OAI.LittleFinitistic.SelectedPDDetection.finite_pd_of_base_derived_splitting line 34

Source documentation

Consumer of a supplied actual D-derived bar splitting with bounded target.

theorem finite_pd_of_base_derived_splitting (Y : FiniteSelectionFamily.S.{0})
    (Z : DerivedCategory (ModuleCat.{0} D))
    (e : PDBarQuotient.baseDerived augmentation (Inflated Y) ≅ Z)
    (h : ∃ b : ℕ, ∀ n, b < n → IsZero
      ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj Z)) :
    projectiveDimension (module Y) < ⊤ :=
…

Mentions: OAI.LittleFinitistic.PDBarQuotient.baseDerived

theorem OAI.LittleFinitistic.SelectedPDDetection.finite_pd_of_tensor_bar_splitting line 45

Source documentation

Direct consumer whose source is literally the bar worker's integerQ value.

theorem finite_pd_of_tensor_bar_splitting (Y : FiniteSelectionFamily.S.{0})
    (Z : DerivedCategory (ModuleCat.{0} D))
    (e : (DerivedBar.integerQ D).obj
      (DerivedBar.tensorBarComplex ℂ A D (Inflated Y) augmentation) ≅ Z)
    (h : ∃ b : ℕ, ∀ n, b < n → IsZero
      ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj Z)) :
    projectiveDimension (module Y) < ⊤ :=
…

Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.tensorBarComplex

theorem OAI.LittleFinitistic.SelectedPDDetection.lower_bound_of_tensor_bar_count line 55

Source documentation

The count retract can likewise be supplied at the bar worker's exact source.

theorem lower_bound_of_tensor_bar_count (Y : FiniteSelectionFamily.S.{0}) (r : ℕ)
    (h : ¬ IsZero (SelectedBaseIterates.object Y r))
    (i : SelectedCountCohomology.count Y r ⟶ (DerivedBar.integerQ D).obj
      (DerivedBar.tensorBarComplex ℂ A D (Inflated Y) augmentation))
    (p : (DerivedBar.integerQ D).obj
      (DerivedBar.tensorBarComplex ℂ A D (Inflated Y) augmentation) ⟶ SelectedCountCohomology.count Y r)
    (hip : i ≫ p = 𝟙 _) : r ≤ projectiveDimension (module Y) := by
…

Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object, OAI.LittleFinitistic.SelectedCountCohomology.count, OAI.DerivedBar.integerQ, OAI.DerivedBar.tensorBarComplex