Comparison of combinatorial and topological fundamental groups

This module identifies the free-groupoid computation with the fundamental group of the realization.

def FiniteGraphFreeGroup.coverSymPathValue {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) : (graphCoverSymmetricFreeGroupoidMap root).obj a ⟶ (graphCoverSymmetricFreeGroupoidMap root).obj b

Evaluates a symmetric path in the canonical cover as a base free-groupoid morphism.

Equations

• FiniteGraphFreeGroup.coverSymPathValue p = (CategoryTheory.Paths.lift (FiniteGraphFreeGroup.graphCoverSymmetricFreeGroupoidMap root)).map p

theorem FiniteGraphFreeGroup.coverSymPathValue_cons {V : Type u} [Quiver V] {root : V} {a b c : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) (e : b ⟶ c) : coverSymPathValue (p.cons e) = CategoryTheory.CategoryStruct.comp (coverSymPathValue p) ((graphCoverSymmetricFreeGroupoidMap root).map e)

theorem FiniteGraphFreeGroup.graphCoverSymmetricFreeGroupoidMap_endpoint {V : Type u} [Quiver V] {root : V} {y z : Quiver.Symmetrify (graphCoverVertex root)} (e : y ⟶ z) : z.snd = CategoryTheory.CategoryStruct.comp y.snd ((graphCoverSymmetricFreeGroupoidMap root).map e)

theorem FiniteGraphFreeGroup.coverSymPathValue_endpoint {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (p : Quiver.Path (graphCoverRootVertex root) x) : x.snd = coverSymPathValue p

@[reducible, inline]

abbrev FiniteGraphFreeGroup.baseSymPathValue {V : Type u} [Quiver V] {a b : Quiver.Symmetrify V} (p : Quiver.Path a b) : (Quiver.FreeGroupoid.of V).obj a ⟶ (Quiver.FreeGroupoid.of V).obj b

Evaluates a symmetric path in the base graph's free groupoid.

Equations

• FiniteGraphFreeGroup.baseSymPathValue p = Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep) p

theorem FiniteGraphFreeGroup.coverSymPathValue_eq_baseSymPathValue {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) : coverSymPathValue p = baseSymPathValue ((graphCoverProjection root).symmetrify.mapPath p)

def FiniteGraphFreeGroup.graphFreeGroupPrefunctor {V : Type u} [Quiver V] : V ⥤q CategoryTheory.SingleObj (FreeGroup (Quiver.Total V))

Sends every graph edge to its generator in the free group on total edges.

Equations

• FiniteGraphFreeGroup.graphFreeGroupPrefunctor = { obj := fun (x : V) => (), map := fun {X Y : V} (e : X ⟶ Y) => FreeGroup.of { left := X, right := Y, hom := e } }

@[reducible, inline]

abbrev FiniteGraphFreeGroup.singleObjHomValue {M : Type u} {x y : CategoryTheory.SingleObj M} (f : x ⟶ y) : M

Extracts the monoid value represented by a morphism in a one-object category.

Equations

• FiniteGraphFreeGroup.singleObjHomValue f = f

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphFreeGroupoidToFreeGroup {V : Type u} [Quiver V] : CategoryTheory.Functor (Quiver.FreeGroupoid V) (CategoryTheory.SingleObj (FreeGroup (Quiver.Total V)))

The functor from the free graph groupoid to the free group on total edges.

Equations

• FiniteGraphFreeGroup.graphFreeGroupoidToFreeGroup = Quiver.FreeGroupoid.lift FiniteGraphFreeGroup.graphFreeGroupPrefunctor

def FiniteGraphFreeGroup.coverSymEdgeLetter {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (e : a ⟶ b) : Quiver.Total V × Bool

The signed base-edge letter represented by an edge of the symmetric cover.

Equations

• One or more equations did not get rendered due to their size.

def FiniteGraphFreeGroup.coverSymPathWord {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) : List (Quiver.Total V × Bool)

The signed base-edge word represented by a path in the symmetric cover.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.coverSymPathWord_cons {V : Type u} [Quiver V] {root : V} {a b c : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) (e : b ⟶ c) : coverSymPathWord (p.cons e) = coverSymEdgeLetter e :: coverSymPathWord p

inductive FiniteGraphFreeGroup.symPathNoBacktrack {W : Type u} [Quiver W] {a b : Quiver.Symmetrify W} : Quiver.Path a b → Prop

Paths in a symmetrified quiver that never immediately traverse an edge and its reverse.

• nil {W : Type u} [Quiver W] {a : Quiver.Symmetrify W} : symPathNoBacktrack Quiver.Path.nil
• cons {W : Type u} [Quiver W] {a b c : Quiver.Symmetrify W} (p : Quiver.Path a b) (e : b ⟶ c) : symPathNoBacktrack p → (∀ {d : Quiver.Symmetrify W} (q : Quiver.Path a d) (f : d ⟶ b), p = q.cons f → { left := b, right := c, hom := e } ≠ { left := b, right := d, hom := Quiver.reverse f }) → symPathNoBacktrack (p.cons e)

theorem FiniteGraphFreeGroup.symPathNoBacktrack_of_shortest {W : Type u} [Quiver W] {r a : Quiver.Symmetrify W} (p : Quiver.Path r a) (hshort : ∀ (q : Quiver.Path r a), p.length ≤ q.length) : symPathNoBacktrack p

theorem FiniteGraphFreeGroup.coverSymEdgeLetter_cancel {V : Type u} [Quiver V] {root : V} {a b c : Quiver.Symmetrify (graphCoverVertex root)} (f : a ⟶ b) (e : b ⟶ c) (hbase : (coverSymEdgeLetter e).1 = (coverSymEdgeLetter f).1) (hbool : (coverSymEdgeLetter e).2 = !(coverSymEdgeLetter f).2) : { left := b, right := c, hom := e } = { left := b, right := a, hom := Quiver.reverse f }

theorem FiniteGraphFreeGroup.coverSymPathWord_isReduced {V : Type u} [Quiver V] {root : V} {a : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path (graphCoverRootVertex root) a) (hp : symPathNoBacktrack p) : FreeGroup.IsReduced (coverSymPathWord p)

@[reducible, inline]

abbrev FiniteGraphFreeGroup.coverFreeGroupValue {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) : FreeGroup (Quiver.Total V)

Evaluates a symmetric cover path in the free group on base edges.

Equations

• FiniteGraphFreeGroup.coverFreeGroupValue p = FiniteGraphFreeGroup.singleObjHomValue (FiniteGraphFreeGroup.graphFreeGroupoidToFreeGroup.map (FiniteGraphFreeGroup.coverSymPathValue p))

theorem FiniteGraphFreeGroup.coverFreeGroupValue_nil {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) : coverFreeGroupValue Quiver.Path.nil = 1

theorem FiniteGraphFreeGroup.coverFreeGroupValue_cons {V : Type u} [Quiver V] {root : V} {a b c : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) (e : b ⟶ c) : coverFreeGroupValue (p.cons e) = singleObjHomValue (graphFreeGroupoidToFreeGroup.map ((graphCoverSymmetricFreeGroupoidMap root).map e)) * coverFreeGroupValue p

theorem FiniteGraphFreeGroup.graphFreeGroupoidToFreeGroup_map_pos {V : Type u} [Quiver V] (e : Quiver.Total V) : singleObjHomValue (graphFreeGroupoidToFreeGroup.map ((Quiver.FreeGroupoid.of V).map e.hom)) = FreeGroup.of e

theorem FiniteGraphFreeGroup.coverFreeGroupMap_letter {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (e : a ⟶ b) : singleObjHomValue (graphFreeGroupoidToFreeGroup.map ((graphCoverSymmetricFreeGroupoidMap root).map e)) = FreeGroup.mk [coverSymEdgeLetter e]

theorem FiniteGraphFreeGroup.coverFreeGroupValue_cons_letter {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path (graphCoverRootVertex root) a) (e : a ⟶ b) : coverFreeGroupValue (p.cons e) = FreeGroup.mk [coverSymEdgeLetter e] * coverFreeGroupValue p

theorem FiniteGraphFreeGroup.coverFreeGroupValue_eq_word {V : Type u} [Quiver V] {root : V} {a : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path (graphCoverRootVertex root) a) : coverFreeGroupValue p = FreeGroup.mk (coverSymPathWord p)

theorem FiniteGraphFreeGroup.coverSymPathWord_length {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path a b) : (coverSymPathWord p).length = p.length

theorem FiniteGraphFreeGroup.coverFreeGroupValue_eq_of_endpoint {V : Type u} [Quiver V] {root : V} {a : Quiver.Symmetrify (graphCoverVertex root)} (p q : Quiver.Path (graphCoverRootVertex root) a) : coverFreeGroupValue p = coverFreeGroupValue q

theorem FiniteGraphFreeGroup.coverSymEdge_star_eq_of_letter_eq {V : Type u} [Quiver V] {root : V} {a b c : Quiver.Symmetrify (graphCoverVertex root)} (e : a ⟶ b) (f : a ⟶ c) (h : coverSymEdgeLetter e = coverSymEdgeLetter f) : ⟨b, e⟩ = ⟨c, f⟩

theorem FiniteGraphFreeGroup.coverSymEdge_eq_of_letter_eq {V : Type u} [Quiver V] {root : V} {a b c : Quiver.Symmetrify (graphCoverVertex root)} (e : a ⟶ b) (f : a ⟶ c) (h : coverSymEdgeLetter e = coverSymEdgeLetter f) : e ≍ f

theorem FiniteGraphFreeGroup.coverSymPathStar_eq_of_word_eq {V : Type u} [Quiver V] {root : V} {a b : Quiver.Symmetrify (graphCoverVertex root)} (p : Quiver.Path (graphCoverRootVertex root) a) (q : Quiver.Path (graphCoverRootVertex root) b) (h : coverSymPathWord p = coverSymPathWord q) : ⟨a, p⟩ = ⟨b, q⟩

theorem FiniteGraphFreeGroup.coverSymPath_eq_of_same_endpoint_of_noBacktrack {V : Type u} [Quiver V] {root : V} {a : Quiver.Symmetrify (graphCoverVertex root)} (p q : Quiver.Path (graphCoverRootVertex root) a) (hp : symPathNoBacktrack p) (hq : symPathNoBacktrack q) : p = q

theorem FiniteGraphFreeGroup.graphCoverSymmetric_rootedConnected {V : Type u} [Quiver V] (root : V) : Quiver.RootedConnected (graphCoverRootVertex root)

instance FiniteGraphFreeGroup.graphCoverSymmetricRootedConnected {V : Type u} [Quiver V] (root : V) : Quiver.RootedConnected (graphCoverRootVertex root)

noncomputable def FiniteGraphFreeGroup.graphCoverSymmetricTree {V : Type u} [Quiver V] (root : V) : WideSubquiver (Quiver.Symmetrify (graphCoverVertex root))

The canonical geodesic spanning tree of the symmetrified graph cover.

Equations

• FiniteGraphFreeGroup.graphCoverSymmetricTree root = Quiver.geodesicSubtree (FiniteGraphFreeGroup.graphCoverRootVertex root)

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.graphCoverSymmetricTreeArborescence {V : Type u} [Quiver V] (root : V) : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))

Equations

• FiniteGraphFreeGroup.graphCoverSymmetricTreeArborescence root = id (Quiver.geodesicArborescence (FiniteGraphFreeGroup.graphCoverRootVertex root))

theorem FiniteGraphFreeGroup.graphCoverSymmetric_edge_or_reverse_mem_tree {V : Type u} [Quiver V] (root : V) {a b : Quiver.Symmetrify (graphCoverVertex root)} (e : a ⟶ b) : e ∈ graphCoverSymmetricTree root a b ∨ Quiver.reverse e ∈ graphCoverSymmetricTree root b a

def FiniteGraphFreeGroup.graphRealizationSignedPreMap {U W : Type u} [Quiver U] [Quiver W] (f : U → W) (g : Quiver.Total U → Quiver.Total W) (r : Quiver.Total U → C(↑unitInterval, ↑unitInterval)) : graphRealizationPre U → graphRealizationPre W

The representative-level realization map induced by a signed edge map.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.graphRealizationSignedPreMap_continuous {U W : Type u} [Quiver U] [Quiver W] (f : U → W) (g : Quiver.Total U → Quiver.Total W) (r : Quiver.Total U → C(↑unitInterval, ↑unitInterval)) : Continuous (graphRealizationSignedPreMap f g r)

def FiniteGraphFreeGroup.graphRealizationSignedMap {U W : Type u} [Quiver U] [Quiver W] (f : U → W) (g : Quiver.Total U → Quiver.Total W) (r : Quiver.Total U → C(↑unitInterval, ↑unitInterval)) (h0 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 0⟩) = graphVertex (f e.left)) (h1 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 1⟩) = graphVertex (f e.right)) : graphRealization U → graphRealization W

The continuous realization map induced by a signed edge map.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.continuous_graphRealizationSignedMap {U W : Type u} [Quiver U] [Quiver W] (f : U → W) (g : Quiver.Total U → Quiver.Total W) (r : Quiver.Total U → C(↑unitInterval, ↑unitInterval)) (h0 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 0⟩) = graphVertex (f e.left)) (h1 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 1⟩) = graphVertex (f e.right)) : Continuous (graphRealizationSignedMap f g r h0 h1)

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationSignedMap_vertex {U W : Type u} [Quiver U] [Quiver W] (f : U → W) (g : Quiver.Total U → Quiver.Total W) (r : Quiver.Total U → C(↑unitInterval, ↑unitInterval)) (h0 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 0⟩) = graphVertex (f e.left)) (h1 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 1⟩) = graphVertex (f e.right)) (v : U) : graphRealizationSignedMap f g r h0 h1 (graphVertex v) = graphVertex (f v)

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationSignedMap_edgePath {U W : Type u} [Quiver U] [Quiver W] (f : U → W) (g : Quiver.Total U → Quiver.Total W) (r : Quiver.Total U → C(↑unitInterval, ↑unitInterval)) (h0 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 0⟩) = graphVertex (f e.left)) (h1 : ∀ (e : Quiver.Total U), graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (g e), (r e) 1⟩) = graphVertex (f e.right)) (e : Quiver.Total U) (t : ↑unitInterval) : graphRealizationSignedMap f g r h0 h1 ((graphEdgePath e) t) = (graphEdgePath (g e)) ((r e) t)

def FiniteGraphFreeGroup.graphCoverTreeEdgeBase {V : Type u} [Quiver V] (root : V) (d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) : Quiver.Total (graphCoverVertex root)

The underlying cover edge represented by an edge of the symmetric cover tree.

Equations

• One or more equations did not get rendered due to their size.

def FiniteGraphFreeGroup.graphCoverTreeEdgeSign {V : Type u} [Quiver V] (root : V) (d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) : Bool

The orientation of a symmetric cover-tree edge relative to its underlying cover edge.

Equations

• One or more equations did not get rendered due to their size.

def FiniteGraphFreeGroup.graphCoverTreeEdgeChoiceProperty {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) (d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) : Prop

The specification for choosing the symmetric tree edge above an underlying cover edge.

Equations

• FiniteGraphFreeGroup.graphCoverTreeEdgeChoiceProperty root e d = (FiniteGraphFreeGroup.graphCoverTreeEdgeBase root d = e)

theorem FiniteGraphFreeGroup.graphCoverTreeEdgeChoice_exists {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) : Nonempty { d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root)) // graphCoverTreeEdgeChoiceProperty root e d }

noncomputable def FiniteGraphFreeGroup.graphCoverTreeEdgeChoice {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))

Chooses a symmetric tree edge above an underlying cover edge.

Equations

• FiniteGraphFreeGroup.graphCoverTreeEdgeChoice root e = ↑(Classical.choice ⋯)

theorem FiniteGraphFreeGroup.graphCoverTreeEdgeChoice_base {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) : graphCoverTreeEdgeBase root (graphCoverTreeEdgeChoice root e) = e

def FiniteGraphFreeGroup.graphCoverTreeVertexForget {V : Type u} [Quiver V] (root : V) (v : WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root)) : graphCoverVertex root

Forgets membership in the symmetric cover tree from a tree vertex.

Equations

• FiniteGraphFreeGroup.graphCoverTreeVertexForget root v = id (fun (v : FiniteGraphFreeGroup.graphCoverVertex root) => v) v

def FiniteGraphFreeGroup.graphRealizationIntervalSymm : C(↑unitInterval, ↑unitInterval)

The continuous orientation-reversing involution of the unit interval.

Equations

• FiniteGraphFreeGroup.graphRealizationIntervalSymm = { toFun := unitInterval.symm, continuous_toFun := unitInterval.continuous_symm }

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationIntervalSymm_apply (t : ↑unitInterval) : graphRealizationIntervalSymm t = unitInterval.symm t

theorem FiniteGraphFreeGroup.graphRealizationIntervalSymm_zero : graphRealizationIntervalSymm 0 = 1

theorem FiniteGraphFreeGroup.graphRealizationIntervalSymm_one : graphRealizationIntervalSymm 1 = 0

theorem FiniteGraphFreeGroup.graphRealizationIntervalSymm_symm (t : ↑unitInterval) : graphRealizationIntervalSymm (graphRealizationIntervalSymm t) = t

def FiniteGraphFreeGroup.graphCoverTreeFoldCoordinate {V : Type u} [Quiver V] (root : V) (d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) : C(↑unitInterval, ↑unitInterval)

The interval coordinate used when folding the symmetric cover tree into the cover.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.graphCoverTreeFoldCoordinate_positive {V : Type u} [Quiver V] (root : V) {a b : graphCoverVertex root} (e : a ⟶ b) (h : Sum.inl e ∈ graphCoverSymmetricTree root a b) : graphCoverTreeFoldCoordinate root { left := a, right := b, hom := ⟨Sum.inl e, h⟩ } = ContinuousMap.id ↑unitInterval

theorem FiniteGraphFreeGroup.graphCoverTreeFoldCoordinate_negative {V : Type u} [Quiver V] (root : V) {a b : graphCoverVertex root} (e : a ⟶ b) (h : Sum.inr e ∈ graphCoverSymmetricTree root b a) : graphCoverTreeFoldCoordinate root { left := b, right := a, hom := ⟨Sum.inr e, h⟩ } = graphRealizationIntervalSymm

theorem FiniteGraphFreeGroup.graphCoverTreeFold_h0 {V : Type u} [Quiver V] (root : V) (d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) : graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (graphCoverTreeEdgeBase root d), (graphCoverTreeFoldCoordinate root d) 0⟩) = graphVertex (graphCoverTreeVertexForget root d.left)

theorem FiniteGraphFreeGroup.graphCoverTreeFold_h1 {V : Type u} [Quiver V] (root : V) (d : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) : graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (graphCoverTreeEdgeBase root d), (graphCoverTreeFoldCoordinate root d) 1⟩) = graphVertex (graphCoverTreeVertexForget root d.right)

noncomputable def FiniteGraphFreeGroup.graphCoverTreeToCover {V : Type u} [Quiver V] (root : V) : graphRealization (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root)) → graphRealization (graphCoverVertex root)

The realization map folding the symmetric cover tree onto the canonical cover.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.continuous_graphCoverTreeToCover {V : Type u} [Quiver V] (root : V) : Continuous (graphCoverTreeToCover root)

@[simp]

theorem FiniteGraphFreeGroup.graphCoverTreeToCover_vertex {V : Type u} [Quiver V] (root : V) (v : WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root)) : graphCoverTreeToCover root (graphVertex v) = graphVertex (graphCoverTreeVertexForget root v)

@[simp]

theorem FiniteGraphFreeGroup.graphCoverTreeToCover_edgePath {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) (t : ↑unitInterval) : graphCoverTreeToCover root ((graphEdgePath e) t) = (graphEdgePath (graphCoverTreeEdgeBase root e)) ((graphCoverTreeFoldCoordinate root e) t)

def FiniteGraphFreeGroup.graphCoverVertexEmbed {V : Type u} [Quiver V] (root : V) (v : graphCoverVertex root) : WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root)

Embeds a canonical-cover vertex into the symmetric cover tree.

Equations

• FiniteGraphFreeGroup.graphCoverVertexEmbed root v = v

noncomputable def FiniteGraphFreeGroup.graphCoverSectionCoordinate {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) : C(↑unitInterval, ↑unitInterval)

The signed interval coordinate used by the section from the cover to its tree model.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.graphCoverSectionCoordinate_positive {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) (h : graphCoverTreeEdgeSign root (graphCoverTreeEdgeChoice root e) = true) : graphCoverSectionCoordinate root e = ContinuousMap.id ↑unitInterval

theorem FiniteGraphFreeGroup.graphCoverSectionCoordinate_negative {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) (h : graphCoverTreeEdgeSign root (graphCoverTreeEdgeChoice root e) = false) : graphCoverSectionCoordinate root e = graphRealizationIntervalSymm

theorem FiniteGraphFreeGroup.graphCoverSection_h0 {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) : graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (graphCoverTreeEdgeChoice root e), (graphCoverSectionCoordinate root e) 0⟩) = graphVertex (graphCoverVertexEmbed root e.left)

theorem FiniteGraphFreeGroup.graphCoverSection_h1 {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) : graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge (graphCoverTreeEdgeChoice root e), (graphCoverSectionCoordinate root e) 1⟩) = graphVertex (graphCoverVertexEmbed root e.right)

noncomputable def FiniteGraphFreeGroup.graphCoverToTree {V : Type u} [Quiver V] (root : V) : graphRealization (graphCoverVertex root) → graphRealization (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))

A continuous section from the canonical cover realization to its symmetric tree model.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.continuous_graphCoverToTree {V : Type u} [Quiver V] (root : V) : Continuous (graphCoverToTree root)

@[simp]

theorem FiniteGraphFreeGroup.graphCoverToTree_vertex {V : Type u} [Quiver V] (root : V) (v : graphCoverVertex root) : graphCoverToTree root (graphVertex v) = graphVertex (graphCoverVertexEmbed root v)

@[simp]

theorem FiniteGraphFreeGroup.graphCoverToTree_edgePath {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) (t : ↑unitInterval) : graphCoverToTree root ((graphEdgePath e) t) = (graphEdgePath (graphCoverTreeEdgeChoice root e)) ((graphCoverSectionCoordinate root e) t)

theorem FiniteGraphFreeGroup.graphRealization_map_ext {U W : Type u} [Quiver U] [Quiver W] (F G : graphRealization U → graphRealization W) (hv : ∀ (v : U), F (graphVertex v) = G (graphVertex v)) (he : ∀ (e : Quiver.Total U) (t : ↑unitInterval), F ((graphEdgePath e) t) = G ((graphEdgePath e) t)) : F = G

theorem FiniteGraphFreeGroup.graphCoverTreeVertexForget_embed {V : Type u} [Quiver V] (root : V) (v : graphCoverVertex root) : graphCoverTreeVertexForget root (graphCoverVertexEmbed root v) = v

theorem FiniteGraphFreeGroup.graphCoverTreeToCover_comp_graphCoverToTree {V : Type u} [Quiver V] (root : V) : graphCoverTreeToCover root ∘ graphCoverToTree root = id

theorem FiniteGraphFreeGroup.graphCoverTreeEdgeBase_injective {V : Type u} [Quiver V] (root : V) (d₁ d₂ : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root))) (h : graphCoverTreeEdgeBase root d₁ = graphCoverTreeEdgeBase root d₂) : d₁ = d₂

theorem FiniteGraphFreeGroup.graphCoverToTree_comp_graphCoverTreeToCover {V : Type u} [Quiver V] (root : V) : graphCoverToTree root ∘ graphCoverTreeToCover root = id

noncomputable def FiniteGraphFreeGroup.graphCoverRealizationHomotopyEquiv {V : Type u} [Quiver V] (root : V) : ContinuousMap.HomotopyEquiv (graphRealization (graphCoverVertex root)) (graphRealization (WideSubquiver.toType (Quiver.Symmetrify (graphCoverVertex root)) (graphCoverSymmetricTree root)))

The homotopy equivalence between the canonical cover and its symmetric spanning tree.

Equations

• One or more equations did not get rendered due to their size.

instance FiniteGraphFreeGroup.graphCoverRealization_contractible {V : Type u} [Quiver V] (root : V) : ContractibleSpace (graphRealization (graphCoverVertex root))

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphBaseSymPathValue {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : (Quiver.FreeGroupoid.of V).obj a ⟶ (Quiver.FreeGroupoid.of V).obj b

Evaluates a symmetric base-graph path in the free graph groupoid.

Equations

• FiniteGraphFreeGroup.graphBaseSymPathValue p = FiniteGraphFreeGroup.baseSymPathValue p

theorem FiniteGraphFreeGroup.graphFreeGroupoidToTopological_map_path {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : graphFreeGroupoidToTopological.map (graphBaseSymPathValue p) = FundamentalGroupoid.fromPath (Path.Homotopic.Quotient.mk (graphRealizationQuiverPath p))

theorem FiniteGraphFreeGroup.graphCoverRealization_fiber_vertex {V : Type u} [Quiver V] (root : V) {z : graphCoverRealization root} (hz : graphCoverRealizationProjection root z = graphVertex root) : ∃ (x : graphCoverVertex root), z = graphVertex x ∧ x.fst = root

theorem FiniteGraphFreeGroup.graphCoverRealizationQuiverPath_map {V : Type u} [Quiver V] (root : V) {a b : graphCoverVertex root} (p : Quiver.Path a b) : (graphRealizationQuiverPath p).map ⋯ = graphRealizationQuiverPath ((graphCoverProjection root).symmetrify.mapPath p)

def FiniteGraphFreeGroup.graphCoverRootFiberPoint {V : Type u} [Quiver V] (root : V) : ↑(graphCoverRealizationProjection root ⁻¹' {graphVertex root})

The distinguished point in the covering fiber over the realized root vertex.

Equations

• FiniteGraphFreeGroup.graphCoverRootFiberPoint root = ⟨FiniteGraphFreeGroup.graphVertex (FiniteGraphFreeGroup.graphCoverRootVertex root), ⋯⟩

theorem FiniteGraphFreeGroup.graphRealizationQuiverPath_cast {W : Type u} [Quiver W] {a b a' b' : W} (ha : a = a') (hb : b = b') (p : Quiver.Path a b) : graphRealizationQuiverPath (Quiver.Path.cast ha hb p) = (graphRealizationQuiverPath p).cast ⋯ ⋯

theorem FiniteGraphFreeGroup.graphCombinatorialToTopological_surjective_of_path {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) (γ : Path (graphVertex root) (graphVertex root)) : ∃ (p : Quiver.Path (have this := root; this) root), (graphCombinatorialToTopological root) (graphBaseSymPathValue p) = FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)

theorem FiniteGraphFreeGroup.graphCombinatorialToTopological_surjective {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : Function.Surjective ⇑(graphCombinatorialToTopological root)

theorem FiniteGraphFreeGroup.baseSymPathValue_cast_heq {V : Type u} [Quiver V] {a b a' b' : Quiver.Symmetrify V} (ha : a = a') (hb : b = b') (p : Quiver.Path a b) : baseSymPathValue (Quiver.Path.cast ha hb p) ≍ baseSymPathValue p

theorem FiniteGraphFreeGroup.graphCombinatorialToTopological_injective {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : Function.Injective ⇑(graphCombinatorialToTopological root)

noncomputable def FiniteGraphFreeGroup.graphCombinatorialToTopologicalEquiv {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : graphFundamentalGroup root ≃* FundamentalGroup (graphRealization V) (graphVertex root)

The explicit isomorphism between combinatorial and topological graph fundamental groups.

Equations

• FiniteGraphFreeGroup.graphCombinatorialToTopologicalEquiv root = MulEquiv.ofBijective (FiniteGraphFreeGroup.graphCombinatorialToTopological root) ⋯

noncomputable def FiniteGraphFreeGroup.graphTopologicalFundamentalGroupEquiv {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : FundamentalGroup (graphRealization V) (graphVertex root) ≃* FreeGroup (Fin cycleRank)

Identifies a finite connected graph's topological fundamental group with a free group.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteGraphFreeGroup.proved_topological_fundamental_group_free_rank {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Nonempty (FundamentalGroup (graphRealization V) (graphVertex root) ≃* FreeGroup (Fin (edgeCount + 1 - vertexCount)))