Contraction of a directed tree realization

This module constructs cellwise contraction data from the unique paths in an arborescence.

Contraction data for a directed tree realization

This file isolates the geometric part of the eventual graph comparison theorem. For an arborescence, every vertex has a unique directed path from the root. The cellwise formula below contracts each edge along that root path. The formula is the usual square filling of a concatenated path:

(t, s) ↦ p ((1 - s) * (1 + t) / 2).

The horizontal boundary is the edge, while the two vertical boundaries are the contractions of its endpoints.

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

The path in the realization associated to a directed quiver path.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphTreeRootPath {V : Type u} [Quiver V] [Quiver.Arborescence V] (b : V) : Path (graphVertex (Quiver.root V)) (graphVertex b)

The unique root path in the realization of an arborescence.

Equations

• FiniteGraphFreeGroup.graphTreeRootPath b = FiniteGraphFreeGroup.graphRealizationDirectedPath default

theorem FiniteGraphFreeGroup.graphTreeRootPath_cons {V : Type u} [Quiver V] [Quiver.Arborescence V] {a b : V} (e : a ⟶ b) : graphTreeRootPath b = (graphTreeRootPath a).trans (graphRealizationForwardPath e)

@[simp]

theorem FiniteGraphFreeGroup.treeContractionCoordinate_zero_right (t : ↑unitInterval) : FiniteGraphFreeGroup.treeContractionCoordinate✝ t 0 = ⟨(1 + ↑t) / 2, ⋯⟩

@[simp]

theorem FiniteGraphFreeGroup.treeContractionCoordinate_zero_left (s : ↑unitInterval) : FiniteGraphFreeGroup.treeContractionCoordinate✝ 0 s = ⟨(1 - ↑s) / 2, ⋯⟩

@[simp]

theorem FiniteGraphFreeGroup.treeContractionCoordinate_one_left (s : ↑unitInterval) : FiniteGraphFreeGroup.treeContractionCoordinate✝ 1 s = ⟨1 - ↑s, ⋯⟩

@[simp]

theorem FiniteGraphFreeGroup.treeContractionCoordinate_one_right (t : ↑unitInterval) : FiniteGraphFreeGroup.treeContractionCoordinate✝ t 1 = 0

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

The square which contracts the cell of an edge towards the root.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphTreeVertexContraction {V : Type u} [Quiver V] [Quiver.Arborescence V] (v : V) : C(↑unitInterval, graphRealization V)

The path which contracts a vertex of the tree to the root.

Equations

• FiniteGraphFreeGroup.graphTreeVertexContraction v = (FiniteGraphFreeGroup.graphTreeRootPath v).symm.toContinuousMap

@[simp]

theorem FiniteGraphFreeGroup.graphTreeVertexContraction_apply {V : Type u} [Quiver V] [Quiver.Arborescence V] (v : V) (s : ↑unitInterval) : (graphTreeVertexContraction v) s = (graphTreeRootPath v) (unitInterval.symm s)

@[simp]

theorem FiniteGraphFreeGroup.graphTreeEdgeContraction_zero_right {V : Type u} [Quiver V] [Quiver.Arborescence V] (e : Quiver.Total V) (t : ↑unitInterval) : (graphTreeEdgeContraction e) (t, 0) = (graphEdgePath e) t

@[simp]

theorem FiniteGraphFreeGroup.graphTreeEdgeContraction_zero_left {V : Type u} [Quiver V] [Quiver.Arborescence V] (e : Quiver.Total V) (s : ↑unitInterval) : (graphTreeEdgeContraction e) (0, s) = (graphTreeVertexContraction e.left) s

@[simp]

theorem FiniteGraphFreeGroup.graphTreeEdgeContraction_one_left {V : Type u} [Quiver V] [Quiver.Arborescence V] (e : Quiver.Total V) (s : ↑unitInterval) : (graphTreeEdgeContraction e) (1, s) = (graphTreeVertexContraction e.right) s

@[simp]

theorem FiniteGraphFreeGroup.graphTreeEdgeContraction_one_right {V : Type u} [Quiver V] [Quiver.Arborescence V] (e : Quiver.Total V) (t : ↑unitInterval) : (graphTreeEdgeContraction e) (t, 1) = graphVertex (Quiver.root V)

The cellwise squares agree on the endpoint generators, so the quotient universal property turns them into a global homotopy.

noncomputable def FiniteGraphFreeGroup.graphTreeVertexFamily {V : Type u} [Quiver V] [Quiver.Arborescence V] : C(WithDiscreteTopology V, C(↑unitInterval, graphRealization V))

The continuously parameterized contraction paths assigned to tree vertices.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphTreeEdgeFamily {V : Type u} [Quiver V] [Quiver.Arborescence V] : C((_ : WithDiscreteTopology (Quiver.Total V)) × ↑unitInterval, C(↑unitInterval, graphRealization V))

The continuously parameterized contraction squares assigned to tree edges.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphTreeVertexFamilyUncurry {V : Type u} [Quiver V] [Quiver.Arborescence V] : C(WithDiscreteTopology V × ↑unitInterval, graphRealization V)

The uncurried vertex part of the tree contraction.

Equations

• FiniteGraphFreeGroup.graphTreeVertexFamilyUncurry = FiniteGraphFreeGroup.graphTreeVertexFamily.uncurry

noncomputable def FiniteGraphFreeGroup.graphTreeEdgeFamilyUncurry {V : Type u} [Quiver V] [Quiver.Arborescence V] : C(((_ : WithDiscreteTopology (Quiver.Total V)) × ↑unitInterval) × ↑unitInterval, graphRealization V)

The uncurried edge part of the tree contraction.

Equations

• FiniteGraphFreeGroup.graphTreeEdgeFamilyUncurry = FiniteGraphFreeGroup.graphTreeEdgeFamily.uncurry

noncomputable def FiniteGraphFreeGroup.graphTreeContractionPieces {V : Type u} [Quiver V] [Quiver.Arborescence V] : C(WithDiscreteTopology V × ↑unitInterval ⊕ ((_ : WithDiscreteTopology (Quiver.Total V)) × ↑unitInterval) × ↑unitInterval, graphRealization V)

The sum of the cellwise vertex and edge contractions before quotienting.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphTreeContractionPre {V : Type u} [Quiver V] [Quiver.Arborescence V] : C(graphRealizationPre V × ↑unitInterval, graphRealization V)

The cellwise contraction before descending to the endpoint quotient.

Equations

• FiniteGraphFreeGroup.graphTreeContractionPre = FiniteGraphFreeGroup.graphTreeContractionPieces.comp { toFun := ⇑Homeomorph.sumProdDistrib, continuous_toFun := ⋯ }

@[simp]

theorem FiniteGraphFreeGroup.graphTreeContractionPre_vertex {V : Type u} [Quiver V] [Quiver.Arborescence V] (v : WithDiscreteTopology V) (s : ↑unitInterval) : graphTreeContractionPre (Sum.inl v, s) = (graphTreeVertexContraction (graphVertexUnderlying v)) s

@[simp]

theorem FiniteGraphFreeGroup.graphTreeContractionPre_edge {V : Type u} [Quiver V] [Quiver.Arborescence V] (e : WithDiscreteTopology (Quiver.Total V)) (t s : ↑unitInterval) : graphTreeContractionPre (Sum.inr ⟨e, t⟩, s) = (graphTreeEdgeContraction (graphEdgeUnderlying e)) (t, s)

theorem FiniteGraphFreeGroup.graphTreeContractionPre_respects {V : Type u} [Quiver V] [Quiver.Arborescence V] {x y : graphRealizationPre V} (h : Relation.EqvGen graphRealizationGenerator x y) (s : ↑unitInterval) : graphTreeContractionPre (x, s) = graphTreeContractionPre (y, s)

noncomputable def FiniteGraphFreeGroup.graphTreeContraction {V : Type u} [Quiver V] [Quiver.Arborescence V] : C(graphRealization V × ↑unitInterval, graphRealization V)

The cellwise contraction descended through the endpoint quotient.

Equations

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

@[simp]

theorem FiniteGraphFreeGroup.graphTreeContraction_quotient {V : Type u} [Quiver V] [Quiver.Arborescence V] (x : graphRealizationPre V) (s : ↑unitInterval) : graphTreeContraction (graphRealizationQuotient x, s) = graphTreeContractionPre (x, s)

@[simp]

theorem FiniteGraphFreeGroup.graphTreeContraction_vertex {V : Type u} [Quiver V] [Quiver.Arborescence V] (v : WithDiscreteTopology V) (s : ↑unitInterval) : graphTreeContraction (graphVertex (graphVertexUnderlying v), s) = (graphTreeVertexContraction (graphVertexUnderlying v)) s

theorem FiniteGraphFreeGroup.graphTreeContraction_edge {V : Type u} [Quiver V] [Quiver.Arborescence V] (e : WithDiscreteTopology (Quiver.Total V)) (t s : ↑unitInterval) : graphTreeContraction (graphRealizationQuotient (Sum.inr ⟨e, t⟩), s) = (graphTreeEdgeContraction (graphEdgeUnderlying e)) (t, s)

theorem FiniteGraphFreeGroup.graphTreeContraction_zero {V : Type u} [Quiver V] [Quiver.Arborescence V] (x : graphRealization V) : graphTreeContraction (x, 0) = x

theorem FiniteGraphFreeGroup.graphTreeContraction_one {V : Type u} [Quiver V] [Quiver.Arborescence V] (x : graphRealization V) : graphTreeContraction (x, 1) = graphVertex (Quiver.root V)

instance FiniteGraphFreeGroup.graphRealization_contractible {V : Type u} [Quiver V] [Quiver.Arborescence V] : ContractibleSpace (graphRealization V)

An arborescence realization is contractible.

theorem FiniteGraphFreeGroup.graphRealization_tree_simplyConnected {V : Type u} [Quiver V] [Quiver.Arborescence V] : SimplyConnectedSpace (graphRealization V)