Geometric realization of a finite quiver

This module realizes vertices discretely and every directed edge as a separate interval cell.

A geometric realization of a finite quiver

The combinatorial development works with a quiver and its free groupoid. The construction in this file supplies the missing topological object: every directed edge gets a copy of the unit interval, and its two endpoints are identified with the source and target vertices. Parallel edges and loops are kept as distinct interval cells.

The quotient topology is the standard weak topology on this finite one- dimensional cell complex. The fundamental-group comparison is developed in the later lemmas; the definitions here are intentionally independent of any choice of spanning tree.

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphRealizationPre (V : Type u) [Quiver V] : Type u

The disjoint union of discrete vertices and one interval for each edge.

Equations

• FiniteGraphFreeGroup.graphRealizationPre V = (WithDiscreteTopology V ⊕ (_ : WithDiscreteTopology (Quiver.Total V)) × ↑unitInterval)

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphDiscreteVertex {V : Type u} (v : V) : WithDiscreteTopology V

A graph vertex regarded as a point of the discrete vertex space.

Equations

• FiniteGraphFreeGroup.graphDiscreteVertex v = WithTopology.toTopology ⊥ v

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphDiscreteEdge {V : Type u} [Quiver V] (e : Quiver.Total V) : WithDiscreteTopology (Quiver.Total V)

A graph edge regarded as a point of the discrete total-edge space.

Equations

• FiniteGraphFreeGroup.graphDiscreteEdge e = WithTopology.toTopology ⊥ e

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphVertexUnderlying {V : Type u} (v : WithDiscreteTopology V) : V

Forgets the discrete topology from a graph vertex.

Equations

• FiniteGraphFreeGroup.graphVertexUnderlying v = v.ofTopology

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphEdgeUnderlying {V : Type u} [Quiver V] (e : WithDiscreteTopology (Quiver.Total V)) : Quiver.Total V

Forgets the discrete topology from a total graph edge.

Equations

• FiniteGraphFreeGroup.graphEdgeUnderlying e = e.ofTopology

inductive FiniteGraphFreeGroup.graphRealizationGenerator {V : Type u} [Quiver V] : graphRealizationPre V → graphRealizationPre V → Prop

The endpoint identifications used to form the geometric realization.

• source {V : Type u} [Quiver V] (e : Quiver.Total V) : graphRealizationGenerator (Sum.inr ⟨graphDiscreteEdge e, 0⟩) (Sum.inl (graphDiscreteVertex e.left))
• target {V : Type u} [Quiver V] (e : Quiver.Total V) : graphRealizationGenerator (Sum.inr ⟨graphDiscreteEdge e, 1⟩) (Sum.inl (graphDiscreteVertex e.right))

@[instance_reducible]

instance FiniteGraphFreeGroup.graphRealizationSetoid {V : Type u} [Quiver V] : Setoid (graphRealizationPre V)

The equivalence relation generated by the two endpoint identifications.

Equations

• FiniteGraphFreeGroup.graphRealizationSetoid = Relation.EqvGen.setoid FiniteGraphFreeGroup.graphRealizationGenerator

The endpoint label is an invariant of the quotient relation. Besides separating vertices, this records why no edge cell is accidentally glued to a vertex away from its two prescribed endpoints.

noncomputable def FiniteGraphFreeGroup.graphRealizationEndpointLabel {V : Type u} [Quiver V] : graphRealizationPre V → Option V

Labels the two endpoints of an edge interval and leaves interior points unlabeled.

Equations

• One or more equations did not get rendered due to their size.
• FiniteGraphFreeGroup.graphRealizationEndpointLabel (Sum.inl v) = some (FiniteGraphFreeGroup.graphVertexUnderlying v)

theorem FiniteGraphFreeGroup.graphRealizationGenerator_endpointLabel {V : Type u} [Quiver V] {x y : graphRealizationPre V} (h : graphRealizationGenerator x y) : graphRealizationEndpointLabel x = graphRealizationEndpointLabel y

theorem FiniteGraphFreeGroup.graphRealization_eqvGen_endpointLabel {V : Type u} [Quiver V] {x y : graphRealizationPre V} (h : Relation.EqvGen graphRealizationGenerator x y) : graphRealizationEndpointLabel x = graphRealizationEndpointLabel y

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphRealization (V : Type u) [Quiver V] : Type u

The geometric realization of a finite directed multigraph.

Equations

• FiniteGraphFreeGroup.graphRealization V = Quotient FiniteGraphFreeGroup.graphRealizationSetoid

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphRealizationQuotient {V : Type u} [Quiver V] : graphRealizationPre V → graphRealization V

The quotient map from the disjoint union of cells.

Equations

• FiniteGraphFreeGroup.graphRealizationQuotient = Quotient.mk'

def FiniteGraphFreeGroup.graphVertex {V : Type u} [Quiver V] (v : V) : graphRealization V

The point of the realization corresponding to a vertex.

Equations

• FiniteGraphFreeGroup.graphVertex v = FiniteGraphFreeGroup.graphRealizationQuotient (Sum.inl (FiniteGraphFreeGroup.graphDiscreteVertex v))

noncomputable def FiniteGraphFreeGroup.graphRealizationEndpointLabelQuotient {V : Type u} [Quiver V] : graphRealization V → Option V

The endpoint label descends to the quotient as a set-theoretic invariant.

Equations

• FiniteGraphFreeGroup.graphRealizationEndpointLabelQuotient = Quotient.lift FiniteGraphFreeGroup.graphRealizationEndpointLabel ⋯

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationEndpointLabelQuotient_mk {V : Type u} [Quiver V] (x : graphRealizationPre V) : graphRealizationEndpointLabelQuotient (graphRealizationQuotient x) = graphRealizationEndpointLabel x

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationEndpointLabelQuotient_vertex {V : Type u} [Quiver V] (v : V) : graphRealizationEndpointLabelQuotient (graphVertex v) = some v

theorem FiniteGraphFreeGroup.graphRealization_isOpen_iff {V : Type u} [Quiver V] {s : Set (graphRealization V)} : IsOpen s ↔ IsOpen (graphRealizationQuotient ⁻¹' s)

theorem FiniteGraphFreeGroup.graphRealization_image_preimage_eq_of_saturated {V : Type u} [Quiver V] {s : Set (graphRealizationPre V)} (hs : ∀ {x y : graphRealizationPre V}, Relation.EqvGen graphRealizationGenerator x y → (x ∈ s ↔ y ∈ s)) : graphRealizationQuotient ⁻¹' graphRealizationQuotient '' s = s

theorem FiniteGraphFreeGroup.graphRealization_image_isOpen_of_saturated {V : Type u} [Quiver V] {s : Set (graphRealizationPre V)} (hs : ∀ {x y : graphRealizationPre V}, Relation.EqvGen graphRealizationGenerator x y → (x ∈ s ↔ y ∈ s)) (hopen : IsOpen s) : IsOpen (graphRealizationQuotient '' s)

def FiniteGraphFreeGroup.graphEdgePath {V : Type u} [Quiver V] (e : Quiver.Total V) : C(↑unitInterval, graphRealization V)

The characteristic path of the interval cell associated to an edge.

Equations

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

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationQuotient_vertex {V : Type u} [Quiver V] (v : V) : graphRealizationQuotient (Sum.inl (graphDiscreteVertex v)) = graphVertex v

@[simp]

theorem FiniteGraphFreeGroup.graphEdgePath_zero {V : Type u} [Quiver V] (e : Quiver.Total V) : (graphEdgePath e) 0 = graphVertex e.left

@[simp]

theorem FiniteGraphFreeGroup.graphEdgePath_one {V : Type u} [Quiver V] (e : Quiver.Total V) : (graphEdgePath e) 1 = graphVertex e.right

theorem FiniteGraphFreeGroup.graphRealization_edge_interior_ne_vertex {V : Type u} [Quiver V] (e : Quiver.Total V) {t : ↑unitInterval} (ht0 : t ≠ 0) (ht1 : t ≠ 1) (v : V) : graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge e, t⟩) ≠ graphVertex v

theorem FiniteGraphFreeGroup.continuous_graphEdgePath {V : Type u} [Quiver V] (e : Quiver.Total V) : Continuous ⇑(graphEdgePath e)

def FiniteGraphFreeGroup.graphRealizationForwardPath {V : Type u} [Quiver V] {a b : V} (e : a ⟶ b) : Path (graphVertex a) (graphVertex b)

The interval cell, regarded as a path from the source to the target.

Equations

• FiniteGraphFreeGroup.graphRealizationForwardPath e = { toContinuousMap := FiniteGraphFreeGroup.graphEdgePath { left := a, right := b, hom := e }, source' := ⋯, target' := ⋯ }

def FiniteGraphFreeGroup.graphEdgeRetraction (t : ↑unitInterval) : C(↑unitInterval, ↑unitInterval)

A continuous parametrisation of the part of an interval cell from t to its source endpoint.

Equations

• FiniteGraphFreeGroup.graphEdgeRetraction t = { toFun := fun (s : ↑unitInterval) => ⟨(1 - ↑s) * ↑t, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem FiniteGraphFreeGroup.graphEdgeRetraction_zero (t : ↑unitInterval) : (graphEdgeRetraction t) 0 = t

@[simp]

theorem FiniteGraphFreeGroup.graphEdgeRetraction_one (t : ↑unitInterval) : (graphEdgeRetraction t) 1 = 0

def FiniteGraphFreeGroup.graphEdgePathToSource {V : Type u} [Quiver V] (e : Quiver.Total V) (t : ↑unitInterval) : Path ((graphEdgePath e) t) (graphVertex e.left)

The homotopy moving points of an edge interval toward its source.

Equations

• FiniteGraphFreeGroup.graphEdgePathToSource e t = { toContinuousMap := (FiniteGraphFreeGroup.graphEdgePath e).comp (FiniteGraphFreeGroup.graphEdgeRetraction t), source' := ⋯, target' := ⋯ }

theorem FiniteGraphFreeGroup.graphRealizationPre_join_vertex {V : Type u} [Quiver V] (x : graphRealizationPre V) : ∃ (v : V), Joined (graphRealizationQuotient x) (graphVertex v)

The symmetrified quiver is the combinatorial source used by the free groupoid. Its positive arrows use the characteristic interval in the forward direction, while its negative arrows use the same interval in reverse.

def FiniteGraphFreeGroup.graphRealizationSymmetricEdgePath {V : Type u} [Quiver V] {a b : V} (e : a ⟶ b) : Path (graphVertex a) (graphVertex b)

The realization path of a symmetric edge, reversing the interval when necessary.

Equations

• FiniteGraphFreeGroup.graphRealizationSymmetricEdgePath (Sum.inl e_2) = FiniteGraphFreeGroup.graphRealizationForwardPath e_2
• FiniteGraphFreeGroup.graphRealizationSymmetricEdgePath (Sum.inr e_2) = (FiniteGraphFreeGroup.graphRealizationForwardPath e_2).symm

noncomputable def FiniteGraphFreeGroup.graphRealizationQuiverPath {V : Type u} [Quiver V] {a b : V} (p : Quiver.Path a b) : Path (graphVertex a) (graphVertex b)

Concatenates realized edge paths along a quiver path.

Equations

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

theorem FiniteGraphFreeGroup.graphRealizationQuiverPath_nil {V : Type u} [Quiver V] (a : V) : graphRealizationQuiverPath Quiver.Path.nil = Path.refl (graphVertex a)

theorem FiniteGraphFreeGroup.graphRealization_pathConnected {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : PathConnectedSpace (graphRealization V)

theorem FiniteGraphFreeGroup.graphRealization_compact {V : Type u} [Quiver V] [Finite V] [FiniteQuiver V] : CompactSpace (graphRealization V)

def FiniteGraphFreeGroup.graphRealizationQuiverMap {V : Type u} [Quiver V] : V ⥤q FundamentalGroupoid (graphRealization V)

The prefunctor sending graph vertices and edges to their realization paths.

Equations

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

The universal property of Mathlib's free groupoid produces the canonical functor from the combinatorial graph groupoid into the topological fundamental groupoid of the realization.

noncomputable def FiniteGraphFreeGroup.graphFreeGroupoidToTopological {V : Type u} [Quiver V] : CategoryTheory.Functor (Quiver.FreeGroupoid V) (FundamentalGroupoid (graphRealization V))

The functor from the free graph groupoid to the realization's fundamental groupoid.

Equations

• FiniteGraphFreeGroup.graphFreeGroupoidToTopological = Quiver.FreeGroupoid.lift FiniteGraphFreeGroup.graphRealizationQuiverMap

theorem FiniteGraphFreeGroup.graphFreeGroupoidToTopological_restrict {V : Type u} [Quiver V] : Quiver.FreeGroupoid.of V ⋙q graphFreeGroupoidToTopological.toPrefunctor = graphRealizationQuiverMap

A quiver map acts on the realization cell by cell. This is the map used below for the realization of the path-lifting cover.

def FiniteGraphFreeGroup.graphRealizationPreMap {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) : graphRealizationPre V → graphRealizationPre W

The map on vertex and edge-interval representatives induced by a quiver prefunctor.

Equations

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

theorem FiniteGraphFreeGroup.graphRealizationPreMap_generator {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) {x y : graphRealizationPre V} (h : graphRealizationGenerator x y) : graphRealizationGenerator (graphRealizationPreMap F x) (graphRealizationPreMap F y)

theorem FiniteGraphFreeGroup.graphRealizationPreMap_eqvGen {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) {x y : graphRealizationPre V} (h : Relation.EqvGen graphRealizationGenerator x y) : Relation.EqvGen graphRealizationGenerator (graphRealizationPreMap F x) (graphRealizationPreMap F y)

def FiniteGraphFreeGroup.graphRealizationMap {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) : graphRealization V → graphRealization W

The continuous map of graph realizations induced by a quiver prefunctor.

Equations

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

theorem FiniteGraphFreeGroup.continuous_graphRealizationMap {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) : Continuous (graphRealizationMap F)

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationMap_vertex {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) (v : V) : graphRealizationMap F (graphVertex v) = graphVertex (F.obj v)

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationMap_edgePath {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) (e : Quiver.Total V) (t : ↑unitInterval) : graphRealizationMap F ((graphEdgePath e) t) = (graphEdgePath { left := F.obj e.left, right := F.obj e.right, hom := F.map e.hom }) t

theorem FiniteGraphFreeGroup.graphRealizationMap_forwardPath {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) {a b : V} (e : a ⟶ b) : graphRealizationMap F ∘ ⇑(graphRealizationForwardPath e) = ⇑(graphRealizationForwardPath (F.map e))

Taking the endomorphism group at a chosen vertex gives the canonical comparison homomorphism on fundamental groups. The present file proves its construction and its behavior on edge generators; an isomorphism theorem requires the separate topological normal-form argument for paths in a finite one-dimensional cell complex.

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

The homomorphism from combinatorial loops to loops in the topological realization.

Equations

• FiniteGraphFreeGroup.graphCombinatorialToTopological root = CategoryTheory.Functor.mapEnd ((Quiver.FreeGroupoid.of V).obj root) FiniteGraphFreeGroup.graphFreeGroupoidToTopological

The geometric basepoint change is available independently of the still open comparison-isomorphism theorem.

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

Changes the basepoint of the topological fundamental group along a chosen graph path.

Equations

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

theorem FiniteGraphFreeGroup.graphVertex_injective {V : Type u} [Quiver V] {v w : V} (h : graphVertex v = graphVertex w) : v = w

theorem FiniteGraphFreeGroup.graphVertex_injective_iff {V : Type u} [Quiver V] {v w : V} : graphVertex v = graphVertex w ↔ v = w