CompletedOddDoubleEvaluation.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.QuadraticEncoding.mapBiprod_square line 11
def OAI.LittleFinitistic.QuadraticEncoding.completedOddDoubleImageIso line 40
Source documentation
Evaluation of the formal odd double used in Section 3.
```
def completedOddDoubleImageIso (r : PresentedAlgebra P) (hr : r*r=r) (n : ℤ) :
    (completedDerivedEvaluation X).obj
      (quotientSummand r hr ⊞
        ((functorExtension₂ (BoundedQ P) (BoundedQ P)).obj (shiftFunctor (BoundedQ P) n)).obj
          (quotientSummand r hr)) ≅
    evaluatedImageDerived X r ⊞ (evaluatedImageDerived X r)⟦n⟧ :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientSummand, OAI.LittleFinitistic.QuadraticEncoding.BoundedQ, OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageDerived
theorem OAI.LittleFinitistic.QuadraticEncoding.completed_oddDouble_corner_square line 51
Source documentation
The two summands of the evaluated odd double carry exactly the original corner action and its shift. This is the action used at each diagram vertex.
```
theorem completed_oddDouble_corner_square (e a : PresentedAlgebra P) (he : e*e=e) (n : ℤ) :
    (completedDerivedEvaluation X).map
      (biprod.map (quotientCornerEnd e a he)
        (((functorExtension₂ (BoundedQ P) (BoundedQ P)).obj (shiftFunctor (BoundedQ P) n)).map
          (quotientCornerEnd e a he))) ≫ (completedOddDoubleImageIso X e he n).hom =
    (completedOddDoubleImageIso X e he n).hom ≫
      biprod.map (evaluatedCornerEnd X e a) ((evaluatedCornerEnd X e a)⟦n⟧') := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientCornerEnd, OAI.LittleFinitistic.QuadraticEncoding.BoundedQ, OAI.LittleFinitistic.QuadraticEncoding.completedOddDoubleImageIso, OAI.LittleFinitistic.QuadraticEncoding.evaluatedCornerEnd