OAI/Algebra/Finitistic/Localization/BoundedQuotientEvaluation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.FiniteProjectiveHomotopy.single_property line 16
2. instance OAI.LittleFinitistic.QuadraticEncoding.vertexModuleFinite line 32
3. instance OAI.LittleFinitistic.QuadraticEncoding.vertexModuleProjective line 39
4. abbrev OAI.LittleFinitistic.QuadraticEncoding.BoundedK line 45

   Source documentation

   The exact bounded-projective source category used in Section 3.

   abbrev BoundedK := K.{u,u} (B P)ᵐᵒᵖ

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.B

5. def OAI.LittleFinitistic.QuadraticEncoding.boundedConeS line 47
6. def OAI.LittleFinitistic.QuadraticEncoding.boundedConeS' line 49
7. def OAI.LittleFinitistic.QuadraticEncoding.boundedConeGenerators line 52
8. abbrev OAI.LittleFinitistic.QuadraticEncoding.boundedDenominators line 55
9. abbrev OAI.LittleFinitistic.QuadraticEncoding.BoundedQ line 59

   Source documentation

   The actual localization of K^b(proj-B) by the thick subcategory generated by the two cones.

   abbrev BoundedQ := (boundedDenominators P).Localization
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.boundedDenominators

10. def OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluation line 63
11. instance OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluationAdditive line 66
12. instance OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluationShift line 68
13. instance OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluationTriangulated line 70
14. lemma OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluation_kills_generators line 73
15. def OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluation line 80

    Source documentation

    Tensor evaluation on the manuscript's fixed quotient; no generator-vanishing assumption remains.

    def boundedQuotientEvaluation : BoundedQ P ⥤ HomotopyCategory (ModuleCat.{max u v} k) (.up ℤ) :=
    …

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedQ

16. def OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluationFactors line 84
17. theorem OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluation_finite line 90

    Source documentation

    Evaluation of every bounded-projective representative has bounded finite-dimensional terms.

    theorem boundedEvaluation_finite [FiniteDimensional k Y] (T : BoundedK P) :
        (∃ a b : ℤ, ∀ i, i < a ∨ b < i → IsZero (((boundedEvaluation X).obj T).as.X i)) ∧
        ∀ i, FiniteDimensional k (((boundedEvaluation X).obj T).as.X i) := by
    …

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedK, OAI.LittleFinitistic.QuadraticEncoding.boundedEvaluation