Local charts and topological graph covers

This module verifies the local topology needed to realize the combinatorial path-lifting cover.

Local charts for graph realizations

The quotient realization has two kinds of local charts. At a vertex we use the vertex together with the two half-open germs of every incident edge. At an edge-interior point we use the open interval cell. These sets are kept at the prequotient level so that openness is checked by isOpen_coinduced and the endpoint quotient is handled by a small saturation lemma.

noncomputable def FiniteGraphFreeGroup.graphHalf : ↑unitInterval

The midpoint of the unit interval used to separate the two incident-edge stars.

Equations

• FiniteGraphFreeGroup.graphHalf = ⟨1 / 2, FiniteGraphFreeGroup.graphHalf._proof_2⟩

@[simp]

theorem FiniteGraphFreeGroup.graphHalf_coe : ↑graphHalf = 1 / 2

@[simp]

theorem FiniteGraphFreeGroup.graphHalf_pos : 0 < graphHalf

@[simp]

theorem FiniteGraphFreeGroup.graphHalf_lt_one : graphHalf < 1

theorem FiniteGraphFreeGroup.graphHalf_not_lt_zero : ¬graphHalf < 0

@[simp]

theorem FiniteGraphFreeGroup.one_not_lt_graphHalf : ¬1 < graphHalf

def FiniteGraphFreeGroup.graphVertexStarPre {V : Type u} [Quiver V] (v : V) : Set (graphRealizationPre V)

Representatives of the open star of a vertex before taking the realization quotient.

Equations

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

theorem FiniteGraphFreeGroup.graphVertexStarPre_isOpen {V : Type u} [Quiver V] (v : V) : IsOpen (graphVertexStarPre v)

theorem FiniteGraphFreeGroup.graphVertexStarPre_saturated {V : Type u} [Quiver V] (v : V) {x y : graphRealizationPre V} (h : Relation.EqvGen graphRealizationGenerator x y) : x ∈ graphVertexStarPre v ↔ y ∈ graphVertexStarPre v

theorem FiniteGraphFreeGroup.graphVertexStarPre_disjoint {V : Type u} [Quiver V] {v w : V} (hvw : v ≠ w) : Disjoint (graphVertexStarPre v) (graphVertexStarPre w)

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

The open star of a vertex in the graph realization.

Equations

• FiniteGraphFreeGroup.graphVertexStar v = FiniteGraphFreeGroup.graphRealizationQuotient '' FiniteGraphFreeGroup.graphVertexStarPre v

theorem FiniteGraphFreeGroup.graphVertexStar_isOpen {V : Type u} [Quiver V] (v : V) : IsOpen (graphVertexStar v)

theorem FiniteGraphFreeGroup.graphVertexStar_preimage {V : Type u} [Quiver V] (v : V) : graphRealizationQuotient ⁻¹' graphVertexStar v = graphVertexStarPre v

theorem FiniteGraphFreeGroup.graphVertex_mem_graphVertexStar {V : Type u} [Quiver V] (v : V) : graphVertex v ∈ graphVertexStar v

def FiniteGraphFreeGroup.graphEdgeInteriorPre {V : Type u} [Quiver V] (e : Quiver.Total V) : Set (graphRealizationPre V)

Representatives of an edge interior before taking the realization quotient.

Equations

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

theorem FiniteGraphFreeGroup.graphEdgeInteriorPre_isOpen {V : Type u} [Quiver V] (e : Quiver.Total V) : IsOpen (graphEdgeInteriorPre e)

theorem FiniteGraphFreeGroup.graphEdgeInteriorPre_saturated {V : Type u} [Quiver V] (e : Quiver.Total V) {x y : graphRealizationPre V} (h : Relation.EqvGen graphRealizationGenerator x y) : x ∈ graphEdgeInteriorPre e ↔ y ∈ graphEdgeInteriorPre e

def FiniteGraphFreeGroup.graphEdgeInterior {V : Type u} [Quiver V] (e : Quiver.Total V) : Set (graphRealization V)

The open interior of an edge in the graph realization.

Equations

• FiniteGraphFreeGroup.graphEdgeInterior e = FiniteGraphFreeGroup.graphRealizationQuotient '' FiniteGraphFreeGroup.graphEdgeInteriorPre e

theorem FiniteGraphFreeGroup.graphEdgeInterior_isOpen {V : Type u} [Quiver V] (e : Quiver.Total V) : IsOpen (graphEdgeInterior e)

theorem FiniteGraphFreeGroup.graphEdgeInterior_preimage {V : Type u} [Quiver V] (e : Quiver.Total V) : graphRealizationQuotient ⁻¹' graphEdgeInterior e = graphEdgeInteriorPre e

theorem FiniteGraphFreeGroup.graphEdgePath_mem_graphEdgeInterior {V : Type u} [Quiver V] (e : Quiver.Total V) {t : ↑unitInterval} (ht0 : 0 < t) (ht1 : t < 1) : (graphEdgePath e) t ∈ graphEdgeInterior e

noncomputable def FiniteGraphFreeGroup.graphRealizationInteriorLabel {V : Type u} [Quiver V] : graphRealizationPre V → Option (Quiver.Total V × ↑unitInterval)

Records an interior edge representative and parameter, ignoring quotient endpoints.

Equations

• FiniteGraphFreeGroup.graphRealizationInteriorLabel (Sum.inl w) = none
• FiniteGraphFreeGroup.graphRealizationInteriorLabel (Sum.inr z) = if z.snd = 0 ∨ z.snd = 1 then none else some (FiniteGraphFreeGroup.graphEdgeUnderlying z.fst, z.snd)

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

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

theorem FiniteGraphFreeGroup.graphRealization_interior_eqvGen_eq {V : Type u} [Quiver V] {e e' : Quiver.Total V} {t t' : ↑unitInterval} (ht0 : 0 < t) (ht1 : t < 1) (ht0' : 0 < t') (ht1' : t' < 1) (h : Relation.EqvGen graphRealizationGenerator (Sum.inr ⟨graphDiscreteEdge e, t⟩) (Sum.inr ⟨graphDiscreteEdge e', t'⟩)) : e = e' ∧ t = t'

theorem FiniteGraphFreeGroup.graphRealization_vertex_edge_endpoint {V : Type u} [Quiver V] {v : V} {e : Quiver.Total V} {t : ↑unitInterval} (h : graphRealizationQuotient (Sum.inl (graphDiscreteVertex v)) = graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge e, t⟩)) : t = 0 ∨ t = 1

theorem FiniteGraphFreeGroup.graphRealization_vertex_edge_source {V : Type u} [Quiver V] {v : V} {e : Quiver.Total V} {t : ↑unitInterval} (h : graphRealizationQuotient (Sum.inl (graphDiscreteVertex v)) = graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge e, t⟩)) (ht : t = 0) : v = e.left

theorem FiniteGraphFreeGroup.graphRealization_vertex_edge_target {V : Type u} [Quiver V] {v : V} {e : Quiver.Total V} {t : ↑unitInterval} (h : graphRealizationQuotient (Sum.inl (graphDiscreteVertex v)) = graphRealizationQuotient (Sum.inr ⟨graphDiscreteEdge e, t⟩)) (ht : t = 1) : v = e.right

The combinatorial cover viewed through the same geometric-realization construction.

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphCoverRealization {V : Type u} [Quiver V] (root : V) : Type u

The realization of the canonical combinatorial cover based at root.

Equations

• FiniteGraphFreeGroup.graphCoverRealization root = FiniteGraphFreeGroup.graphRealization (FiniteGraphFreeGroup.graphCoverVertex root)

def FiniteGraphFreeGroup.graphCoverRealizationProjection {V : Type u} [Quiver V] (root : V) : graphCoverRealization root → graphRealization V

The realization map induced by the canonical graph-cover projection.

Equations

• FiniteGraphFreeGroup.graphCoverRealizationProjection root = FiniteGraphFreeGroup.graphRealizationMap (FiniteGraphFreeGroup.graphCoverProjection root)

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

@[simp]

theorem FiniteGraphFreeGroup.graphRealizationMap_quotient {V W : Type u} [Quiver V] [Quiver W] (F : V ⥤q W) (x : graphRealizationPre V) : graphRealizationMap F (graphRealizationQuotient x) = graphRealizationQuotient (graphRealizationPreMap F x)

def FiniteGraphFreeGroup.graphCoverRootVertex {V : Type u} [Quiver V] (root : V) : graphCoverVertex root

The cover vertex represented by the identity path at the root.

Equations

• FiniteGraphFreeGroup.graphCoverRootVertex root = ⟨root, CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of V).obj root)⟩

@[simp]

theorem FiniteGraphFreeGroup.graphCoverRootVertex_projection {V : Type u} [Quiver V] (root : V) : (graphCoverRootVertex root).fst = root

def FiniteGraphFreeGroup.graphCoverVertexOver {V : Type u} [Quiver V] (root v : V) : Type u

The discrete fiber of cover vertices over a base vertex.

Equations

• FiniteGraphFreeGroup.graphCoverVertexOver root v = { x : FiniteGraphFreeGroup.graphCoverVertex root // x.fst = v }

@[instance_reducible]

instance FiniteGraphFreeGroup.graphCoverVertexOverTopology {V : Type u} [Quiver V] (root v : V) : TopologicalSpace (graphCoverVertexOver root v)

Equations

• FiniteGraphFreeGroup.graphCoverVertexOverTopology root v = ⊥

instance FiniteGraphFreeGroup.graphCoverVertexOver_discrete {V : Type u} [Quiver V] (root v : V) : DiscreteTopology (graphCoverVertexOver root v)

def FiniteGraphFreeGroup.graphCoverSymmetricFreeGroupoidMap {V : Type u} [Quiver V] (root : V) : Quiver.Symmetrify (graphCoverVertex root) ⥤q Quiver.FreeGroupoid V

The symmetric-edge prefunctor from the canonical cover into the base free groupoid.

Equations

• FiniteGraphFreeGroup.graphCoverSymmetricFreeGroupoidMap root = Quiver.Symmetrify.lift (FiniteGraphFreeGroup.graphCoverProjection root ⋙q Quiver.FreeGroupoid.of V)

theorem FiniteGraphFreeGroup.graphCoverSymmetricFreeGroupoidMap_map_pos {V : Type u} [Quiver V] (root : V) {x y : graphCoverVertex root} (e : x ⟶ y) : (graphCoverSymmetricFreeGroupoidMap root).map (Sum.inl e) = (Quiver.FreeGroupoid.of V).map ↑e

theorem FiniteGraphFreeGroup.graphCoverVertexOver_nonempty {V : Type u} [Quiver V] [WeaklyConnected V] (root v : V) : Nonempty (graphCoverVertexOver root v)

theorem FiniteGraphFreeGroup.graphCoverPreMap_vertexStar_preimage {V : Type u} [Quiver V] {root v : V} : graphRealizationPreMap (graphCoverProjection root) ⁻¹' graphVertexStarPre v = ⋃ (x : graphCoverVertexOver root v), graphVertexStarPre ↑x

theorem FiniteGraphFreeGroup.graphCoverVertexStarPre_union_saturated {V : Type u} [Quiver V] {root v : V} {x y : graphRealizationPre (graphCoverVertex root)} (h : Relation.EqvGen graphRealizationGenerator x y) : x ∈ ⋃ (z : graphCoverVertexOver root v), graphVertexStarPre ↑z ↔ y ∈ ⋃ (z : graphCoverVertexOver root v), graphVertexStarPre ↑z

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_vertexStar_preimage {V : Type u} [Quiver V] {root v : V} : graphCoverRealizationProjection root ⁻¹' graphVertexStar v = ⋃ (x : graphCoverVertexOver root v), graphVertexStar ↑x

@[simp]

theorem FiniteGraphFreeGroup.graphCoverPreMap_vertex {V : Type u} [Quiver V] (root : V) (x : graphCoverVertex root) : graphRealizationPreMap (graphCoverProjection root) (Sum.inl (graphDiscreteVertex x)) = Sum.inl (graphDiscreteVertex x.fst)

@[simp]

theorem FiniteGraphFreeGroup.graphCoverPreMap_edge {V : Type u} [Quiver V] (root : V) (e : Quiver.Total (graphCoverVertex root)) (t : ↑unitInterval) : graphRealizationPreMap (graphCoverProjection root) (Sum.inr ⟨graphDiscreteEdge e, t⟩) = Sum.inr ⟨graphDiscreteEdge { left := e.left.fst, right := e.right.fst, hom := ↑e.hom }, t⟩

theorem FiniteGraphFreeGroup.graphVertexStar_disjoint {V : Type u} [Quiver V] {v w : V} (hvw : v ≠ w) : Disjoint (graphVertexStar v) (graphVertexStar w)

theorem FiniteGraphFreeGroup.graphStar_total_injective {V : Type u} [Quiver V] {x : V} : Function.Injective fun (s : Quiver.Star x) => { left := x, right := s.fst, hom := s.snd }

theorem FiniteGraphFreeGroup.graphCostar_total_injective {V : Type u} [Quiver V] {x : V} : Function.Injective fun (s : Quiver.Costar x) => { left := s.fst, right := x, hom := s.snd }

theorem FiniteGraphFreeGroup.graphCoverStarEquiv_map_eq_of_total_eq {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (e f : Quiver.Total (graphCoverVertex root)) (he : e.left = x) (hf : f.left = x) (htot : { left := e.left.fst, right := e.right.fst, hom := ↑e.hom } = { left := f.left.fst, right := f.right.fst, hom := ↑f.hom }) : (graphCoverStarEquiv root x) ⟨e.right, he ▸ e.hom⟩ = (graphCoverStarEquiv root x) ⟨f.right, hf ▸ f.hom⟩

theorem FiniteGraphFreeGroup.graphCoverCostarEquiv_map_eq_of_total_eq {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (e f : Quiver.Total (graphCoverVertex root)) (he : e.right = x) (hf : f.right = x) (htot : { left := e.left.fst, right := e.right.fst, hom := ↑e.hom } = { left := f.left.fst, right := f.right.fst, hom := ↑f.hom }) : (graphCoverCostarEquiv root x) ⟨e.left, he ▸ e.hom⟩ = (graphCoverCostarEquiv root x) ⟨f.left, hf ▸ f.hom⟩

theorem FiniteGraphFreeGroup.graphCover_total_eq_of_star_eq {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (e f : Quiver.Total (graphCoverVertex root)) (he : e.left = x) (hf : f.left = x) (hstar : ⟨e.right, he ▸ e.hom⟩ = ⟨f.right, hf ▸ f.hom⟩) : e = f

theorem FiniteGraphFreeGroup.graphCover_total_eq_of_costar_eq {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (e f : Quiver.Total (graphCoverVertex root)) (he : e.right = x) (hf : f.right = x) (hcostar : ⟨e.left, he ▸ e.hom⟩ = ⟨f.left, hf ▸ f.hom⟩) : e = f

theorem FiniteGraphFreeGroup.graphCover_source_lift {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (e : Quiver.Total V) (h : x.fst = e.left) : ∃ (d : Quiver.Total (graphCoverVertex root)), d.left = x ∧ { left := d.left.fst, right := d.right.fst, hom := ↑d.hom } = e

theorem FiniteGraphFreeGroup.graphCover_target_lift {V : Type u} [Quiver V] {root : V} (x : graphCoverVertex root) (e : Quiver.Total V) (h : e.right = x.fst) : ∃ (d : Quiver.Total (graphCoverVertex root)), d.right = x ∧ { left := d.left.fst, right := d.right.fst, hom := ↑d.hom } = e

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_vertexStar_injective {V : Type u} [Quiver V] {root v : V} (x : graphCoverVertexOver root v) : Set.InjOn (graphCoverRealizationProjection root) (graphVertexStar ↑x)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_vertexStar_surjective {V : Type u} [Quiver V] {root v : V} (x : graphCoverVertexOver root v) : Set.SurjOn (graphCoverRealizationProjection root) (graphVertexStar ↑x) (graphVertexStar v)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_vertexStar_open_iff {V : Type u} [Quiver V] {root v : V} (x : graphCoverVertexOver root v) {W : Set (graphRealization V)} (hW : W ⊆ graphVertexStar v) : IsOpen W ↔ IsOpen (graphCoverRealizationProjection root ⁻¹' W ∩ graphVertexStar ↑x)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_vertexStar_open {V : Type u} [Quiver V] {root v : V} (x : graphCoverVertexOver root v) {W : Set (graphRealization V)} (hW : W ⊆ graphVertexStar v) (hopen : IsOpen W) : IsOpen (graphCoverRealizationProjection root ⁻¹' W ∩ graphVertexStar ↑x)

The forward open-set implication used by the vertex-star trivialization.

def FiniteGraphFreeGroup.graphCoverEdgeProjection {V : Type u} [Quiver V] (root : V) (d : Quiver.Total (graphCoverVertex root)) : Quiver.Total V

Projects a total edge of the canonical cover to its underlying base edge.

Equations

• FiniteGraphFreeGroup.graphCoverEdgeProjection root d = { left := d.left.fst, right := d.right.fst, hom := ↑d.hom }

def FiniteGraphFreeGroup.graphCoverEdgeOver {V : Type u} [Quiver V] (root : V) (e : Quiver.Total V) : Type u

The discrete fiber of cover edges over a base edge.

Equations

• FiniteGraphFreeGroup.graphCoverEdgeOver root e = { d : Quiver.Total (FiniteGraphFreeGroup.graphCoverVertex root) // FiniteGraphFreeGroup.graphCoverEdgeProjection root d = e }

@[instance_reducible]

instance FiniteGraphFreeGroup.graphCoverEdgeOverTopology {V : Type u} [Quiver V] (root : V) (e : Quiver.Total V) : TopologicalSpace (graphCoverEdgeOver root e)

Equations

• FiniteGraphFreeGroup.graphCoverEdgeOverTopology root e = ⊥

instance FiniteGraphFreeGroup.graphCoverEdgeOver_discrete {V : Type u} [Quiver V] (root : V) (e : Quiver.Total V) : DiscreteTopology (graphCoverEdgeOver root e)

theorem FiniteGraphFreeGroup.graphEdgeInterior_disjoint {V : Type u} [Quiver V] {e f : Quiver.Total V} (hef : e ≠ f) : Disjoint (graphEdgeInterior e) (graphEdgeInterior f)

theorem FiniteGraphFreeGroup.graphCoverEdgeOver_nonempty {V : Type u} [Quiver V] [WeaklyConnected V] {root : V} (e : Quiver.Total V) : Nonempty (graphCoverEdgeOver root e)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_edgeInterior_injective {V : Type u} [Quiver V] {root : V} (d : Quiver.Total (graphCoverVertex root)) : Set.InjOn (graphCoverRealizationProjection root) (graphEdgeInterior d)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_edgeInterior_surjective {V : Type u} [Quiver V] {root : V} {e : Quiver.Total V} (d : graphCoverEdgeOver root e) : Set.SurjOn (graphCoverRealizationProjection root) (graphEdgeInterior ↑d) (graphEdgeInterior e)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_edgeInterior_open_iff {V : Type u} [Quiver V] {root : V} {e : Quiver.Total V} (d : graphCoverEdgeOver root e) {W : Set (graphRealization V)} (hW : W ⊆ graphEdgeInterior e) : IsOpen W ↔ IsOpen (graphCoverRealizationProjection root ⁻¹' W ∩ graphEdgeInterior ↑d)

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_edgeInterior_preimage {V : Type u} [Quiver V] {root : V} (e : Quiver.Total V) : graphCoverRealizationProjection root ⁻¹' graphEdgeInterior e = ⋃ (d : graphCoverEdgeOver root e), graphEdgeInterior ↑d

The local charts above assemble into an honest covering map. Vertices use the lifted stars, while the open interval cells use their lifted interiors.

theorem FiniteGraphFreeGroup.graphCoverRealizationProjection_isCovering {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : IsCoveringMap (graphCoverRealizationProjection root)