OAI/Algebra/Finitistic/Localization/SourceActionEvaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SourceActionEvaluation.representation line 15
2. abbrev OAI.LittleFinitistic.SourceActionEvaluation.evaluation line 18
3. abbrev OAI.LittleFinitistic.SourceActionEvaluation.vertexIso line 19
4. def OAI.LittleFinitistic.SourceActionEvaluation.given line 21
5. def OAI.LittleFinitistic.SourceActionEvaluation.evaluated line 25
6. lemma OAI.LittleFinitistic.SourceActionEvaluation.theta_generator line 29
7. lemma OAI.LittleFinitistic.SourceActionEvaluation.generator_square line 36
8. lemma OAI.LittleFinitistic.SourceActionEvaluation.evaluated_generator line 50
9. theorem OAI.LittleFinitistic.SourceActionEvaluation.action_evaluates line 60

   Source documentation

   The native theta evaluates to the entire R-action, not just its generators.

   theorem action_evaluates : evaluated (Y := Y) E = given (Y := Y) E := by
   …

   Mentions: OAI.LittleFinitistic.SourceActionEvaluation.evaluated, OAI.LittleFinitistic.SourceActionEvaluation.given

10. theorem OAI.LittleFinitistic.SourceActionEvaluation.action_square line 75
11. theorem OAI.LittleFinitistic.SourceActionEvaluation.derived_action_square line 86

    Source documentation

    Whole-action compatibility in the bounded finite-dimensional derived target.

    theorem derived_action_square (r : R) :
        (SourceEvaluation.derived (representation (Y := Y) E) ⋙ derivedTargetInclusion (k := k)).map
    …

    Mentions: OAI.LittleFinitistic.SourceEvaluation.derived, OAI.LittleFinitistic.SourceActionEvaluation.representation