BimoduleBar.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.BimoduleTensor.freeMap line 19
Source documentation
Balanced tensor on a map of free modules, in the explicit field-tensor coordinates.
```
def freeMap (h : D ⊗[k] V →ₗ[D] D ⊗[k] W) : X ⊗[k] V →ₗ[D] X ⊗[k] W :=
…
```
theorem OAI.DerivedBar.BimoduleTensor.freeMap_descend line 23
Source documentation
Coordinate change commutes with every free-module differential.
```
theorem freeMap_descend (h : D ⊗[k] V →ₗ[D] D ⊗[k] W)
    (z : tensor k D X (D ⊗[k] V)) :
    freeMap k D X V W h (descend k D X V z) =
      descend k D X W (map k D X _ _ h z) := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensor, OAI.DerivedBar.BimoduleTensor.freeMap, OAI.DerivedBar.BimoduleTensor.descend, OAI.DerivedBar.BimoduleTensor.map
theorem OAI.DerivedBar.BimoduleTensor.freeMap_comp line 31
theorem OAI.DerivedBar.BimoduleTensor.freeMap_zero line 42
def OAI.DerivedBar.BimoduleTensor.barDifferential line 51
Source documentation
The two-sided bar differential for arbitrary bimodule coefficients X.
```
def barDifferential (n : ℕ) : X ⊗[k] DerivedBar.term k D N (n+1) →ₗ[D]
    X ⊗[k] DerivedBar.term k D N n :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.BimoduleTensor.barDifferential_tmul line 56
Source documentation
Independent endpoint-minus-tail formula, including the noncommutative right action.
```
theorem barDifferential_tmul (n : ℕ) (x : X) (z : DerivedBar.term k D N (n+1)) :
    barDifferential k D X N n (x ⊗ₜ[k] z) =
      collapse k D X (DerivedBar.term k D N n) (x ⊗ₜ[k] z) -
        x ⊗ₜ[k] DerivedBar.differential k D N n z := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.BimoduleTensor.barDifferential, OAI.DerivedBar.BimoduleTensor.collapse, OAI.DerivedBar.differential
theorem OAI.DerivedBar.BimoduleTensor.barDifferential_sq line 67
def OAI.DerivedBar.BimoduleTensor.tensorResolution line 73
Source documentation
Balanced X tensor of the actual free projective resolution of N.
```
def tensorResolution : ChainComplex (ModuleCat D) ℕ :=
…
```
def OAI.DerivedBar.BimoduleTensor.barComplex line 83
Source documentation
The explicit two-sided X,D,N bar complex, with no D-flatness assumption.
```
def barComplex : ChainComplex (ModuleCat D) ℕ :=
…
```
def OAI.DerivedBar.BimoduleTensor.tensorResolutionIso line 89
Source documentation
The explicit two-sided bar is isomorphic to genuine balanced tensor of the free resolution.
```
def tensorResolutionIso : tensorResolution k D X N ≅ barComplex k D X N :=
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.tensorResolution, OAI.DerivedBar.BimoduleTensor.barComplex