FullTensorRectification.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.FullTensorRectification.tensor line 17
Source documentation
The actual left B-module complex P tensor_B N.
```
abbrev tensor := ((BimoduleBalancedTensor.functor k (B P) N).mapHomologicalComplex (.up ℤ)).obj
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor
abbrev OAI.LittleFinitistic.FullTensorRectification.source line 20
abbrev OAI.LittleFinitistic.FullTensorRectification.target line 23
def OAI.LittleFinitistic.FullTensorRectification.iota line 28
Source documentation
The original vertex insertion after balanced tensoring and the canonical comparison.
```
def iota (v : Fin 3) : source P D₀ D₁ D₂ N v ⟶ target P D₀ D₁ D₂ f g H N v :=
…
```
Mentions: OAI.LittleFinitistic.FullTensorRectification.source, OAI.LittleFinitistic.FullTensorRectification.target

theorem OAI.LittleFinitistic.FullTensorRectification.equivalence line 36

Source documentation

The equivalences retain the full left B-valued tensor target and the exact original maps.

theorem equivalence (v : Fin 3) (lo hi : ℤ)
    (b₀ : ∀ n, n < lo ∨ hi < n → IsZero (D₀.X n))
    (b₁ : ∀ n, n < lo ∨ hi < n → IsZero (D₁.X n))
    (b₂ : ∀ n, n < lo ∨ hi < n → IsZero (D₂.X n))
    (p₀ : ∀ n, Module.Projective (B P)ᵐᵒᵖ (D₀.X n))
    (p₁ : ∀ n, Module.Projective (B P)ᵐᵒᵖ (D₁.X n))
    (p₂ : ∀ n, Module.Projective (B P)ᵐᵒᵖ (D₂.X n)) :
    ∃ E : HomotopyEquiv (source P D₀ D₁ D₂ N v) (target P D₀ D₁ D₂ f g H N v),
      E.hom = iota P D₀ D₁ D₂ f g H N v := by
…

Mentions: OAI.LittleFinitistic.FullTensorRectification.source, OAI.LittleFinitistic.FullTensorRectification.target, OAI.LittleFinitistic.FullTensorRectification.iota

abbrev OAI.LittleFinitistic.FullTensorRectification.arrow01Map line 56
abbrev OAI.LittleFinitistic.FullTensorRectification.arrow12Map line 61
lemma OAI.LittleFinitistic.FullTensorRectification.original_iota0 line 67
lemma OAI.LittleFinitistic.FullTensorRectification.original_iota1 line 69
lemma OAI.LittleFinitistic.FullTensorRectification.original_iota2 line 71
def OAI.LittleFinitistic.FullTensorRectification.compatibility01 line 75
Source documentation
Actual arrow compatibility on the vertex diagram of the full B-valued tensor.
```
def compatibility01 (a : Fin (d+1)) : Homotopy
    (iota P D₀ D₁ D₂ f g H N 0 ≫ arrow01Map P D₀ D₁ D₂ f g H N a)
    (((BalancedTensor.tensorFunctor k (B P) N).mapHomologicalComplex (.up ℤ)).map (f a) ≫
      iota P D₀ D₁ D₂ f g H N 1) := by
…
```
Mentions: OAI.LittleFinitistic.FullTensorRectification.iota, OAI.LittleFinitistic.FullTensorRectification.arrow01Map, OAI.LittleFinitistic.BalancedTensor.tensorFunctor
def OAI.LittleFinitistic.FullTensorRectification.compatibility12 line 99
Source documentation
The second arrow family retains its original maps as well.
```
def compatibility12 (b : Fin (d+1)) : Homotopy
    (iota P D₀ D₁ D₂ f g H N 1 ≫ arrow12Map P D₀ D₁ D₂ f g H N b)
    (((BalancedTensor.tensorFunctor k (B P) N).mapHomologicalComplex (.up ℤ)).map (g b) ≫
      iota P D₀ D₁ D₂ f g H N 2) := by
…
```
Mentions: OAI.LittleFinitistic.FullTensorRectification.iota, OAI.LittleFinitistic.FullTensorRectification.arrow12Map, OAI.LittleFinitistic.BalancedTensor.tensorFunctor