OAI/Algebra/Finitistic/Encoding/RelationVertexCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.RelationVertexCoordinates.vertex line 14
  2. abbrev OAI.LittleFinitistic.RelationVertexCoordinates.tensor line 15
  3. def OAI.LittleFinitistic.RelationVertexCoordinates.zeroIso line 17
  4. def OAI.LittleFinitistic.RelationVertexCoordinates.oneIso line 19
  5. def OAI.LittleFinitistic.RelationVertexCoordinates.twoIso line 21
  6. def OAI.LittleFinitistic.RelationVertexCoordinates.quotientEntry line 24
  7. def OAI.LittleFinitistic.RelationVertexCoordinates.relationEntry line 27
  8. theorem OAI.LittleFinitistic.RelationVertexCoordinates.relationEntry_eq line 31
  9. theorem OAI.LittleFinitistic.RelationVertexCoordinates.p_square line 46

    Source documentation

    The source-zero p entry becomes the actual length-two path quotient.

    theorem p_square (a : Fin (d+1)) :
    (oneIso P D).hom ≫ (tensor P D).map (quotientEntry P a) =
      (vertex P).map (path k T (s).e₀ (s).e₁ (arrow01 P a) ((s).ha a) D) ≫
        (zeroIso P D).hom := by
…

    Mentions: OAI.LittleFinitistic.RelationVertexCoordinates.oneIso, OAI.LittleFinitistic.RelationVertexCoordinates.tensor, OAI.LittleFinitistic.RelationVertexCoordinates.quotientEntry, OAI.LittleFinitistic.RelationVertexCoordinates.vertex, OAI.LittleFinitistic.RelationVertexCoordinates.zeroIso

  10. theorem OAI.LittleFinitistic.RelationVertexCoordinates.q_square line 62

    Source documentation

    The source-zero q entry uses the original coefficients and actual b-arrow maps.

    theorem q_square (r : RelationIndex P) (a : Fin (d+1)) :
    (twoIso P D).hom ≫ (tensor P D).map (relationEntry P r a) =
      (vertex P).map (∑ b, basisCoefficient P r a b •
        path k T (s).e₁ (s).e₂ (arrow12 P b) ((s).hb b) D) ≫ (oneIso P D).hom := by
…

    Mentions: OAI.LittleFinitistic.RelationVertexCoordinates.twoIso, OAI.LittleFinitistic.RelationVertexCoordinates.tensor, OAI.LittleFinitistic.RelationVertexCoordinates.relationEntry, OAI.LittleFinitistic.RelationVertexCoordinates.vertex, OAI.LittleFinitistic.RelationVertexCoordinates.oneIso