TensorComplex.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.TensorComplex.ScalarModule line 14
instance OAI.LittleFinitistic.TensorComplex.scalarTower line 17
def OAI.LittleFinitistic.TensorComplex.mapRight line 25
Source documentation
The actual tensor differential, with the original right B-action.
```
def mapRight (M : ModuleCat.{u} k) {N N' : ModuleCat.{u} Bᵐᵒᵖ} (g : N ⟶ N') :
    (M ⊗[k] ScalarModule k B N) →ₗ[Bᵐᵒᵖ] (M ⊗[k] ScalarModule k B N') where
…
```
Mentions: OAI.LittleFinitistic.TensorComplex.ScalarModule
theorem OAI.LittleFinitistic.TensorComplex.mapRight_tmul line 36
def OAI.LittleFinitistic.TensorComplex.complex line 42
Source documentation
Tensor a vector space with every term and differential of the given right-module complex.
```
def complex (M : ModuleCat.{u} k) : CochainComplex (ModuleCat.{u} Bᵐᵒᵖ) ℤ where
…
```
def OAI.LittleFinitistic.TensorComplex.complexMap line 71
Source documentation
The first-factor tensor map is a chain map.
```
def complexMap {M M' : ModuleCat.{u} k} (f : M ⟶ M') : complex D M ⟶ complex D M' where
…
```
Mentions: OAI.LittleFinitistic.TensorComplex.complex
def OAI.LittleFinitistic.TensorComplex.tensorFunctor line 84
Source documentation
The genuine additive tensor-with-D functor required by the path exact sequence.
```
def tensorFunctor : ModuleCat.{u} k ⥤ CochainComplex (ModuleCat.{u} Bᵐᵒᵖ) ℤ where
…
```
instance OAI.LittleFinitistic.TensorComplex.tensorFunctor_additive line 108
theorem OAI.LittleFinitistic.TensorComplex.adjacent_total_acyclic line 129
Source documentation
The adjacent-vertex graded piece is the cone of the path-space identity.
```
theorem adjacent_total_acyclic (M : ModuleCat.{u} k) :
    (CochainComplex.mappingCone (𝟙 (complex D M))).Acyclic :=
…
```
Mentions: OAI.LittleFinitistic.TensorComplex.complex
theorem OAI.LittleFinitistic.TensorComplex.relation_total_acyclic line 134
Source documentation
The source-0 path-relation graded piece is acyclic for the actual tensor functor.
```
theorem relation_total_acyclic {d t : ℕ} (P : QuadraticEncoding.Relations k d t) :
    (RectificationTotal.total ((RelationSequence.sequence P).map (tensorFunctor (k := k) D)).g
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations, OAI.LittleFinitistic.RectificationTotal.total, OAI.LittleFinitistic.RelationSequence.sequence, OAI.LittleFinitistic.TensorComplex.tensorFunctor