ReidemeisterSchreier/Quiver.lean
1import Mathlib.Combinatorics.Quiver.Arborescence
2import Mathlib.Combinatorics.Quiver.ConnectedComponent
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Quiver.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Quiver arborescences
15Rooted arborescences, symmetrified quiver paths, complement edges, and total-edge counting used in Schreier basis constructions.
16-/
18namespace ReidemeisterSchreier
20/-- Forgetting the orientation of a tree edge in a symmetrized quiver identifies the total arrows
21of the tree with the original arrows covered by its symmetrification. -/
22noncomputable def Quiver.coveredArrowEquivTotal
23 {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence T] :
24 ↥(Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T)) ≃ Quiver.Total T := by
25 classical
26 refine
27 { toFun := fun e =>
28 if hpos : T e.1.left e.1.right (Sum.inl e.1.hom) then
29 { left := e.1.left
30 right := e.1.right
31 hom := ⟨Sum.inl e.1.hom, hpos⟩ }
32 else
33 { left := e.1.right
34 right := e.1.left
35 hom := ⟨Sum.inr e.1.hom, by
36 rcases e.2 with h | h
37 · exact False.elim (hpos h)
38 · exact h⟩ }
39 invFun := fun e =>
40 match he : e.hom.1 with
41 | Sum.inl f =>
42 ⟨⟨e.left, e.right, f⟩, by
43 simpa [Quiver.wideSubquiverSymmetrify, he] using Or.inl e.hom.2⟩
44 | Sum.inr f =>
45 ⟨⟨e.right, e.left, f⟩, by
46 simpa [Quiver.wideSubquiverSymmetrify, he] using Or.inr e.hom.2⟩
47 left_inv := ?_
48 right_inv := ?_ }
49 · intro e
50 apply Subtype.ext
51 rcases e with ⟨⟨a, b, f⟩, hf⟩
52 dsimp
53 by_cases hpos : T a b (Sum.inl f)
54 · rw [dif_pos hpos]
55 · rcases hf with h | h
56 · exact False.elim (hpos h)
57 · rw [dif_neg hpos]
58 · let edgeStep {a b : T} (e : a ⟶ b) :
59 (default : Quiver.Path (Quiver.root T) a).length + 1 =
60 (default : Quiver.Path (Quiver.root T) b).length := by
61 have hpath :
62 ((default : Quiver.Path (Quiver.root T) a).cons e :
63 Quiver.Path (Quiver.root T) b) = default :=
64 Subsingleton.elim _ _
65 simpa using congrArg Quiver.Path.length hpath
66 intro e
67 rcases e with ⟨a, b, e⟩
68 cases e with
70 cases e with
71 | inl f =>
72 dsimp
73 by_cases hpos : T a b (Sum.inl f)
74 · simp only [hpos, ↓reduceDIte]
75 · exact False.elim (hpos he)
76 | inr f =>
77 dsimp
78 have hnot : ¬ T b a (Sum.inl f) := by
79 intro hpos
80 let e₁ : a ⟶ b := ⟨Sum.inr f, he⟩
81 let e₂ : b ⟶ a := ⟨Sum.inl f, hpos⟩
82 have h₁ := edgeStep e₁
83 have h₂ := edgeStep e₂
84 have hab :
85 (default : Quiver.Path (Quiver.root T) a).length <
86 (default : Quiver.Path (Quiver.root T) b).length := by
87 rw [← h₁]
88 exact Nat.lt_succ_self _
89 have hba :
90 (default : Quiver.Path (Quiver.root T) b).length <
91 (default : Quiver.Path (Quiver.root T) a).length := by
92 rw [← h₂]
93 exact Nat.lt_succ_self _
94 exact (Nat.lt_asymm hab hba).elim
95 rw [dif_neg hnot]
97namespace Quiver
99/-- In an arborescence, the last edge of the unique path to a non-root vertex determines that
100vertex, and every edge arises this way. -/
101noncomputable def Arborescence.totalEquivNonRoot
102 (V : Type u) [Quiver V] [Quiver.Arborescence V] :
103 Quiver.Total V ≃ {v : V // v ≠ Quiver.root V} := by
104 let f : Quiver.Total V → {v : V // v ≠ Quiver.root V} := fun e =>
105 ⟨e.right, by
106 intro hroot
107 have hpath :
108 ((default : Quiver.Path (Quiver.root V) e.left).cons
109 (Quiver.homOfEq e.hom rfl hroot) :
110 Quiver.Path (Quiver.root V) (Quiver.root V)) = default :=
111 Subsingleton.elim _ _
112 have hnil : (default : Quiver.Path (Quiver.root V) (Quiver.root V)) = Quiver.Path.nil :=
113 Subsingleton.elim _ _
114 exact Quiver.Path.cons_ne_nil
115 (default : Quiver.Path (Quiver.root V) e.left)
116 (Quiver.homOfEq e.hom rfl hroot) (hpath.trans hnil)⟩
117 refine Equiv.ofBijective f ⟨?_, ?_⟩
118 · intro e e' h
119 cases e with
121 cases e' with
123 cases h
124 have hpath :
125 ((default : Quiver.Path (Quiver.root V) left).cons hom :
126 Quiver.Path (Quiver.root V) right) =
127 ((default : Quiver.Path (Quiver.root V) left').cons hom' :
128 Quiver.Path (Quiver.root V) right) :=
129 Subsingleton.elim _ _
130 have hleft : left = left' := Quiver.Path.obj_eq_of_cons_eq_cons hpath
131 subst hleft
132 have hhom : hom ≍ hom' := Quiver.Path.hom_heq_of_cons_eq_cons hpath
133 cases hhom
134 rfl
135 · intro v
136 let p : Quiver.Path (Quiver.root V) v.1 := default
137 have hpne : p.length ≠ 0 := by
138 intro hp0
139 exact v.2 (Quiver.Path.eq_of_length_zero p hp0).symm
140 rcases (Quiver.Path.length_ne_zero_iff_eq_cons p).mp hpne with ⟨c, p', e, hp⟩
141 refine ⟨⟨c, v.1, e⟩, ?_⟩
142 exact Subtype.ext rfl
144end Quiver
146end ReidemeisterSchreier