Paths without immediate reversal in a Serre graph

A path in the quiver of a Serre graph is reduced when no consecutive darts cancel. This condition retains the distinction between a loop and its reversed dart, and between parallel edges. It is the local normal-form condition used for graph path groups and Stallings graphs. The ordered dart list is obtained from Mathlib's Quiver.Path.weight in the free monoid; its decomposition and mapping lemmas support subgraph and based-core constructions. The paths of a restriction Γ.restrict S hS are the paths of Γ whose darts lie in S, and a path leaving a vertex set crosses its boundary along one of its darts.

def TauCeti.SerreGraph.Path.darts (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) : List Γ.E

The ordered list of darts traversed by a path.

@[simp]

theorem TauCeti.SerreGraph.Path.darts_nil (Γ : SerreGraph) (a : Γ.V) : darts Γ Quiver.Path.nil = []

@[simp]

theorem TauCeti.SerreGraph.Path.darts_cons (Γ : SerreGraph) {a b c : Γ.V} (p : Γ.Path a b) (e : b ⟶ c) : darts Γ (Quiver.Path.cons p e) = darts Γ p ++ [↑e]

@[simp]

theorem TauCeti.SerreGraph.Path.darts_toPath (Γ : SerreGraph) {a b : Γ.V} (e : a ⟶ b) : darts Γ e.toPath = [↑e]

@[simp]

theorem TauCeti.SerreGraph.Path.darts_comp (Γ : SerreGraph) {a b c : Γ.V} (p : Γ.Path a b) (q : Γ.Path b c) : darts Γ (Quiver.Path.comp p q) = darts Γ p ++ darts Γ q

@[simp]

theorem TauCeti.SerreGraph.Path.darts_reverse (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) : darts Γ (Quiver.Path.reverse p) = List.map Γ.rev (darts Γ p).reverse

@[simp]

theorem TauCeti.SerreGraph.Path.length_darts (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) : (darts Γ p).length = Quiver.Path.length p

A path traverses as many darts as its length.

theorem TauCeti.SerreGraph.Path.exists_eq_cons_comp_of_mem_darts (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) {e : Γ.E} (he : e ∈ darts Γ p) : ∃ (q : Γ.Path a (Γ.src e)) (r : Γ.Path (Γ.tgt e) b), p = (Quiver.Path.cons q (Γ.dart e)).comp r

A traversed dart separates a path into a prefix, that dart, and a suffix.

def TauCeti.SerreGraph.Path.IsReduced (Γ : SerreGraph) {a b : Γ.V} : Γ.Path a b → Prop

A Serre path has no consecutive pair of mutually reversed darts.

@[simp]

theorem TauCeti.SerreGraph.Path.isReduced_nil (Γ : SerreGraph) (a : Γ.V) : IsReduced Γ Quiver.Path.nil

@[simp]

theorem TauCeti.SerreGraph.Path.isReduced_toPath (Γ : SerreGraph) {a b : Γ.V} (e : a ⟶ b) : IsReduced Γ e.toPath

@[simp]

theorem TauCeti.SerreGraph.Path.isReduced_cons_cons (Γ : SerreGraph) {a b c d : Γ.V} (p : Γ.Path a b) (e : b ⟶ c) (f : c ⟶ d) : IsReduced Γ ((Quiver.Path.cons p e).cons f) ↔ IsReduced Γ (Quiver.Path.cons p e) ∧ ↑f ≠ Γ.rev ↑e

The reducedness test for a newly appended dart only examines the preceding dart.

@[simp]

theorem TauCeti.SerreGraph.Path.darts_cast (Γ : SerreGraph) {a b a' b' : Γ.V} (ha : a = a') (hb : b = b') (p : Γ.Path a b) : darts Γ (Quiver.Path.cast ha hb p) = darts Γ p

Transporting a path along equalities of its endpoints keeps its darts.

@[simp]

theorem TauCeti.SerreGraph.Path.isReduced_cast (Γ : SerreGraph) {a b a' b' : Γ.V} (ha : a = a') (hb : b = b') (p : Γ.Path a b) : IsReduced Γ (Quiver.Path.cast ha hb p) ↔ IsReduced Γ p

Transporting a path along equalities of its endpoints keeps it reduced.

theorem TauCeti.SerreGraph.Path.IsReduced.of_cons (Γ : SerreGraph) {a b c : Γ.V} {p : Γ.Path a b} {e : b ⟶ c} (hp : IsReduced Γ (Quiver.Path.cons p e)) : IsReduced Γ p

Every prefix obtained by removing the final dart of a reduced path is reduced.

theorem TauCeti.SerreGraph.Path.IsReduced.of_comp_left (Γ : SerreGraph) {a b c : Γ.V} {p : Γ.Path a b} {q : Γ.Path b c} (hp : IsReduced Γ (Quiver.Path.comp p q)) : IsReduced Γ p

A prefix of a reduced concatenation is reduced.

@[simp]

theorem TauCeti.SerreGraph.Hom.darts_mapPath (Γ : SerreGraph) {Δ : SerreGraph} (f : Γ.Hom Δ) {a b : Γ.V} (p : Γ.Path a b) : Path.darts Δ (f.toPrefunctor.mapPath p) = List.map f.mapE (Path.darts Γ p)

Mapping a path maps its dart list pointwise.

theorem TauCeti.SerreGraph.Hom.isReduced_mapPath_iff (Γ : SerreGraph) {Δ : SerreGraph} (f : Γ.Hom Δ) (hf : Function.Injective f.mapE) {a b : Γ.V} (p : Γ.Path a b) : Path.IsReduced Δ (f.toPrefunctor.mapPath p) ↔ Path.IsReduced Γ p

A morphism injective on darts preserves and reflects reduced paths.

@[simp]

theorem TauCeti.SerreGraph.Path.isReduced_reverse (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) : IsReduced Γ (Quiver.Path.reverse p) ↔ IsReduced Γ p

Reversing a path preserves the absence of immediate backtracking.

theorem TauCeti.SerreGraph.Path.IsReduced.of_comp_right (Γ : SerreGraph) {a b c : Γ.V} {p : Γ.Path a b} {q : Γ.Path b c} (hp : IsReduced Γ (Quiver.Path.comp p q)) : IsReduced Γ q

A suffix of a reduced concatenation is reduced.

theorem TauCeti.SerreGraph.Path.isReduced_iff_isChain (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) : IsReduced Γ p ↔ List.IsChain (fun (e f : Γ.E) => f ≠ Γ.rev e) (darts Γ p)

A path is reduced exactly when no dart of its dart list is followed by its reverse.

theorem TauCeti.SerreGraph.Path.isReduced_comp_iff (Γ : SerreGraph) {a b c : Γ.V} (p : Γ.Path a b) (q : Γ.Path b c) : IsReduced Γ (Quiver.Path.comp p q) ↔ IsReduced Γ p ∧ IsReduced Γ q ∧ ∀ e ∈ (darts Γ p).getLast?, ∀ f ∈ (darts Γ q).head?, f ≠ Γ.rev e

A concatenation is reduced exactly when both pieces are and the first dart of the second piece does not reverse the last dart of the first.

theorem TauCeti.SerreGraph.Path.src_eq_of_mem_head?_darts (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) {e : Γ.E} (he : e ∈ (darts Γ p).head?) : Γ.src e = a

The first dart of a path starts at the start of the path.

theorem TauCeti.SerreGraph.Path.tgt_eq_of_mem_getLast?_darts (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) {e : Γ.E} (he : e ∈ (darts Γ p).getLast?) : Γ.tgt e = b

The last dart of a path ends at the end of the path.

theorem TauCeti.SerreGraph.Path.eq_of_darts_eq_nil (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) (hp : darts Γ p = []) : a = b

A path without darts joins a vertex to itself.

theorem TauCeti.SerreGraph.Path.mem_iff_mem_of_forall_mem_darts (Γ : SerreGraph) {S : Set Γ.E} {R : Set Γ.V} (hS : ∀ e ∈ S, Γ.rev e ∈ S) (hR : ∀ e ∈ S, Γ.src e ∈ R → Γ.tgt e ∈ R) {a b : Γ.V} (p : Γ.Path a b) (hp : ∀ e ∈ darts Γ p, e ∈ S) : a ∈ R ↔ b ∈ R

Paths in a set of darts that preserves a vertex set R start in R exactly when they end in R.

theorem TauCeti.SerreGraph.Path.exists_boundary_dart (Γ : SerreGraph) {a b : Γ.V} (p : Γ.Path a b) (R : Set Γ.V) (ha : a ∈ R) (hb : b ∉ R) : ∃ e ∈ darts Γ p, Γ.src e ∈ R ∧ Γ.tgt e ∉ R

A path from a vertex set R to its complement has a dart from R to its complement.

theorem TauCeti.SerreGraph.exists_restrict_path (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) {a b : Γ.V} (p : Γ.Path a b) (hp : ∀ e ∈ Path.darts Γ p, e ∈ S) : ∃ (q : (Γ.restrict S hS).Path a b), (Γ.restrictInclusion S hS).toPrefunctor.mapPath q = p

A path all of whose darts lie in S lifts through the inclusion of the restriction.

theorem TauCeti.SerreGraph.mem_of_mem_darts_mapPath (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) {a b : (Γ.restrict S hS).V} (q : (Γ.restrict S hS).Path a b) {e : Γ.E} (he : e ∈ Path.darts Γ ((Γ.restrictInclusion S hS).toPrefunctor.mapPath q)) : e ∈ S

The darts of a path in the restriction lie in S.

@[simp]

theorem TauCeti.SerreGraph.isReduced_restrictInclusion_mapPath_iff (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) {a b : (Γ.restrict S hS).V} (q : (Γ.restrict S hS).Path a b) : Path.IsReduced Γ ((Γ.restrictInclusion S hS).toPrefunctor.mapPath q) ↔ Path.IsReduced (Γ.restrict S hS) q

A path in the restriction is reduced exactly when it is reduced in the ambient graph.

theorem TauCeti.SerreGraph.preconnected_restrict_iff (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) : (Γ.restrict S hS).Preconnected ↔ ∀ (a b : Γ.V), ∃ (p : Γ.Path a b), ∀ e ∈ Path.darts Γ p, e ∈ S

The restriction is preconnected exactly when any two vertices are joined by a path of Γ whose darts lie in S.

theorem TauCeti.SerreGraph.rose_not_isReduced_backtrack {α : Type u_1} (a : α) : ¬Path.IsReduced (rose α) ((Quiver.Path.nil.cons ((rose α).dart (a, true))).cons ((rose α).dart (a, false)))

Traversing a rose petal and then its reverse is a backtrack.

theorem TauCeti.SerreGraph.rose_isReduced_of_ne {α : Type u_1} {a b : α} (hab : a ≠ b) : Path.IsReduced (rose α) ((Quiver.Path.nil.cons ((rose α).dart (a, true))).cons ((rose α).dart (b, false)))

Traversing one rose petal and then the reverse of a different petal is reduced.

def TauCeti.SerreGraph.rosePetal {α : Type u_1} (a : α) : (rose α).Path PUnit.unit PUnit.unit

A rose petal is a closed path of length one.

theorem TauCeti.SerreGraph.rosePetal_eq_toPath {α : Type u_1} (a : α) : rosePetal a = ((rose α).dart (a, true)).toPath

A rose petal is the path consisting of its positive dart.

@[simp]

theorem TauCeti.SerreGraph.rosePetal_length {α : Type u_1} (a : α) : Quiver.Path.length (rosePetal a) = 1

theorem TauCeti.SerreGraph.rosePetal_isReduced {α : Type u_1} (a : α) : Path.IsReduced (rose α) (rosePetal a)

A rose petal is reduced.