OAI/Algebra/Finitistic/Localization/FiniteEvaluationTarget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.QuadraticEncoding.FiniteVectorHomotopy line 14

   Source documentation

   The concrete bounded homotopy category of finite-dimensional vector spaces.

   abbrev FiniteVectorHomotopy := K.{u,max u v} k

2. theorem OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluation_property line 16
3. def OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluation line 23

   Source documentation

   Evaluation with bounded finite-dimensional vector-space complexes as its actual target.

   def finiteEvaluation : BoundedK P ⥤ FiniteVectorHomotopy.{u,v} (k := k) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedK

4. instance OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluationAdditive line 26
5. instance OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluationShift line 29
6. instance OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluationTriangulated line 32
7. lemma OAI.LittleFinitistic.QuadraticEncoding.finiteEvaluation_kills_generators line 36
8. def OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluation line 43

   Source documentation

   The fixed quotient Q evaluates directly into bounded finite-dimensional complexes.

   def finiteQuotientEvaluation : BoundedQ P ⥤ FiniteVectorHomotopy.{u,v} (k := k) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedQ

9. def OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluationFactors line 47