OAI/Algebra/Finitistic/Localization/EvaluationVertexDiagram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.EvaluationVertexDiagram.module line 13
2. def OAI.LittleFinitistic.EvaluationVertexDiagram.equiv line 16

   Source documentation

   The vertex of the actual evaluation module is exactly the original vector space.

   def equiv (i : Fin 3) :
       (LeftVertexHomology.vertex k (B P) (ThreeVertexAlgebra.vertex (composition P) i)).obj (module X) ≃ₗ[k] Y where
   …

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

3. def OAI.LittleFinitistic.EvaluationVertexDiagram.vertexIso line 35
4. def OAI.LittleFinitistic.EvaluationVertexDiagram.action line 37
5. theorem OAI.LittleFinitistic.EvaluationVertexDiagram.arrow01_square line 41

   Source documentation

   The first arrow family acts by the given representation, including the identity arrow.

   theorem arrow01_square (a : Fin (d+1))
       (ha : ThreeVertexAlgebra.vertex (composition P) 1 * arrow01 P a = arrow01 P a) :
       (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 0)
         (ThreeVertexAlgebra.vertex (composition P) 1) (arrow01 P a) ha).app (module X) ≫
         (vertexIso X 1).hom = (vertexIso X 0).hom ≫ action X a := by
   …

   Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.EvaluationVertexDiagram.module, OAI.LittleFinitistic.EvaluationVertexDiagram.vertexIso, OAI.LittleFinitistic.EvaluationVertexDiagram.action

6. theorem OAI.LittleFinitistic.EvaluationVertexDiagram.arrow12_square line 54

   Source documentation

   The second arrow family has the same specified representation action.

   theorem arrow12_square (b : Fin (d+1))
       (hb : ThreeVertexAlgebra.vertex (composition P) 2 * arrow12 P b = arrow12 P b) :
       (LeftVertexHomology.arrow k (B P) (ThreeVertexAlgebra.vertex (composition P) 1)
         (ThreeVertexAlgebra.vertex (composition P) 2) (arrow12 P b) hb).app (module X) ≫
         (vertexIso X 2).hom = (vertexIso X 1).hom ≫ action X b := by
   …

   Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.LeftVertexHomology.arrow, OAI.LittleFinitistic.EvaluationVertexDiagram.module, OAI.LittleFinitistic.EvaluationVertexDiagram.vertexIso, OAI.LittleFinitistic.EvaluationVertexDiagram.action