PDTor.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.PDTensor.Tor line 14
Source documentation
Tor is the left derived functor of the actual balanced tensor functor.
```
abbrev Tor (M : ModuleCat.{u} A) (n : ℕ) : ModuleCat.{u} k :=
…
```
def OAI.LittleFinitistic.PDTensor.model line 19
def OAI.LittleFinitistic.PDTensor.torIsoModel line 23
Source documentation
The chosen minimal resolution computes this actual derived functor.
```
def torIsoModel (n : ℕ) : Tor (k := k) U M.cat n ≅ (model U M).homology n :=
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.model
theorem OAI.LittleFinitistic.PDTensor.model_d_zero line 30
Source documentation
Minimality annihilates every tensor differential, including non-adjacent ones.
```
theorem model_d_zero (i j : ℕ) : (model U M).d i j = 0 := by
…
```
Mentions: OAI.LittleFinitistic.PDTensor.model
def OAI.LittleFinitistic.PDTensor.torIsoTerm line 47
Source documentation
Homology of the tensor of a minimal resolution is its term, because all its differentials have been proved zero.
```
def torIsoTerm (n : ℕ) : Tor (k := k) U M.cat n ≅
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor