TotalBarComparison.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.BimoduleTensor.tensorBarBicomplexIso line 20
Source documentation
The termwise balanced/free comparison is an isomorphism of bicomplexes.
```
def tensorBarBicomplexIso (Z : ChainComplex (ModuleCat.{u} D) ℕ) :
    mapBicomplex (tensorFunctor k D X) (barBicomplex k D Z) ≅
      twoSidedBarBicomplex k D X Z :=
…
```
Mentions: OAI.DerivedBar.mapBicomplex, OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.barBicomplex, OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex
def OAI.DerivedBar.BimoduleTensor.explicitBarTotal line 27
Source documentation
The explicit two-sided total bar on a nonnegative chain complex.
```
def explicitBarTotal (Z : ChainComplex (ModuleCat.{u} D) ℕ) :
    ChainComplex (ModuleCat.{u} D) ℕ :=
…
```
def OAI.DerivedBar.BimoduleTensor.tensorTotalExplicitIso line 33
Source documentation
Resolving the whole input and applying balanced tensor gives precisely the explicit two-sided bar total. Finite diagonal sums suffice; X need not be flat.
```
def tensorTotalExplicitIso (Z : ChainComplex (ModuleCat.{u} D) ℕ) :
    (tensorTotalFunctor k D X).obj Z ≅ explicitBarTotal k D X Z :=
…
```
Mentions: OAI.DerivedBar.tensorTotalFunctor, OAI.DerivedBar.BimoduleTensor.explicitBarTotal

theorem OAI.DerivedBar.BimoduleTensor.explicitBar_horizontal line 39

Source documentation

Actual horizontal endpoint-minus-tail face in the explicit bicomplex.

theorem explicitBar_horizontal (Z : ChainComplex (ModuleCat.{u} D) ℕ)
    (i q : ℕ) (x : X) (z : term k D (Z.X q) (i+1)) :
    (((twoSidedBarBicomplex k D X Z).d (i+1) i).f q).hom (x ⊗ₜ[k] z) =
      collapse k D X (term k D (Z.X q) i) (x ⊗ₜ[k] z) -
        x ⊗ₜ[k] differential k D (Z.X q) i z := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex, OAI.DerivedBar.BimoduleTensor.collapse, OAI.DerivedBar.differential

theorem OAI.DerivedBar.BimoduleTensor.explicitBar_vertical line 48
Source documentation
Actual vertical differential applies the input differential to the last factor.
```
theorem explicitBar_vertical (Z : ChainComplex (ModuleCat.{u} D) ℕ)
    (i q q' : ℕ) :
    ((twoSidedBarBicomplex k D X Z).X i).d q q' =
      ModuleCat.ofHom (barTermMap k D X (Z.d q q') i) := rfl
```
Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex, OAI.DerivedBar.BimoduleTensor.barTermMap

theorem OAI.DerivedBar.BimoduleTensor.explicitBarTotal_d₁_succ line 54

Source documentation

Horizontal differential in the explicit total.

theorem explicitBarTotal_d₁_succ (Z : ChainComplex (ModuleCat.{u} D) ℕ)
    (i q n : ℕ) (h : i+q=n) :
    (twoSidedBarBicomplex k D X Z).d₁ c (i+1) q n =
      ModuleCat.ofHom (barDifferential k D X (Z.X q) i) ≫
        (twoSidedBarBicomplex k D X Z).ιTotal c i q n h := by
…

Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex, OAI.DerivedBar.BimoduleTensor.barDifferential

theorem OAI.DerivedBar.BimoduleTensor.explicitBarTotal_d₂_succ line 65

Source documentation

Standard vertical totalization sign, independent of the count differential.

theorem explicitBarTotal_d₂_succ (Z : ChainComplex (ModuleCat.{u} D) ℕ)
    (i q n : ℕ) (h : i+q=n) :
    (twoSidedBarBicomplex k D X Z).d₂ c i (q+1) n =
      ((-1 : ℤˣ)^i) • (ModuleCat.ofHom (barTermMap k D X (Z.d (q+1) q) i) ≫
        (twoSidedBarBicomplex k D X Z).ιTotal c i q n h) := by
…

Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex, OAI.DerivedBar.BimoduleTensor.barTermMap

theorem OAI.DerivedBar.BimoduleTensor.explicitBarTotal_d₁_zero line 73
theorem OAI.DerivedBar.BimoduleTensor.explicitBarTotal_d₂_zero line 78