PresentedActionCompatibility.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.QuadraticEncoding.identifiedEndHom line 16
Source documentation
Evaluation of endomorphisms, expressed in a specified identification of the target.
```
def identifiedEndHom : End L →ₐ[k] End T where
…
```
def OAI.LittleFinitistic.QuadraticEncoding.liftedEndHom line 34
Source documentation
Canonical transport of every endomorphism of Y to its universe lift.
```
def liftedEndHom : Module.End k Y →ₐ[k] End (ModuleCat.of k (ULift.{u} Y)) where
…
```
def OAI.LittleFinitistic.QuadraticEncoding.givenAction line 44
Source documentation
The presented algebra acts on Y by precisely its specified generator endomorphisms.
```
def givenAction : PresentedAlgebra P →ₐ[k] Module.End k Y :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra
def OAI.LittleFinitistic.QuadraticEncoding.givenStalkAction line 47
def OAI.LittleFinitistic.QuadraticEncoding.evaluatedAction line 53
Source documentation
The quotient action, evaluated and identified with the stalk of Y.
```
def evaluatedAction : PresentedAlgebra P →ₐ[k]
    End ((vectorStalk (k := k)).obj (ModuleCat.of k (ULift.{u} Y))) :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk
lemma OAI.LittleFinitistic.QuadraticEncoding.evaluatedAction_generator line 58
theorem OAI.LittleFinitistic.QuadraticEncoding.quotientAction_evaluates line 74
Source documentation
Section 3, lines 167–168: the entire quotient action evaluates to the given action.
```
theorem quotientAction_evaluates : evaluatedAction X = givenStalkAction X := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.evaluatedAction, OAI.LittleFinitistic.QuadraticEncoding.givenStalkAction