OAI/Algebra/Finitistic/Selected/SelectedDiagramEvaluation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedDiagramEvaluation.F line 15
  2. abbrev OAI.LittleFinitistic.SelectedDiagramEvaluation.G line 16
  3. abbrev OAI.LittleFinitistic.SelectedDiagramEvaluation.target line 17
  4. def OAI.LittleFinitistic.SelectedDiagramEvaluation.targetAction line 18
  5. def OAI.LittleFinitistic.SelectedDiagramEvaluation.V0Iso line 22

    Source documentation

    Evaluation of the one fixed actual V0 is precisely eY direct-sum eY[3].

    def V0Iso : (F (Y := Y)).obj fixed.V0 ≅ target (Y := Y) :=
…

    Mentions: OAI.LittleFinitistic.SelectedDiagramEvaluation.F, OAI.LittleFinitistic.SelectedDiagramEvaluation.target

  6. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.V0_action line 27

    Source documentation

    The V0 identification intertwines every selected algebra element on both summands.

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

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

  7. abbrev OAI.LittleFinitistic.SelectedDiagramEvaluation.sourceEvaluation line 44
  8. def OAI.LittleFinitistic.SelectedDiagramEvaluation.sourceFactors line 47
  9. def OAI.LittleFinitistic.SelectedDiagramEvaluation.D0Iso line 52
  10. def OAI.LittleFinitistic.SelectedDiagramEvaluation.D1Iso line 54
  11. def OAI.LittleFinitistic.SelectedDiagramEvaluation.D2Iso line 56
  12. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.D_arrow01 line 60

    Source documentation

    Every first-family arrow of the same fixed K diagram has its selected action.

    theorem D_arrow01 (a : Fin (encoding.generators+1)) :
    (sourceEvaluation (Y := Y)).map (fixed.f a) ≫ (D1Iso (Y := Y)).hom =
…

    Mentions: OAI.LittleFinitistic.SelectedDiagramEvaluation.sourceEvaluation, OAI.LittleFinitistic.SelectedDiagramEvaluation.D1Iso

  13. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.D_arrow12 line 75
  14. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.targetAction_one line 90
  15. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.distinguished_arrow01 line 96
  16. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.distinguished_arrow12 line 101
  17. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.fixed_diagram_evaluates line 107

    Source documentation

    The same globally chosen K diagram evaluates correctly for every finite module.

    theorem fixed_diagram_evaluates :
    ∃ (i0 : (sourceEvaluation (Y := Y)).obj fixed.D0 ≅ target (Y := Y))
…

    Mentions: OAI.LittleFinitistic.SelectedDiagramEvaluation.sourceEvaluation, OAI.LittleFinitistic.SelectedDiagramEvaluation.target

  18. theorem OAI.LittleFinitistic.SelectedDiagramEvaluation.targetAction_on_image line 119

    Source documentation

    Exact vector formula for the selected action, including the alpha restriction.

    theorem targetAction_on_image (r : SelectionRing) (y : imageSpace (k := ℂ) (Y := Y) e) :
…

    Mentions: OAI.LittleFinitistic.SelectionRing