OAI/Algebra/Finitistic/Localization/CompletedImageEvaluation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.QuadraticEncoding.sandwich_cancel line 10
2. def OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageK line 20

   Source documentation

   The image vector space, as an actual bounded finite-dimensional stalk complex.

   def evaluatedImageK : K.{u,max u v} k :=
   …

3. def OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageDerived line 24
4. abbrev OAI.LittleFinitistic.QuadraticEncoding.derivedTargetInclusion line 27
5. def OAI.LittleFinitistic.QuadraticEncoding.derivedImageProjection line 29
6. def OAI.LittleFinitistic.QuadraticEncoding.derivedImageInclusion line 35
7. lemma OAI.LittleFinitistic.QuadraticEncoding.derived_image_inclusion_projection line 43
8. lemma OAI.LittleFinitistic.QuadraticEncoding.derived_image_projection_inclusion line 52
9. def OAI.LittleFinitistic.QuadraticEncoding.completedSummandImageIso line 66

   Source documentation

   The full completed derived evaluation takes U to the actual finite-dimensional eY stalk.

   def completedSummandImageIso :
       (completedDerivedEvaluation X).obj (quotientSummand r hr) ≅ evaluatedImageDerived X r :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientSummand, OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageDerived