GraphTree.lean

1 import Mathlib.Combinatorics.Quiver.Symmetric
2 import Mathlib.Data.Fintype.Card
3 import Mathlib.Data.Nat.Find
4 import Mathlib.Tactic
5 
6 /-! A rooted spanning tree of a connected quiver, with the identities of the
7 original edges retained. The construction selects a predecessor along a
8 shortest path in the symmetrified quiver. -/
9 set_option autoImplicit false
10 set_option backward.isDefEq.respectTransparency false
11 noncomputable section
12 namespace PaperXI.GraphTree
13 
14 universe u v
15 variable {α : Type u} [Quiver.{v} α]
16 
17 /-- The original edges, counted once with their chosen orientation. -/
18 abbrev Edge (α : Type u) [Quiver.{v} α] := Σ a b : α, (a ⟶ b)
19 
20 /-- Traversals include both formal orientations, including for a self-loop. -/
21 abbrev Traversal (a b : α) := @Quiver.Hom (Quiver.Symmetrify α) _ a b
22 
23 /-- Paths in the graph use its formal symmetrification. -/
24 abbrev Path (a b : α) := @Quiver.Path (Quiver.Symmetrify α) _ a b
25 
26 /-- Connectedness is actual reachability by typed edge paths. -/
27 def Connected : Prop := ∀ a b : α, Nonempty (Path a b)
28 
29 /-- Rooted predecessor data with strictly decreasing depth. -/
30 structure Rooted (α : Type u) [Quiver.{v} α] (r : α) where
31   depth : α → ℕ
32   depth_root : depth r = 0
33   parent : {a : α // a ≠ r} → α
34   parentEdge : ∀ a : {a : α // a ≠ r}, Traversal (parent a) a.val
35   parent_depth : ∀ a : {a : α // a ≠ r}, depth (parent a) < depth a.val
36 
37 variable (r : α) (hc : Connected (α := α))
38 
39 include hc in
40 private theorem exists_length (a : α) : ∃ n, ∃ p : Path r a, p.length = n := by
41   obtain ⟨p⟩ := hc r a
42   exact ⟨p.length, p, rfl⟩
43 
44 /-- The minimum number of traversals from the root. -/
45 def distance (a : α) : ℕ := by
46   classical
47   exact Nat.find (exists_length r hc a)
48 
49 theorem distance_le (a : α) (p : Path r a) : distance r hc a ≤ p.length := by
50   classical
51   exact Nat.find_min' (exists_length r hc a) ⟨p, rfl⟩
52 
53 theorem distance_root : distance r hc r = 0 := by
54   have h := distance_le r hc r Quiver.Path.nil
55   exact Nat.eq_zero_of_le_zero h
56 
57 private theorem exists_predecessor (a : α) (ha : a ≠ r) :
58     ∃ b : α, Nonempty (Traversal b a) ∧ distance r hc b < distance r hc a := by
59   classical
60   obtain ⟨p, hp⟩ := Nat.find_spec (exists_length r hc a)
61   cases p with
62   | nil => exact (ha rfl).elim
63   | @cons b a p e =>
64     refine ⟨b, ⟨e⟩, ?_⟩
65     have hm := distance_le r hc b p
66     simp only [Quiver.Path.length_cons] at hp
67     change _ = distance r hc a at hp
68     omega
69 
70 /-- Connectedness constructs a rooted spanning tree; none is supplied as input. -/
71 def ofConnected : Rooted α r where
72   depth := distance r hc
73   depth_root := distance_root r hc
74   parent a := Classical.choose (exists_predecessor r hc a.val a.property)
75   parentEdge a := Classical.choice
76     (Classical.choose_spec (exists_predecessor r hc a.val a.property)).1
77   parent_depth a :=
78     (Classical.choose_spec (exists_predecessor r hc a.val a.property)).2
79 
80 variable {r}
81 
82 /-- The actual root path, constructed by recursion on decreasing depth. -/
83 def rootPath (T : Rooted α r) (a : α) : Path r a := by
84   classical
85   exact if h : a = r then h.symm ▸ Quiver.Path.nil
86   else (rootPath T (T.parent ⟨a, h⟩)).cons (T.parentEdge ⟨a, h⟩)
87 termination_by T.depth a
88 decreasing_by exact T.parent_depth ⟨a, h⟩
89 
90 variable (T : Rooted α r)
91 
92 theorem rootPath_root : rootPath T r = Quiver.Path.nil := by
93   rw [rootPath]
94   simp
95 
96 theorem rootPath_parent (a : {a : α // a ≠ r}) :
97     (rootPath T (T.parent a)).cons (T.parentEdge a) = rootPath T a.val := by
98   conv_rhs => rw [rootPath]
99   rw [dite_eq_right a.property]
100 
101 /-- Induction along the constructed rooted tree follows decreasing depth. -/
102 theorem rooted_induction (P : α → Prop) (hr : P r)
103     (step : ∀ a : {a : α // a ≠ r}, P (T.parent a) → P a.val) (a : α) : P a := by
104   classical
105   by_cases h : a = r
106   · simpa only [h] using hr
107   · exact step ⟨a, h⟩ (rooted_induction P hr step (T.parent ⟨a, h⟩))
108 termination_by T.depth a
109 decreasing_by exact T.parent_depth ⟨a, h⟩
110 
111 /-- Forget the formal direction, retaining the original edge identity. -/
112 def underlying {a b : α} (e : Traversal a b) : Edge α :=
113   match e with
114   | Sum.inl f => ⟨a, b, f⟩
115   | Sum.inr f => ⟨b, a, f⟩
116 
117 /-- One selected original edge for each nonroot vertex. -/
118 def selected (a : {a : α // a ≠ r}) : Edge α := underlying (T.parentEdge a)
119 
120 theorem underlying_endpoints {a b : α} (e : Traversal a b) :
121     ((underlying e).1 = a ∧ (underlying e).2.1 = b) ∨
122     ((underlying e).1 = b ∧ (underlying e).2.1 = a) := by
123   cases e <;> simp [underlying]
124 
125 theorem selected_injective : Function.Injective (selected T) := by
126   intro a b hab
127   have ha := underlying_endpoints (T.parentEdge a)
128   have hb := underlying_endpoints (T.parentEdge b)
129   change selected T a = selected T b at hab
130   change ((selected T a).1 = T.parent a ∧ (selected T a).2.1 = a.val) ∨
131     ((selected T a).1 = a.val ∧ (selected T a).2.1 = T.parent a) at ha
132   change ((selected T b).1 = T.parent b ∧ (selected T b).2.1 = b.val) ∨
133     ((selected T b).1 = b.val ∧ (selected T b).2.1 = T.parent b) at hb
134   rw [hab] at ha
135   have hda := T.parent_depth a
136   have hdb := T.parent_depth b
137   rcases ha with ha | ha <;> rcases hb with hb | hb
138   · exact Subtype.ext (ha.2.symm.trans hb.2)
139   · have h1 : T.parent a = b.val := ha.1.symm.trans hb.1
140     have h2 : T.parent b = a.val := hb.2.symm.trans ha.2
141     rw [h1] at hda
142     rw [h2] at hdb
143     omega
144   · have h1 : T.parent a = b.val := ha.2.symm.trans hb.2
145     have h2 : T.parent b = a.val := hb.1.symm.trans ha.1
146     rw [h1] at hda
147     rw [h2] at hdb
148     omega
149   · exact Subtype.ext (ha.1.symm.trans hb.1)
150 
151 /-- Tree support is a set of original edges, rather than endpoint pairs. -/
152 def treeEdges : Set (Edge α) := Set.range (selected T)
153 
154 /-- Every original edge outside the selected tree is a chord. -/
155 def Chord := {e : Edge α // e ∉ treeEdges T}
156 
157 theorem mem_treeEdges (a : {a : α // a ≠ r}) : selected T a ∈ treeEdges T :=
158   ⟨a, rfl⟩
159 
160 theorem treeEdges_induction (P : Edge α → Prop)
161     (h : ∀ a : {a : α // a ≠ r}, P (selected T a)) :
162     ∀ e ∈ treeEdges T, P e := by
163   rintro e ⟨a, rfl⟩
164   exact h a
165 
166 /-- A tree never selects a self-loop, even when the original quiver has them. -/
167 theorem selected_not_loop (a : {a : α // a ≠ r}) :
168     (selected T a).1 ≠ (selected T a).2.1 := by
169   have hd := T.parent_depth a
170   have he := underlying_endpoints (T.parentEdge a)
171   change ((selected T a).1 = T.parent a ∧ (selected T a).2.1 = a.val) ∨
172     ((selected T a).1 = a.val ∧ (selected T a).2.1 = T.parent a) at he
173   intro h
174   rcases he with he | he
175   · have hp : T.parent a = a.val := he.1.symm.trans (h.trans he.2)
176     rw [hp] at hd
177     exact (Nat.lt_irrefl _ hd)
178   · have hp : T.parent a = a.val := he.2.symm.trans (h.symm.trans he.1)
179     rw [hp] at hd
180     exact (Nat.lt_irrefl _ hd)
181 
182 /-- Every traversal of a supported path belongs to the selected tree. -/
183 def Supported {a : Quiver.Symmetrify α} :
184     ∀ {b : Quiver.Symmetrify α}, Quiver.Path a b → Prop
185   | _, .nil => True
186   | _, .cons p e => Supported p ∧ underlying (α := α) e ∈ treeEdges T
187 
188 theorem rootPath_supported (a : α) : Supported T (rootPath T a) := by
189   apply rooted_induction T (fun a => Supported T (rootPath T a))
190   · rw [rootPath_root]
191     trivial
192   · intro b hb
193     rw [← rootPath_parent]
194     exact ⟨hb, mem_treeEdges T b⟩
195 
196 theorem treeEdges_no_loop (e : Edge α) (he : e ∈ treeEdges T) : e.1 ≠ e.2.1 :=
197   treeEdges_induction T (fun e => e.1 ≠ e.2.1) (selected_not_loop T) e he
198 
199 /-- The selected tree has exactly one edge per nonroot vertex. -/
200 theorem tree_card [Fintype α] [Fintype (treeEdges T)] :
201     Fintype.card (treeEdges T) = Fintype.card α - 1 := by
202   classical
203   calc
204     Fintype.card (treeEdges T) = Fintype.card {a : α // a ≠ r} :=
205       (Fintype.card_congr (show {a : α // a ≠ r} ≃ treeEdges T from
206         Equiv.ofInjective (selected T) (selected_injective T))).symm
207     _ = Fintype.card α - 1 := by
208       rw [Fintype.card_subtype_compl, Fintype.card_subtype_eq]
209 
210 /-- The cycle rank counts original edge identities, not doubled traversals. -/
211 theorem chord_count [Fintype α] [Fintype (Edge α)] [Fintype (Chord T)] :
212     Fintype.card (Chord T) + Fintype.card α = Fintype.card (Edge α) + 1 := by
213   classical
214   let : Fintype (treeEdges T) := Fintype.ofFinite _
215   have htree := tree_card T
216   have hle : Fintype.card (treeEdges T) ≤ Fintype.card (Edge α) :=
217     Fintype.card_le_of_injective Subtype.val Subtype.val_injective
218   have hcomp : Fintype.card (Chord T) =
219       Fintype.card (Edge α) - Fintype.card (treeEdges T) :=
220     by simpa only [← Nat.card_eq_fintype_card, Chord] using
221       Fintype.card_subtype_compl (fun e : Edge α => e ∈ treeEdges T)
222   have hpos : 0 < Fintype.card α := Fintype.card_pos_iff.mpr ⟨r⟩
223   omega
224 
225 include T in
226 theorem edge_count_lower_bound [Fintype α] [Fintype (Edge α)] :
227     Fintype.card α - 1 ≤ Fintype.card (Edge α) := by
228   classical
229   let : Fintype (treeEdges T) := Fintype.ofFinite _
230   rw [← tree_card T]
231   exact Fintype.card_le_of_injective Subtype.val Subtype.val_injective
232 
233 theorem chord_card [Fintype α] [Fintype (Edge α)] [Fintype (Chord T)] :
234     Fintype.card (Chord T) = Fintype.card (Edge α) + 1 - Fintype.card α := by
235   have h := chord_count T
236   omega
237 
238 /-- The usual subtraction formula is exact as an integer identity. -/
239 theorem chord_card_int [Fintype α] [Fintype (Edge α)] [Fintype (Chord T)] :
240     (Fintype.card (Chord T) : ℤ) =
241       (Fintype.card (Edge α) : ℤ) - (Fintype.card α : ℤ) + 1 := by
242   have h := chord_count T
243   omega
244 
245 end PaperXI.GraphTree

Back to source controls