OAI/Algebra/Finitistic/Localization/CompletedDerivedEvaluation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.LittleFinitistic.QuadraticEncoding.karoubiExtensionAdditive line 15
  2. instance OAI.LittleFinitistic.QuadraticEncoding.completedExtensionAdditive line 23
  3. def OAI.LittleFinitistic.QuadraticEncoding.completedExtensionFactors line 27

    Source documentation

    The extension restricts to the original functor under the canonical embedding.

    def completedExtensionFactors :
    toKaroubi C ⋙ (functorExtension C D).obj F ≅ F :=
…
  4. def OAI.LittleFinitistic.QuadraticEncoding.completedExtensionImageIso line 37

    Source documentation

    An explicitly split evaluated idempotent identifies the value of the completion.

    def completedExtensionImageIso (U : Karoubi C) (I : D)
    (π : F.obj U.X ⟶ I) (ι : I ⟶ F.obj U.X)
    (hπι : π ≫ ι = F.map U.p) (hιπ : ι ≫ π = 𝟙 I) :
    ((functorExtension C D).obj F).obj U ≅ I :=
…
  5. instance OAI.LittleFinitistic.QuadraticEncoding.derivedEmbeddingAdditive line 51
  6. instance OAI.LittleFinitistic.QuadraticEncoding.derivedToEssImageAdditive line 54
  7. instance OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluationAdditive line 58
  8. def OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation line 64

    Source documentation

    The manuscript's additive extension of evaluation to all of Kar(Q), with values in the actual bounded finite-dimensional derived category.

    def completedDerivedEvaluation : Karoubi (BoundedQ P) ⥤ FiniteVectorDerived.{u,v} (k := k) :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedQ

  9. instance OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluationAdditive line 67
  10. def OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluationFactors line 70