CompletedCornerEvaluation.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.QuadraticEncoding.completedExtensionImageSquare line 17
def OAI.LittleFinitistic.QuadraticEncoding.imageCornerEnd line 39
lemma OAI.LittleFinitistic.QuadraticEncoding.image_corner_square line 43
lemma OAI.LittleFinitistic.QuadraticEncoding.imageCornerEnd_apply line 51
Source documentation
When a commutes with p, the corner operator is the restriction of a to the image.
```
lemma imageCornerEnd_apply (ha : p*a=a*p) (x : LinearMap.range p) :
    ((imageCornerEnd p a) x).val = a x.val := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.imageCornerEnd
def OAI.LittleFinitistic.QuadraticEncoding.quotientCornerEnd line 66
def OAI.LittleFinitistic.QuadraticEncoding.evaluatedCornerEnd line 74
lemma OAI.LittleFinitistic.QuadraticEncoding.derived_corner_projection_square line 80
theorem OAI.LittleFinitistic.QuadraticEncoding.completed_corner_square line 101
Source documentation
The complete derived evaluation intertwines every corner endomorphism with its concrete action on eY; this includes e alpha(r) e from Section 3.
```
theorem completed_corner_square :
    (completedDerivedEvaluation X).map (quotientCornerEnd e a he) ≫
      (completedSummandImageIso X e he).hom =
    (completedSummandImageIso X e he).hom ≫ evaluatedCornerEnd X e a := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.completedDerivedEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientCornerEnd, OAI.LittleFinitistic.QuadraticEncoding.completedSummandImageIso, OAI.LittleFinitistic.QuadraticEncoding.evaluatedCornerEnd
theorem OAI.LittleFinitistic.QuadraticEncoding.central_alpha_restriction line 115
Source documentation
For a central e and any algebra endomorphism alpha, the concrete map on eY is the restriction of alpha(r), exactly as in the manuscript.
```
theorem central_alpha_restriction (hec : ∀ b : PresentedAlgebra P, e*b=b*e)
    (α : PresentedAlgebra P →ₐ[k] PresentedAlgebra P) (b : PresentedAlgebra P)
    (y : evaluatedImage X e) :
    ((imageCornerEnd (liftedEndHom (givenAction X e)).hom
      (liftedEndHom (givenAction X (α b))).hom) y).val =
      (liftedEndHom (givenAction X (α b))).hom y.val := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.evaluatedImage, OAI.LittleFinitistic.QuadraticEncoding.imageCornerEnd, OAI.LittleFinitistic.QuadraticEncoding.liftedEndHom, OAI.LittleFinitistic.QuadraticEncoding.givenAction