MeshQuiverWords.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nonzero arrow words are actual paths in the induced simple graph.

def OAI.HarmonicArtin.ParabolicIntersections.meshArrowValues line 12

theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_word_is_path line 19

Source documentation

The outside and noncomposable relations leave only genuine paths. The last-vertex annihilation statement is maintained in the induction.

theorem mesh_word_is_path (B : A → R)
    (houtside : ∀ a, Q.source a∉U ∨ Q.target a∉U → B a=0)
    (hpath : ∀ a b, Q.target a≠Q.source b → B a*B b=0) (w : List A) :
    (w.map B).prod=0 ∨ w=[] ∨
      ∃ (v : U) (p : MeshPaths (meshQuiverGraph Q U hloop) w.length v),
        meshPathEvaluate (meshQuiverGraph Q U hloop) (meshArrowValues Q U hloop B)
          w.length v p=(w.map B).prod ∧
        ∀ a, Q.source a≠v.val → (w.map B).prod*B a=0 := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths, OAI.HarmonicArtin.ParabolicIntersections.meshQuiverGraph, OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate, OAI.HarmonicArtin.ParabolicIntersections.meshArrowValues