TensorModel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.freeEquiv_natural line 15

Source documentation

The balanced free-tensor equivalence respects arbitrary A-linear maps, including bar faces.

theorem freeEquiv_natural (V W : Type u) [AddCommGroup V] [Module k V]
    [AddCommGroup W] [Module k W] (h : A ⊗[k] V →ₗ[A] A ⊗[k] W) :
    (Balanced.descend f W).comp (Balanced.map f (A ⊗[k] V) (A ⊗[k] W) h) =
      (FreeBaseChange.map f V W h).comp (Balanced.descend f V) := by
…

Mentions: OAI.DerivedBar.Balanced.descend, OAI.DerivedBar.Balanced.map, OAI.DerivedBar.FreeBaseChange.map

def OAI.DerivedBar.tensorBarComplex line 31
Source documentation
The actual balanced tensor of D with every term and differential of the verified bar resolution.
```
def tensorBarComplex : ChainComplex (ModuleCat D) ℕ :=
…
```
def OAI.DerivedBar.tensorBarIso line 41
Source documentation
The explicit two-sided bar is isomorphic to balanced tensor applied to a genuine projective resolution.
```
def tensorBarIso : tensorBarComplex k A D N f ≅ twoSidedComplex k A D N f :=
…
```
Mentions: OAI.DerivedBar.tensorBarComplex, OAI.DerivedBar.twoSidedComplex
def OAI.DerivedBar.SquareZero.tensorCountSplitting line 63
Source documentation
The tensor of the actual free resolution splits by X-count as a D-module chain complex. The identification of count r with the shifted r-fold derived tensor remains separate.
```
def tensorCountSplitting
    (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = 0) :
    tensorBarComplex k (TrivSqZeroExt D X) D N (fstHom k D X) ≅
      directSumComplex (twoSidedWeightComplex k D X N hN) :=
…
```
Mentions: OAI.DerivedBar.tensorBarComplex, OAI.DerivedBar.directSumComplex, OAI.DerivedBar.SquareZero.twoSidedWeightComplex