BimoduleDerived.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.BimoduleTensor.scalarModule line 15
Source documentation
The canonical field action on a left D-module.
```
@[instance_reducible] def scalarModule (V : ModuleCat.{u} D) : Module k V := Module.compHom V (algebraMap k D)
…
```
def OAI.DerivedBar.BimoduleTensor.tensorFunctor line 22
Source documentation
Actual balanced tensor by the arbitrary bimodule X, as an additive endofunctor.
```
def tensorFunctor : ModuleCat.{u} D ⥤ ModuleCat.{u} D where
…
```
instance OAI.DerivedBar.BimoduleTensor.tensorFunctor_additive line 28
def OAI.DerivedBar.BimoduleTensor.resolvedTensor line 35
Source documentation
Tensor of X with the verified absolute bar projective resolution. This construction applies the genuine balanced functor to every differential.
```
def resolvedTensor (N : ModuleCat.{u} D) : ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
def OAI.DerivedBar.BimoduleTensor.barComputesDerivedTensor line 42
Source documentation
The explicit projective bar resolution computes actual derived tensor on modules, via mathlib's left derived functor to the homotopy category. Extension to bounded-above complexes and repeated totalization remains separate.
```
def barComputesDerivedTensor (N : ModuleCat.{u} D) :
    (tensorFunctor k D X).leftDerivedToHomotopyCategory.obj N ≅
      (HomotopyCategory.quotient (ModuleCat.{u} D) (ComplexShape.down ℕ)).obj
        (resolvedTensor k D X N) :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.resolvedTensor