OAI/Algebra/Finitistic/Selected/SelectedNativeAction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedNativeEvaluation.imageEnd line 13
2. abbrev OAI.LittleFinitistic.SelectedNativeEvaluation.moduleIso line 15
3. def OAI.LittleFinitistic.SelectedNativeEvaluation.HAction line 17
4. theorem OAI.LittleFinitistic.SelectedNativeEvaluation.HAction_apply line 21

   Source documentation

   The conjugated map is the primary selectionStep module action, on every vector.

   theorem HAction_apply (r : SelectionRing) (x : H (Y := Y)) :
   …

   Mentions: OAI.LittleFinitistic.SelectionRing, OAI.LittleFinitistic.SelectedNativeEvaluation.H

5. lemma OAI.LittleFinitistic.SelectedNativeEvaluation.module_square line 29
6. def OAI.LittleFinitistic.SelectedNativeEvaluation.HKAction line 36
7. def OAI.LittleFinitistic.SelectedNativeEvaluation.HDerivedAction line 38
8. lemma OAI.LittleFinitistic.SelectedNativeEvaluation.imageIsoK_hom line 41
9. lemma OAI.LittleFinitistic.SelectedNativeEvaluation.image_square line 46
10. abbrev OAI.LittleFinitistic.SelectedNativeEvaluation.targetAction line 63
11. lemma OAI.LittleFinitistic.SelectedNativeEvaluation.target_square line 66
12. theorem OAI.LittleFinitistic.SelectedNativeEvaluation.V0_action line 78

    Source documentation

    The fixed V0 evaluates equivariantly to the primary H(Y) plus H(Y)[3].

    theorem V0_action (r : SelectionRing) :
        (SelectedDiagramEvaluation.F (Y := Y)).map (fixed.rho r) ≫ (V0Iso (Y := Y)).hom =
    …

    Mentions: OAI.LittleFinitistic.SelectionRing, OAI.LittleFinitistic.SelectedDiagramEvaluation.F, OAI.LittleFinitistic.SelectedNativeEvaluation.V0Iso

13. theorem OAI.LittleFinitistic.SelectedNativeEvaluation.D_arrow01 line 85
14. theorem OAI.LittleFinitistic.SelectedNativeEvaluation.D_arrow12 line 93