IdempotentImageEvaluation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.QuadraticEncoding.imageProjection line 14
def OAI.LittleFinitistic.QuadraticEncoding.imageInclusion line 17
lemma OAI.LittleFinitistic.QuadraticEncoding.image_projection_inclusion line 20
lemma OAI.LittleFinitistic.QuadraticEncoding.image_inclusion_projection line 22

def OAI.LittleFinitistic.QuadraticEncoding.linearImageKaroubiIso line 35

Source documentation

A functor takes a concrete linear idempotent's formal image to the actual image module.

def linearImageKaroubiIso :
    (⟨F.obj (ModuleCat.of k V), F.map (ModuleCat.ofHom p), by
      rw [← F.map_comp]
      congr 1
      exact congrArg ModuleCat.ofHom hp⟩ : Karoubi D) ≅
    (toKaroubi D).obj (F.obj (ModuleCat.of k (LinearMap.range p))) :=
…

def OAI.LittleFinitistic.QuadraticEncoding.evaluatedImage line 51
Source documentation
The actual image eY, represented in the same universe as tensor evaluation.
```
def evaluatedImage := LinearMap.range ((liftedEndHom (givenAction X r)).hom)
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.liftedEndHom, OAI.LittleFinitistic.QuadraticEncoding.givenAction
lemma OAI.LittleFinitistic.QuadraticEncoding.lifted_action_idempotent line 54
def OAI.LittleFinitistic.QuadraticEncoding.stalkSummandImageIso line 62
Source documentation
The formal evaluated summand is the stalk of the concrete image of the action.
```
def stalkSummandImageIso : stalkSummand X r hr ≅
    (toKaroubi _).obj ((vectorStalk (k := k)).obj (ModuleCat.of k (evaluatedImage X r))) := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.stalkSummand, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk, OAI.LittleFinitistic.QuadraticEncoding.evaluatedImage
def OAI.LittleFinitistic.QuadraticEncoding.quotientSummandImageIso line 70
Source documentation
Section 3: evaluation sends the formal quotient summand U to eY.
```
def quotientSummandImageIso : (karoubiEvaluation X).obj (quotientSummand r hr) ≅
    (toKaroubi _).obj ((vectorStalk (k := k)).obj (ModuleCat.of k (evaluatedImage X r))) :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.karoubiEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientSummand, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk, OAI.LittleFinitistic.QuadraticEncoding.evaluatedImage
instance OAI.LittleFinitistic.QuadraticEncoding.evaluatedImageFinite line 74