CompletedShiftEvaluation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.QuadraticEncoding.completedCommutationIso line 15

Source documentation

Commutation with any endofunctor extends uniquely across idempotent completion.

def completedCommutationIso (S : C ⥤ C) (T : D ⥤ D) (e : S ⋙ F ≅ F ⋙ T) :
    (functorExtension₂ C C).obj S ⋙ (functorExtension C D).obj F ≅
      (functorExtension C D).obj F ⋙ T := by
…

def OAI.LittleFinitistic.QuadraticEncoding.completedDerivedShiftIso line 36
Source documentation
This is the formal shift used by the native odd-double construction: shift the underlying object and its idempotent. No shift coherence is assumed.
```
def completedDerivedShiftIso (n : ℤ) :
    (functorExtension₂ (BoundedQ P) (BoundedQ P)).obj (shiftFunctor (BoundedQ P) n) ⋙
      completedDerivedEvaluation X ≅
    completedDerivedEvaluation X ⋙ shiftFunctor (FiniteVectorDerived.{u,v} (k := k)) n :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedQ, OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation
def OAI.LittleFinitistic.QuadraticEncoding.completedShiftedSummandImageIso line 44
Source documentation
In particular, every formal shift of U evaluates to the same shift of eY.
```
def completedShiftedSummandImageIso (r : PresentedAlgebra P) (hr : r*r=r) (n : ℤ) :
    (completedDerivedEvaluation X).obj
      (((functorExtension₂ (BoundedQ P) (BoundedQ P)).obj (shiftFunctor (BoundedQ P) n)).obj
        (quotientSummand r hr)) ≅ (evaluatedImageDerived X r)⟦n⟧ :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.BoundedQ, OAI.LittleFinitistic.QuadraticEncoding.quotientSummand, OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageDerived