BimoduleComparison.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.BimoduleTensor.scalarModule_eq line 15
Source documentation
Canonical scalar restriction agrees with every supplied compatible field action.
```
theorem scalarModule_eq (V : Type u) [AddCommGroup V] [Module k V]
    [Module D V] [IsScalarTower k D V] :
    scalarModule k D (ModuleCat.of D V) = (inferInstance : Module k V) := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.scalarModule
def OAI.DerivedBar.BimoduleTensor.tensorFunctorObjIso line 23
Source documentation
Coherence between the categorical tensor functor and the literal balancing quotient.
```
def tensorFunctorObjIso (V : Type u) [AddCommGroup V] [Module k V]
    [Module D V] [IsScalarTower k D V] :
    (tensorFunctor k D X).obj (ModuleCat.of D V) ≅ ModuleCat.of D (tensor k D X V) := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.tensor

theorem OAI.DerivedBar.BimoduleTensor.tensorFunctorObjIso_natural line 32

Source documentation

The scalar-action coherence is natural for every D-linear map.

theorem tensorFunctorObjIso_natural (V W : Type u)
    [AddCommGroup V] [Module k V] [Module D V] [IsScalarTower k D V]
    [AddCommGroup W] [Module k W] [Module D W] [IsScalarTower k D W]
    (h : V →ₗ[D] W) :
    (tensorFunctor k D X).map (ModuleCat.ofHom h) ≫ (tensorFunctorObjIso k D X W).hom =
      (tensorFunctorObjIso k D X V).hom ≫ ModuleCat.ofHom (map k D X V W h) := by
…

Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.map, OAI.DerivedBar.BimoduleTensor.tensorFunctorObjIso

def OAI.DerivedBar.BimoduleTensor.resolvedTensorIso line 49
Source documentation
The categorical derived-resolution model and the explicit balanced bar complex agree.
```
def resolvedTensorIso (N : ModuleCat.{u} D) :
    resolvedTensor k D X N ≅ tensorResolution k D X N :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.resolvedTensor, OAI.DerivedBar.BimoduleTensor.tensorResolution
def OAI.DerivedBar.BimoduleTensor.explicitBarComputesDerivedTensor line 63
Source documentation
The literal arbitrary-bimodule two-sided bar computes genuine derived tensor of a module. There is no flatness assumption or ordinary tensor-power replacement.
```
def explicitBarComputesDerivedTensor (N : ModuleCat.{u} D) :
    (tensorFunctor k D X).leftDerivedToHomotopyCategory.obj N ≅
      (HomotopyCategory.quotient (ModuleCat.{u} D) (ComplexShape.down ℕ)).obj
        (barComplex k D X N) :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.barComplex
def OAI.DerivedBar.BimoduleTensor.barHomologyIso line 72
Source documentation
Actual left-derived tensor homology (Tor), computed by the explicit two-sided bar.
```
def barHomologyIso (N : ModuleCat.{u} D) (i : ℕ) :
    ((tensorFunctor k D X).leftDerived i).obj N ≅
      (HomologicalComplex.homologyFunctor (ModuleCat.{u} D) (ComplexShape.down ℕ) i).obj
        (barComplex k D X N) :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.barComplex