OAI/Algebra/Finitistic/Selected/SelectedCohomologyVanishing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.SelectedCohomologyVanishing.module_isZero line 13

   Source documentation

   The three actual vertex functors jointly detect a zero module.

   theorem module_isZero (M : ModuleCat.{u} (B P))
       (h : ∀ i : Fin 3, IsZero
         ((LeftVertexHomology.vertex k (B P) (ThreeVertexAlgebra.vertex (composition P) i)).obj M)) :
       IsZero M := by
   …

   Mentions: OAI.LittleFinitistic.LeftVertexHomology.vertex, OAI.LittleFinitistic.ThreeVertexAlgebra.vertex

2. theorem OAI.LittleFinitistic.SelectedCohomologyVanishing.cohomology_isZero line 32

   Source documentation

   Vanishing on all three evaluated representatives gives actual cohomology vanishing of the fixed selecting tensor as a B-module.

   theorem cohomology_isZero (n : ℤ)
       (h : ∀ v : Fin 3, IsZero ((SelectedTensor.source N v).homology n)) :
       IsZero ((SelectedTensor.complex N).homology n) := by
   …

   Mentions: OAI.LittleFinitistic.SelectedTensor.source, OAI.LittleFinitistic.SelectedTensor.complex