BimoduleSingleEvaluation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.evaluationAtIndex_transport line 15
theorem OAI.LittleFinitistic.BimoduleTotal.evaluationTermIso_at line 22
def OAI.LittleFinitistic.BimoduleTotal.singleEvaluationIso line 32
Source documentation
The ordinary signed total on an input module in degree zero is the exact native P tensor_B N complex.
```
def singleEvaluationIso : total k B P p hp (singleInput B N) ≅ moduleEvaluation k B P N :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation
def OAI.LittleFinitistic.BimoduleTotal.derivedSingleEvaluation line 50
Source documentation
Evaluation of the actual derived endofunctor on a degree-zero module is the native tensor complex in D(B-Mod).
```
def derivedSingleEvaluation :
    (derived k B P p hp).obj (DerivedCategory.Q.obj (singleInput B N)) ≅
      DerivedCategory.Q.obj (moduleEvaluation k B P N) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.derived, OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation