OAI/Algebra/Finitistic/Localization/EvaluationModule.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LittleFinitistic.QuadraticEncoding.Representation line 13

    Source documentation

    An arbitrary vector-space representation of the presented quadratic algebra.

    structure Representation (P : Relations k d t) (Y : Type v)
    [AddCommGroup Y] [Module k Y] where
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Relations

  2. def OAI.LittleFinitistic.QuadraticEncoding.Representation.arrowAction line 22
  3. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.arrowAction_basis line 25
  4. def OAI.LittleFinitistic.QuadraticEncoding.Representation.rawPathAction line 30
  5. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.rawPathAction_tmul line 33
  6. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.relations_killed line 36
  7. def OAI.LittleFinitistic.QuadraticEncoding.Representation.pathAction line 43

    Source documentation

    The actual descended length-two action, using the proved relation ideal.

    def pathAction : (Paths k d ⧸ relationSpace P) →ₗ[k] Module.End k Y :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Paths, OAI.LittleFinitistic.QuadraticEncoding.relationSpace

  8. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.pathAction_mk line 46
  9. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.pathAction_composition line 49
  10. def OAI.LittleFinitistic.QuadraticEncoding.Representation.Evaluation line 53

    Source documentation

    Three copies of Y, with its representation kept in the type.

    def Evaluation (_X : Representation P Y) := Y × Y × Y

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Representation

  11. instance OAI.LittleFinitistic.QuadraticEncoding.Representation.(instance at line 54) line 54
  12. instance OAI.LittleFinitistic.QuadraticEncoding.Representation.(instance at line 55) line 55
  13. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.evaluation_add line 57
  14. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.evaluation_zero line 59
  15. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.evaluation_smul line 60
  16. def OAI.LittleFinitistic.QuadraticEncoding.Representation.act line 63
  17. instance OAI.LittleFinitistic.QuadraticEncoding.Representation.evaluationModule line 68
  18. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.smul_eq line 106
  19. instance OAI.LittleFinitistic.QuadraticEncoding.Representation.(instance at line 109) line 109
  20. instance OAI.LittleFinitistic.QuadraticEncoding.Representation.(instance at line 117) line 117
  21. instance OAI.LittleFinitistic.QuadraticEncoding.Representation.(instance at line 125) line 125
  22. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.vertex0_smul line 128
  23. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.vertex1_smul line 131
  24. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.vertex2_smul line 134
  25. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.arrow01_smul line 138
  26. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.arrow12_smul line 141
  27. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.s_smul line 145
  28. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.s'_smul line 147
  29. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.generator01_smul line 149
  30. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.generator12_smul line 151
  31. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.pathMap_smul line 154
  32. def OAI.LittleFinitistic.QuadraticEncoding.Representation.inclusion line 159

    Source documentation

    Inclusion of the copy of Y at each vertex.

    def inclusion (i : Fin 3) : Y →ₗ[k] X.Evaluation where
…
  33. def OAI.LittleFinitistic.QuadraticEncoding.Representation.projection line 167
  34. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.projection_inclusion line 175
  35. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.vertex_smul line 178
  36. def OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexSpace line 183

    Source documentation

    The vertex space e_i M(Y), as an actual k-subspace of the constructed module.

    def vertexSpace (i : Fin 3) : Submodule k X.Evaluation := (X.inclusion i).range
  37. def OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexEquiv line 185