strands

Mathlib.Tactic.Widget.StringDiagram

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryLike.NormalExpr.strands

Lean4

/-- The list of strands associated with a 2-morphism. -/
def strands (e : NormalExpr) : CoherenceM ρ (List (List Strand)) := do
  let l ← e.nodes
  (pairs l).mapM fun (x, y) ↦ do
      let xs := (x.map (fun n ↦ n.tarList)).flatten
      let ys := (y.map (fun n ↦ n.srcList)).flatten
      if xs.length ≠ ys.length then
        throwError"The number of the start and end points of a string does not match."
      (xs.zip ys).mapIdxM fun k ((n₁, f₁), (n₂, _)) => do
          return ⟨n₁.hPosTar + k, n₁, n₂, f₁⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru