OAI/Algebra/Finitistic/Localization/HomotopyVertexEvaluation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.QuadraticEncoding.liftedY line 13
2. def OAI.LittleFinitistic.QuadraticEncoding.liftedVertexEquiv line 15
3. def OAI.LittleFinitistic.QuadraticEncoding.actionArrow line 19
4. lemma OAI.LittleFinitistic.QuadraticEncoding.tensor_arrow01_square line 24
5. lemma OAI.LittleFinitistic.QuadraticEncoding.tensor_arrow12_square line 32
6. abbrev OAI.LittleFinitistic.QuadraticEncoding.vectorStalk line 40
7. def OAI.LittleFinitistic.QuadraticEncoding.homotopyVertexIso line 43

   Source documentation

   Evaluation of each concrete degree-zero vertex object is the stalk complex Y.

   def homotopyVertexIso (i : Fin 3) :
       (boundedEvaluation X).obj (vertexK P i) ≅ (vectorStalk (k := k)).obj (ModuleCat.of k (ULift.{u} Y)) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.vertexK, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk

8. lemma OAI.LittleFinitistic.QuadraticEncoding.homotopy_arrow01_square line 50
9. lemma OAI.LittleFinitistic.QuadraticEncoding.homotopy_arrow12_square line 86