OAI/Algebra/Finitistic/Selected/SelectedReferenceCohomology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.SelectedReferenceCohomology.transfer_to_vertices line 10
2. def OAI.LittleFinitistic.SelectedReferenceCohomology.iso line 28

   Source documentation

   Identify the full tensor cohomology with the actual evaluation module from three coordinate models and their generator actions.

   def iso
       (h01 : ∀ a,
         homologyMap (((BalancedTensor.tensorFunctor ℂ (B P) N).mapHomologicalComplex (.up ℤ)).map (f a)) n ≫
           (E 1).hom = (E 0).hom ≫ EvaluationVertexDiagram.action X a)
       (h12 : ∀ b,
         homologyMap (((BalancedTensor.tensorFunctor ℂ (B P) N).mapHomologicalComplex (.up ℤ)).map (g b)) n ≫
           (E 2).hom = (E 1).hom ≫ EvaluationVertexDiagram.action X b) :
       (SelectedTensor.complex N).homology n ≅ EvaluationVertexDiagram.module X := by
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.tensorFunctor, OAI.LittleFinitistic.EvaluationVertexDiagram.action, OAI.LittleFinitistic.SelectedTensor.complex, OAI.LittleFinitistic.EvaluationVertexDiagram.module