TensorCohomologyDiagram.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.TensorCohomologyDiagram.comparison line 17
Source documentation
From cohomology of an evaluated representative to the actual vertex of cohomology of the full B-module tensor complex.
```
def comparison (v : Fin 3) (n : ℤ) : (source P D₀ D₁ D₂ N v).homology n ⟶
    (LeftVertexHomology.vertex k (B P) (ThreeVertexAlgebra.vertex (composition P) v)).obj
      ((tensor P D₀ D₁ D₂ f g H N).homology n) :=
…
```
Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex

theorem OAI.LittleFinitistic.TensorCohomologyDiagram.comparison_isIso line 26

Source documentation

The canonical cohomology comparison is invertible under the proved input hypotheses.

theorem comparison_isIso (v : Fin 3) (n 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)) :
    IsIso (comparison P D₀ D₁ D₂ f g H N v n) := by
…

Mentions: OAI.LittleFinitistic.TensorCohomologyDiagram.comparison

theorem OAI.LittleFinitistic.TensorCohomologyDiagram.arrow01_square line 43

Source documentation

The first-family cohomology square retains the full original arrow action.

theorem arrow01_square (a : Fin (d+1)) (n : ℤ) :
    homologyMap (((BalancedTensor.tensorFunctor k (B P) N).mapHomologicalComplex (.up ℤ)).map (f a)) n ≫
      comparison P D₀ D₁ D₂ f g H N 1 n =
    comparison P D₀ D₁ D₂ f g H N 0 n ≫
      (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 0)
        (ThreeVertexAlgebra.vertex (composition P) 1) (arrow01 P a)
        (CanonicalArrowCompatibility.arrow01_target P a)).app
          ((tensor P D₀ D₁ D₂ f g H N).homology n) := by
…

Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.TensorCohomologyDiagram.comparison, OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.CanonicalArrowCompatibility.arrow01_target

theorem OAI.LittleFinitistic.TensorCohomologyDiagram.arrow12_square line 62

Source documentation

The second-family cohomology square retains the full original arrow action.

theorem arrow12_square (b : Fin (d+1)) (n : ℤ) :
    homologyMap (((BalancedTensor.tensorFunctor k (B P) N).mapHomologicalComplex (.up ℤ)).map (g b)) n ≫
      comparison P D₀ D₁ D₂ f g H N 2 n =
    comparison P D₀ D₁ D₂ f g H N 1 n ≫
      (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 1)
        (ThreeVertexAlgebra.vertex (composition P) 2) (arrow12 P b)
        (CanonicalArrowCompatibility.arrow12_target P b)).app
          ((tensor P D₀ D₁ D₂ f g H N).homology n) := by
…