PDResidueBaseBar.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.PDResidueAssociativity.scalarTensorEquiv line 14

Source documentation

Scalar restriction coherence for an arbitrary right tensor factor.

def scalarTensorEquiv {R : Type u} [Ring R] [Algebra k R]
    (U V : Type u) [AddCommGroup U] [Module k U] [Module Rᵐᵒᵖ U]
    [AddCommGroup V] [Module k V] [Module R V] [IsScalarTower k R V] :
    (PDTensor.tensorFunctor k R U).obj (ModuleCat.of R V) ≃ₗ[k] BalancedTensor.Tensor k R U V :=
…

Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor, OAI.LittleFinitistic.BalancedTensor.Tensor

def OAI.LittleFinitistic.PDResidueAssociativity.objectIso line 28
theorem OAI.LittleFinitistic.PDResidueAssociativity.objectIso_natural line 34
def OAI.LittleFinitistic.PDResidueAssociativity.barIso line 45
def OAI.LittleFinitistic.PDResidueAssociativity.twoSidedIso line 56
def OAI.LittleFinitistic.PDResidueAssociativity.residueTorIso line 67
Source documentation
Actual residue Tor is computed by tensoring the free D-bar with D/rad D. This proves the needed change-of-rings comparison on the actual models.
```
def residueTorIso (n : ℕ) : PDTensor.Tor (k := k) (PDTensor.Residue (A := A)) (ModuleCat.of A N) n ≅
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDResidueAssociativity.twoSided_projective line 75
Source documentation
The actual D-bar has projective terms, even when its length is infinite.
```
theorem twoSided_projective (n : ℕ) : Projective ((DerivedBar.twoSidedComplex k A D N f).X n) := by
…
```
Mentions: OAI.DerivedBar.twoSidedComplex
theorem OAI.LittleFinitistic.PDResidueAssociativity.finite_pd_of_bounded_base_bar line 87
Source documentation
Bounded D-derived bar homology suffices for finite pd over A. The exact-tail theorem supplies the amplitude after residue tensor.
```
theorem finite_pd_of_bounded_base_bar (g : ℕ) (hg : ∀ M : ModuleCat.{u} D, HasProjectiveDimensionLE M g)
    (h : ∃ b : ℕ, ∀ n, b < n → IsZero ((DerivedBar.twoSidedComplex k A D N f).homology n)) :
    projectiveDimension (ModuleCat.of A N) < ⊤ := by
…
```
Mentions: OAI.DerivedBar.twoSidedComplex
theorem OAI.LittleFinitistic.PDResidueAssociativity.finite_pd_of_base_derived_iso line 102