GraphLoop.lean

1 import Mathlib.CategoryTheory.Groupoid.FreeGroupoid
2 import Mathlib.CategoryTheory.Endomorphism
3 import Mathlib.GroupTheory.Abelianization.Defs
4 
5 /-!
6 # Reduced graph loops and their abelianization
7 
8 Edges belong to the original quiver. A path in its symmetrification can traverse
9 an edge in either direction. The free groupoid identifies paths under insertion
10 and deletion of an edge followed by its reverse. Based endomorphisms therefore
11 give the combinatorial fundamental group, with multiplication ordered as function
12 composition: `x * y` traverses `y` before `x`.
13 
14 `H1` is the abelianization of this actual path quotient. No comparison with a
15 topological realization or singular homology is asserted here.
16 -/
17 
18 namespace PaperXI.GraphLoop
19 
20 open CategoryTheory
21 
22 universe u v w
23 
24 variable {α : Type u} [Quiver.{v} α]
25 
26 /-- The object of the free groupoid represented by a graph vertex. -/
27 abbrev vertex (r : α) : Quiver.FreeGroupoid α :=
28   (Quiver.FreeGroupoid.of α).obj r
29 
30 /-- The quotient class of an actual oriented path. -/
31 def pathClass {u v : α} (p : @Quiver.Path (Quiver.Symmetrify α) _ u v) :
32     vertex u ⟶ vertex v :=
33   (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map p
34 
35 @[simp] theorem pathClass_nil (r : α) :
36     pathClass (@Quiver.Path.nil (Quiver.Symmetrify α) _ r) = 𝟙 (vertex r) := rfl
37 
38 @[simp] theorem pathClass_comp {u v w : α}
39     (p : @Quiver.Path (Quiver.Symmetrify α) _ u v)
40     (q : @Quiver.Path (Quiver.Symmetrify α) _ v w) :
41     pathClass (p.comp q) = pathClass p ≫ pathClass q := rfl
42 
43 @[simp] theorem pathClass_reverse {u v : α}
44     (p : @Quiver.Path (Quiver.Symmetrify α) _ u v) :
45     pathClass p.reverse = Groupoid.inv (pathClass p) := rfl
46 
47 /-- Every morphism of the graph groupoid is represented by an actual path. -/
48 theorem pathClass_surjective (u v : α) :
49     Function.Surjective (@pathClass α _ u v) :=
50   (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).map_surjective
51 
52 /-- The group of actual reduced loops based at `r`. -/
53 abbrev Loop (r : α) := CategoryTheory.End (vertex r)
54 
55 /-- A based path as an element of the reduced loop group. -/
56 def loopClass {r : α} (p : @Quiver.Path (Quiver.Symmetrify α) _ r r) : Loop r :=
57   pathClass p
58 
59 @[simp] theorem loopClass_nil (r : α) :
60     loopClass (@Quiver.Path.nil (Quiver.Symmetrify α) _ r) = 1 := rfl
61 
62 /-- Multiplication follows function composition, so path concatenation reverses its order. -/
63 @[simp] theorem loopClass_comp {r : α}
64     (p q : @Quiver.Path (Quiver.Symmetrify α) _ r r) :
65     loopClass (p.comp q) = loopClass q * loopClass p := rfl
66 
67 @[simp] theorem loopClass_reverse {r : α}
68     (p : @Quiver.Path (Quiver.Symmetrify α) _ r r) :
69     loopClass p.reverse = (loopClass p)⁻¹ := rfl
70 
71 theorem loopClass_surjective (r : α) :
72     Function.Surjective (@loopClass α _ r) := pathClass_surjective r r
73 
74 /-- The first combinatorial homology group, defined as the abelianization of reduced loops. -/
75 abbrev H1 (r : α) := Abelianization (Loop r)
76 
77 /-- The canonical homomorphism from reduced loops to their abelianization. -/
78 def homologyClass (r : α) : Loop r →* H1 r := Abelianization.of
79 
80 @[simp] theorem homologyClass_mul (r : α) (x y : Loop r) :
81     homologyClass r (x * y) = homologyClass r x * homologyClass r y := rfl
82 
83 /-- Abelian characters of reduced loops are exactly characters of `H1`. -/
84 def factorCharacter (r : α) (C : Type w) [CommGroup C] :
85     (Loop r →* C) ≃ (H1 r →* C) := Abelianization.lift
86 
87 @[simp] theorem factorCharacter_apply_class {r : α} {C : Type w} [CommGroup C]
88     (χ : Loop r →* C) (x : Loop r) :
89     factorCharacter r C χ (homologyClass r x) = χ x := rfl
90 
91 /-- The character factorization is unique, including its values away from chosen loops. -/
92 theorem factorCharacter_unique {r : α} {C : Type w} [CommGroup C]
93     (χ : Loop r →* C) (ψ : H1 r →* C)
94     (h : ∀ x, ψ (homologyClass r x) = χ x) : ψ = factorCharacter r C χ := by
95   ext x
96   exact Abelianization.lift_unique χ ψ h
97 
98 /-- Equality on represented paths suffices for equality of loop homomorphisms. -/
99 theorem character_ext_paths {r : α} {C : Type w} [Monoid C]
100     (χ ψ : Loop r →* C)
101     (h : ∀ p, χ (loopClass p) = ψ (loopClass p)) : χ = ψ := by
102   ext x
103   obtain ⟨p, rfl⟩ := loopClass_surjective r x
104   exact h p
105 
106 end PaperXI.GraphLoop

Back to source controls