OAI/Algebra/Finitistic/Rectification/VertexTensorEvaluation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexId line 13
  2. def OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexFixedEquiv line 16

    Source documentation

    Identify the actual fixed-point vertex part of M(Y) with Y.

    def vertexFixedEquiv (i : Fin 3) : leftSpace (k := k) (vertexId (P := P) i) X.Evaluation ≃ₗ[k] Y where
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexId

  3. def OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexTensorEquiv line 27

    Source documentation

    The manuscript's E_i tensor_B M(Y) ≃ Y, for the actual right ideal E_i=e_iB.

    def vertexTensorEquiv (i : Fin 3) :
    Tensor k (B P) (rightIdeal (vertexId (P := P) i)) X.Evaluation ≃ₗ[k] Y :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexId

  4. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexTensorEquiv_mk line 32
  5. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexTensorEquiv_symm line 37
  6. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.tensor_leftMultiply line 44

    Source documentation

    Under the natural tensor identifications, an arrow map evaluates to its module action.

    theorem tensor_leftMultiply (i j : Fin 3) (b : B P)
    (ht : vertexId (P := P) j*b=b) (hs : b*vertexId (P := P) i=b) (y : Y) :
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.B, OAI.LittleFinitistic.QuadraticEncoding.Representation.vertexId

  7. lemma OAI.LittleFinitistic.QuadraticEncoding.Representation.arrow01_target line 52
  8. lemma OAI.LittleFinitistic.QuadraticEncoding.Representation.arrow01_source line 55
  9. lemma OAI.LittleFinitistic.QuadraticEncoding.Representation.arrow12_target line 58
  10. lemma OAI.LittleFinitistic.QuadraticEncoding.Representation.arrow12_source line 61
  11. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.tensor_arrow01 line 65
  12. theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.tensor_arrow12 line 75