BarCoordinateNaturality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.Multibar.freeBarObjIso_d line 16
Source documentation
The categorical free-bar differential is the supplied-scalars literal one.
```
theorem freeBarObjIso_d (n : ℕ) :
    ((barFunctor k D).obj (ModuleCat.of D V)).d (n+1) n ≫
      (freeBarObjIso k D V n).hom =
    (freeBarObjIso k D V (n+1)).hom ≫
      ModuleCat.ofHom (DerivedBar.differential k D V (n+1)) := by
…
```
Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.Multibar.freeBarObjIso, OAI.DerivedBar.differential
theorem OAI.DerivedBar.Multibar.twoSidedBarObjIso_d line 27
Source documentation
The X-bar differential retains the original noncommutative bimodule actions.
```
theorem twoSidedBarObjIso_d (n : ℕ) :
    ((BimoduleTensor.twoSidedBarFunctor k D X).obj (ModuleCat.of D V)).d (n+1) n ≫
      (twoSidedBarObjIso k D X V n).hom =
    (twoSidedBarObjIso k D X V (n+1)).hom ≫
      ModuleCat.ofHom (BimoduleTensor.barDifferential k D X V n) := by
…
```
Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor, OAI.DerivedBar.Multibar.twoSidedBarObjIso, OAI.DerivedBar.BimoduleTensor.barDifferential
theorem OAI.DerivedBar.Multibar.freeBarObjIso_map line 38
Source documentation
Scalar coherence is natural for every D-linear map of input modules.
```
theorem freeBarObjIso_map (f : V →ₗ[D] W) (n : ℕ) :
    ((barFunctor k D).map (ModuleCat.ofHom f)).f n ≫ (freeBarObjIso k D W n).hom =
    (freeBarObjIso k D V n).hom ≫ ModuleCat.ofHom (termMap k D V W f (n+1)) := by
…
```
Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.Multibar.freeBarObjIso, OAI.DerivedBar.termMap

theorem OAI.DerivedBar.Multibar.twoSidedBarObjIso_map line 48

Source documentation

All vertical maps of the categorical X bar become literal tensor maps.

theorem twoSidedBarObjIso_map (f : V →ₗ[D] W) (n : ℕ) :
    ((BimoduleTensor.twoSidedBarFunctor k D X).map (ModuleCat.ofHom f)).f n ≫
      (twoSidedBarObjIso k D X W n).hom =
    (twoSidedBarObjIso k D X V n).hom ≫ ModuleCat.ofHom
      (AlgebraTensorModule.lTensor D X ((termMap k D V W f n).restrictScalars k)) := by
…

Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor, OAI.DerivedBar.Multibar.twoSidedBarObjIso, OAI.DerivedBar.termMap