PDDerivedBarConsumer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.PDBar.derivedObject line 15
Source documentation
Actual derived object of a nonnegative chain complex, with degree n sent to -n.
```
abbrev derivedObject (C : ChainComplex (ModuleCat.{u} k) ℕ) :=
…
```
def OAI.LittleFinitistic.PDBar.derivedHomologyIso line 18
theorem OAI.LittleFinitistic.PDBar.finite_pd_of_derived_iso line 28
Source documentation
A supplied actual derived bar comparison and bounded residue cohomology imply finite projective dimension. The comparison is an explicit input.
```
theorem finite_pd_of_derived_iso
    (Z : DerivedCategory (ModuleCat.{u} k))
    (e : derivedObject (tensorComplex M (PDTensor.Residue (A := A)) P) ≅ Z)
…
```
Mentions: OAI.LittleFinitistic.PDBar.derivedObject, OAI.LittleFinitistic.PDBar.tensorComplex, OAI.LittleFinitistic.PDTensor.Residue

theorem OAI.LittleFinitistic.PDBar.lower_bound_of_derived_retract line 45

Source documentation

Nonzero cohomology of a retract of the supplied actual derived bar object provides the lower pd bound. Inclusion and projection retain the summand data.

theorem lower_bound_of_derived_retract
    (Z T : DerivedCategory (ModuleCat.{u} k))
    (e : derivedObject (tensorComplex M U P) ≅ Z)
    (i : T ⟶ Z) (p : Z ⟶ T) (hip : i ≫ p = 𝟙 T)
    (r n : ℕ) (hrn : r ≤ n)
    (h : ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat k) (-(n : ℤ))).obj T)) :
    r ≤ projectiveDimension M.cat := by
…

Mentions: OAI.LittleFinitistic.PDBar.derivedObject, OAI.LittleFinitistic.PDBar.tensorComplex