OAI/Algebra/Finitistic/Encoding/ThreeVertexAlgebra.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.ThreeVertexAlgebra line 15

    Source documentation

    Coordinates by the six possible path endpoints: three vertices, 0-to-1 arrows, 1-to-2 arrows, and length-two paths modulo relations.

    abbrev ThreeVertexAlgebra (_μ : W →ₗ[k] V →ₗ[k] U) := k × k × k × V × W × U
…
  2. instance OAI.LittleFinitistic.ThreeVertexAlgebra.(instance at line 20) line 20
  3. instance OAI.LittleFinitistic.ThreeVertexAlgebra.(instance at line 22) line 22
  4. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.zero_eq line 25
  5. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.add_eq line 26
  6. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.smul_eq line 30
  7. def OAI.LittleFinitistic.ThreeVertexAlgebra.mul line 34
  8. def OAI.LittleFinitistic.ThreeVertexAlgebra.unit line 40
  9. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.ext line 42
  10. instance OAI.LittleFinitistic.ThreeVertexAlgebra.(instance at line 48) line 48
  11. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.mul_eq line 104
  12. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.one_eq line 105
  13. instance OAI.LittleFinitistic.ThreeVertexAlgebra.(instance at line 107) line 107
  14. instance OAI.LittleFinitistic.ThreeVertexAlgebra.(instance at line 129) line 129
  15. def OAI.LittleFinitistic.ThreeVertexAlgebra.vertex line 134

    Source documentation

    The three vertex idempotents, in the manuscript's order.

    def vertex : Fin 3 → ThreeVertexAlgebra μ
  | ⟨0, _⟩ => (1, 0, 0, 0, 0, 0)
  | ⟨1, _⟩ => (0, 1, 0, 0, 0, 0)
  | ⟨2, _⟩ => (0, 0, 1, 0, 0, 0)

    Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra

  16. def OAI.LittleFinitistic.ThreeVertexAlgebra.directedSystem line 139
  17. theorem OAI.LittleFinitistic.ThreeVertexAlgebra.globalDimension_le_two line 156

    Source documentation

    The three-vertex coordinate algebra has global dimension at most two on both sides.

    theorem globalDimension_le_two :
    (⨆ N : ModuleCat.{max u v} (ThreeVertexAlgebra μ), projectiveDimension N) ≤ (2 : ℕ) ∧
    (⨆ N : ModuleCat.{max u v} (ThreeVertexAlgebra μ)ᵐᵒᵖ, projectiveDimension N) ≤ (2 : ℕ) :=
…

    Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra