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