TwoSidedBarFunctor.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.BimoduleTensor.freeBarTensorIso line 19
Source documentation
The component comparison to the explicit two-sided bar.
```
def freeBarTensorIso (N : ModuleCat.{u} D) :
    ((barFunctor k D ⋙ (tensorFunctor k D X).mapHomologicalComplex c).obj N) ≅
      barComplex k D X N :=
…
```
Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.barComplex
def OAI.DerivedBar.BimoduleTensor.barTermMap line 25
Source documentation
The map on the explicit field-tensor bar terms.
```
def barTermMap {V W : ModuleCat.{u} D} (f : V ⟶ W) (n : ℕ) :
    X ⊗[k] term k D V n →ₗ[D] X ⊗[k] term k D W n :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.BimoduleTensor.freeMap_termMap line 29
theorem OAI.DerivedBar.BimoduleTensor.barDifferential_natural line 39
def OAI.DerivedBar.BimoduleTensor.twoSidedBarMap line 47
Source documentation
The two-sided bar map is defined on literal tensor coordinates.
```
def twoSidedBarMap {V W : ModuleCat.{u} D} (f : V ⟶ W) :
    barComplex k D X V ⟶ barComplex k D X W where
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.barComplex
def OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor line 58
Source documentation
A functor with both maps and differential defined on the explicit bar tensors.
```
def twoSidedBarFunctor : ModuleCat.{u} D ⥤ ChainComplex (ModuleCat.{u} D) ℕ where
…
```
instance OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor_preservesZero line 79
def OAI.DerivedBar.BimoduleTensor.freeBarTensorNatIso line 90
Source documentation
Natural comparison, preserving the exterior D-action.
```
def freeBarTensorNatIso :
    barFunctor k D ⋙ (tensorFunctor k D X).mapHomologicalComplex c ≅
      twoSidedBarFunctor k D X :=
…
```
Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.BimoduleTensor.tensorFunctor, OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor
def OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex line 113
Source documentation
The literal two-sided bar bicomplex of an arbitrary nonnegative chain input.
```
def twoSidedBarBicomplex (Z : ChainComplex (ModuleCat.{u} D) ℕ) :
    HomologicalComplex₂ (ModuleCat.{u} D) c c :=
…
```
theorem OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex_d₁ line 118
Source documentation
Horizontal differential is the explicit two-sided bar, without count transport.
```
theorem twoSidedBarBicomplex_d₁ (Z : ChainComplex (ModuleCat.{u} D) ℕ) (i q : ℕ) :
    ((twoSidedBarBicomplex k D X Z).d (i+1) i).f q =
      ModuleCat.ofHom (barDifferential k D X (Z.X q) i) := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarBicomplex, OAI.DerivedBar.BimoduleTensor.barDifferential