DerivedActionCompatibility.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.QuadraticEncoding.finiteUnderlyingLifting line 15
def OAI.LittleFinitistic.QuadraticEncoding.finiteUnderlyingComparison line 22
Source documentation
Both constructions of evaluation through Q agree by uniqueness of localization.
```
def finiteUnderlyingComparison : finiteQuotientEvaluation X ⋙ inclusion k ≅
    boundedQuotientEvaluation X :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.finiteQuotientEvaluation, OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluation
def OAI.LittleFinitistic.QuadraticEncoding.derivedUnderlyingComparison line 29
Source documentation
The existing finite derived evaluation agrees with canonical derived localization of the explicitly computed homotopy evaluation.
```
def derivedUnderlyingComparison :
    derivedQuotientEvaluation X ⋙ (derivedEmbedding k).essImage.ι ≅
      boundedQuotientEvaluation X ⋙ DerivedCategory.Qh :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluation, OAI.LittleFinitistic.QuadraticEncoding.boundedQuotientEvaluation
def OAI.LittleFinitistic.QuadraticEncoding.derivedVertexIso line 34
theorem OAI.LittleFinitistic.QuadraticEncoding.derived_quotientAction_square line 42
Source documentation
The full action square in the actual derived category, for the previously constructed bounded finite-dimensional evaluation functor.
```
theorem derived_quotientAction_square (r : PresentedAlgebra P) :
    (derivedQuotientEvaluation X ⋙ (derivedEmbedding k).essImage.ι).map (quotientAction P r) ≫
      (derivedVertexIso X 0).hom =
    (derivedVertexIso X 0).hom ≫ DerivedCategory.Qh.map
      ((vectorStalk (k := k)).map (liftedEndHom (givenAction X r))) := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.derivedQuotientEvaluation, OAI.LittleFinitistic.QuadraticEncoding.quotientAction, OAI.LittleFinitistic.QuadraticEncoding.derivedVertexIso, OAI.LittleFinitistic.QuadraticEncoding.vectorStalk, OAI.LittleFinitistic.QuadraticEncoding.liftedEndHom, OAI.LittleFinitistic.QuadraticEncoding.givenAction