OAI/Algebra/Finitistic/Selected/SelectedVertexTensorEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.QuadraticEncoding.vertexModule line 13

   Source documentation

   The manuscript's actual right vertex projectives.

   def vertexModule (i : Fin 3) : ModuleCat.{u} (B P)ᵐᵒᵖ :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.B

2. def OAI.LittleFinitistic.QuadraticEncoding.arrowModule01 line 16
3. def OAI.LittleFinitistic.QuadraticEncoding.arrowModule12 line 18
4. def OAI.LittleFinitistic.QuadraticEncoding.evaluationVertexEquiv line 24

   Source documentation

   The natural identifications for the actual tensor functor.

   def evaluationVertexEquiv (i : Fin 3) :
       (tensorFunctor k (B P) X.Evaluation).obj (vertexModule P i) ≃ₗ[k] Y :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.QuadraticEncoding.vertexModule

5. theorem OAI.LittleFinitistic.QuadraticEncoding.evaluation_arrow01 line 28
6. theorem OAI.LittleFinitistic.QuadraticEncoding.evaluation_arrow12 line 38
7. theorem OAI.LittleFinitistic.QuadraticEncoding.evaluation_s_isIso line 49

   Source documentation

   Tensor evaluation sends s to an actual isomorphism, conjugate to id_Y.

   theorem evaluation_s_isIso : IsIso ((tensorFunctor k (B P) X.Evaluation).map (arrowModule01 P 0)) := by
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.QuadraticEncoding.arrowModule01

8. theorem OAI.LittleFinitistic.QuadraticEncoding.evaluation_s'_isIso line 59