Graphs with edge reversal

A Serre graph has directed edges paired by a fixed-point-free reversal. In particular, a loop still has two distinct directions, and parallel edges remain distinct. The quiver associated to a Serre graph keeps those directed edge identities, so its paths can be used for reduced paths, graph groups, and labelled-graph arguments.

The geometric edges of a Serre graph are the reversal pairs {e, rev e}; data attached to an unoriented edge, such as the edge groups of a graph of groups, is indexed by them.

For a reversal-closed set S of darts, the subgraph Γ.restrict S hS keeps every vertex of Γ and the darts in S.

The simple-graph construction takes its edge set from Mathlib's darts. It provides the familiar loopless example while retaining the reversal structure used for general graphs.

References

• J.-P. Serre, Trees, Chapter I, §2.1.

structure TauCeti.SerreGraph : Type (max (u + 1) (v + 1))

A graph in Serre's sense: every directed edge has a distinct reverse edge. Loops and parallel edges are permitted.

• V : Type u

  Vertices.

• E : Type v

  Directed edges, or darts.

• src : self.E → self.V

  Initial vertex of a dart.

• rev : self.E → self.E

  Reverse dart.

• rev_rev (e : self.E) : self.rev (self.rev e) = e

  Reversing twice does nothing.

• rev_ne (e : self.E) : self.rev e ≠ e

  A dart differs from its reverse, even when it is a loop.

def TauCeti.SerreGraph.tgt (Γ : SerreGraph) (e : Γ.E) : Γ.V

Terminal vertex of a dart. The body is exposed so that families indexed by vertices, such as the vertex groups of a graph of groups, can be evaluated at Γ.tgt e without a cast.

theorem TauCeti.SerreGraph.tgt_def (Γ : SerreGraph) (e : Γ.E) : Γ.tgt e = Γ.src (Γ.rev e)

A dart ends where its reverse starts.

@[simp]

theorem TauCeti.SerreGraph.src_rev (Γ : SerreGraph) (e : Γ.E) : Γ.src (Γ.rev e) = Γ.tgt e

@[simp]

theorem TauCeti.SerreGraph.tgt_rev (Γ : SerreGraph) (e : Γ.E) : Γ.tgt (Γ.rev e) = Γ.src e

theorem TauCeti.SerreGraph.rev_injective (Γ : SerreGraph) : Function.Injective Γ.rev

def TauCeti.SerreGraph.GeomEdge (Γ : SerreGraph) : Type v

The geometric edges of a Serre graph: the pairs {e, rev e} of mutually reverse darts.

def TauCeti.SerreGraph.toGeomEdge (Γ : SerreGraph) (e : Γ.E) : Γ.GeomEdge

The geometric edge underlying a dart.

@[simp]

theorem TauCeti.SerreGraph.toGeomEdge_rev (Γ : SerreGraph) (e : Γ.E) : Γ.toGeomEdge (Γ.rev e) = Γ.toGeomEdge e

A dart and its reverse have the same underlying geometric edge.

theorem TauCeti.SerreGraph.toGeomEdge_surjective (Γ : SerreGraph) : Function.Surjective Γ.toGeomEdge

theorem TauCeti.SerreGraph.toGeomEdge_eq_toGeomEdge_iff (Γ : SerreGraph) {e f : Γ.E} : Γ.toGeomEdge e = Γ.toGeomEdge f ↔ f = e ∨ f = Γ.rev e

Two darts have the same geometric edge exactly when they are equal or mutually reverse.

def TauCeti.SerreGraph.GeomEdge.lift (Γ : SerreGraph) {β : Sort u_1} (f : Γ.E → β) (hf : ∀ (e : Γ.E), f (Γ.rev e) = f e) : Γ.GeomEdge → β

A function on darts taking the same value on mutually reverse darts descends to geometric edges.

@[simp]

theorem TauCeti.SerreGraph.GeomEdge.lift_toGeomEdge (Γ : SerreGraph) {β : Sort u_1} (f : Γ.E → β) (hf : ∀ (e : Γ.E), f (Γ.rev e) = f e) (e : Γ.E) : lift Γ f hf (Γ.toGeomEdge e) = f e

def TauCeti.SerreGraph.IsOrientation (Γ : SerreGraph) (O : Set Γ.E) : Prop

An orientation chooses one dart from each reverse pair.

theorem TauCeti.SerreGraph.isOrientation_iff (Γ : SerreGraph) (O : Set Γ.E) : Γ.IsOrientation O ↔ ∀ (e : Γ.E), e ∈ O ↔ Γ.rev e ∉ O

theorem TauCeti.SerreGraph.IsOrientation.mem_rev_iff (Γ : SerreGraph) {O : Set Γ.E} (hO : Γ.IsOrientation O) (e : Γ.E) : Γ.rev e ∈ O ↔ e ∉ O

theorem TauCeti.SerreGraph.IsOrientation.rev_notMem_of_mem (Γ : SerreGraph) {O : Set Γ.E} (hO : Γ.IsOrientation O) (e : Γ.E) (he : e ∈ O) : Γ.rev e ∉ O

@[instance_reducible]

instance TauCeti.SerreGraph.toQuiver (Γ : SerreGraph) : Quiver Γ.V

The quiver whose arrows are the actual darts from their source to their target.

@[instance_reducible]

instance TauCeti.SerreGraph.toQuiverHasInvolutiveReverse (Γ : SerreGraph) : Quiver.HasInvolutiveReverse Γ.V

Reversal on the quiver associated to a Serre graph.

@[simp]

theorem TauCeti.SerreGraph.reverse_val (Γ : SerreGraph) {a b : Γ.V} (f : a ⟶ b) : ↑(Quiver.reverse f) = Γ.rev ↑f

def TauCeti.SerreGraph.dart (Γ : SerreGraph) (e : Γ.E) : Γ.src e ⟶ Γ.tgt e

A dart as an arrow of the associated quiver.

@[simp]

theorem TauCeti.SerreGraph.dart_val (Γ : SerreGraph) (e : Γ.E) : ↑(Γ.dart e) = e

@[reducible, inline]

abbrev TauCeti.SerreGraph.Path (Γ : SerreGraph) (a b : Γ.V) : Type (max u v)

An indexed path in a Serre graph is a path of its associated quiver.

def TauCeti.SerreGraph.Preconnected (Γ : SerreGraph) : Prop

A Serre graph is preconnected when any two vertices are joined by a path.

theorem TauCeti.SerreGraph.preconnected_iff (Γ : SerreGraph) : Γ.Preconnected ↔ ∀ (a b : Γ.V), Nonempty (Γ.Path a b)

Preconnectivity is pairwise Serre path reachability.

theorem TauCeti.SerreGraph.preconnected_of_forall_nonempty_path (Γ : SerreGraph) (a : Γ.V) (h : ∀ (b : Γ.V), Nonempty (Γ.Path a b)) : Γ.Preconnected

A Serre graph is preconnected as soon as one vertex is joined by a path to every vertex: paths can be reversed.

theorem TauCeti.SerreGraph.eq_of_path_of_forall_src_eq_tgt (Γ : SerreGraph) (h : ∀ (e : Γ.E), Γ.src e = Γ.tgt e) {a b : Γ.V} (p : Γ.Path a b) : a = b

In a Serre graph all of whose darts are loops, a path never leaves its starting vertex.

def TauCeti.SerreGraph.Connected (Γ : SerreGraph) : Prop

A Serre graph is connected when it is nonempty and path-connected.

theorem TauCeti.SerreGraph.connected_iff (Γ : SerreGraph) : Γ.Connected ↔ Nonempty Γ.V ∧ Γ.Preconnected

Connectedness requires a vertex as well as preconnectivity.

structure TauCeti.SerreGraph.Hom (Γ : SerreGraph) (Δ : SerreGraph) : Type (max (max (max u v) w) x)

A morphism of Serre graphs maps vertices and darts and preserves incidence and reversal.

• mapV : Γ.V → Δ.V

  Vertex map.

• mapE : Γ.E → Δ.E

  Dart map.

• map_src (e : Γ.E) : Δ.src (self.mapE e) = self.mapV (Γ.src e)

  Sources are preserved.

• map_rev (e : Γ.E) : self.mapE (Γ.rev e) = Δ.rev (self.mapE e)

  Reversal is preserved.

theorem TauCeti.SerreGraph.Hom.ext (Γ : SerreGraph) {Δ : SerreGraph} {f g : Γ.Hom Δ} (hV : f.mapV = g.mapV) (hE : f.mapE = g.mapE) : f = g

theorem TauCeti.SerreGraph.Hom.ext_iff {Γ : SerreGraph} {Δ : SerreGraph} {f g : Γ.Hom Δ} : f = g ↔ f.mapV = g.mapV ∧ f.mapE = g.mapE

@[simp]

theorem TauCeti.SerreGraph.Hom.map_tgt (Γ : SerreGraph) {Δ : SerreGraph} (f : Γ.Hom Δ) (e : Γ.E) : Δ.tgt (f.mapE e) = f.mapV (Γ.tgt e)

def TauCeti.SerreGraph.Hom.toPrefunctor {Γ : SerreGraph} {Δ : SerreGraph} (f : Γ.Hom Δ) : Γ.V ⥤q Δ.V

The quiver prefunctor underlying a Serre-graph morphism.

@[simp]

theorem TauCeti.SerreGraph.Hom.toPrefunctor_obj {Γ : SerreGraph} {Δ : SerreGraph} (f : Γ.Hom Δ) (a : Γ.V) : f.toPrefunctor.obj a = f.mapV a

@[simp]

theorem TauCeti.SerreGraph.Hom.toPrefunctor_map_val {Γ : SerreGraph} {Δ : SerreGraph} (f : Γ.Hom Δ) {a b : Γ.V} (e : a ⟶ b) : ↑(f.toPrefunctor.map e) = f.mapE ↑e

theorem TauCeti.SerreGraph.Hom.preconnected_of_surjective {Γ : SerreGraph} {Δ : SerreGraph} (f : Γ.Hom Δ) (hf : Function.Surjective f.mapV) (hΓ : Γ.Preconnected) : Δ.Preconnected

A vertex-surjective graph morphism carries preconnectedness to its target.

theorem TauCeti.SerreGraph.Hom.connected_of_surjective {Γ : SerreGraph} {Δ : SerreGraph} (f : Γ.Hom Δ) (hf : Function.Surjective f.mapV) (hΓ : Γ.Connected) : Δ.Connected

A vertex-surjective graph morphism carries connectedness to its target.

def TauCeti.SerreGraph.Hom.id (Γ : SerreGraph) : Γ.Hom Γ

Identity morphism of a Serre graph.

@[simp]

theorem TauCeti.SerreGraph.Hom.id_mapV (Γ : SerreGraph) : (id Γ).mapV = _root_.id

@[simp]

theorem TauCeti.SerreGraph.Hom.id_mapE (Γ : SerreGraph) : (id Γ).mapE = _root_.id

def TauCeti.SerreGraph.Hom.comp {Γ : SerreGraph} {Δ : SerreGraph} {Θ : SerreGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) : Γ.Hom Θ

Compose Serre-graph morphisms.

@[simp]

theorem TauCeti.SerreGraph.Hom.comp_mapV (Γ : SerreGraph) {Δ : SerreGraph} {Θ : SerreGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) : (g.comp f).mapV = g.mapV ∘ f.mapV

@[simp]

theorem TauCeti.SerreGraph.Hom.comp_mapE (Γ : SerreGraph) {Δ : SerreGraph} {Θ : SerreGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) : (g.comp f).mapE = g.mapE ∘ f.mapE

@[simp]

theorem TauCeti.SerreGraph.Hom.id_comp (Γ : SerreGraph) {Δ : SerreGraph} (f : Γ.Hom Δ) : (id Δ).comp f = f

@[simp]

theorem TauCeti.SerreGraph.Hom.comp_id (Γ : SerreGraph) {Δ : SerreGraph} (f : Γ.Hom Δ) : f.comp (id Γ) = f

theorem TauCeti.SerreGraph.Hom.comp_assoc (Γ : SerreGraph) {Δ : SerreGraph} {Θ : SerreGraph} {Ξ : SerreGraph} (f : Γ.Hom Δ) (g : Δ.Hom Θ) (h : Θ.Hom Ξ) : h.comp (g.comp f) = (h.comp g).comp f

@[simp]

theorem TauCeti.SerreGraph.Hom.toPrefunctor_id (Γ : SerreGraph) : (id Γ).toPrefunctor = 𝟭q Γ.V

@[simp]

theorem TauCeti.SerreGraph.Hom.toPrefunctor_comp (Γ : SerreGraph) {Δ : SerreGraph} {Θ : SerreGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) : (g.comp f).toPrefunctor = f.toPrefunctor ⋙q g.toPrefunctor

instance TauCeti.SerreGraph.Hom.toPrefunctor_mapReverse (Γ : SerreGraph) {Δ : SerreGraph} (f : Γ.Hom Δ) : f.toPrefunctor.MapReverse

@[reducible, inline]

abbrev TauCeti.SerreGraph.restrict (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) : SerreGraph

The subgraph of Γ with all vertices of Γ and the darts of a reversal-closed set S. The vertex type reduces to that of Γ, so vertices of Γ are vertices of the subgraph.

@[simp]

theorem TauCeti.SerreGraph.restrict_src (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) (e : (Γ.restrict S hS).E) : (Γ.restrict S hS).src e = Γ.src ↑e

@[simp]

theorem TauCeti.SerreGraph.restrict_rev_val (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) (e : (Γ.restrict S hS).E) : ↑((Γ.restrict S hS).rev e) = Γ.rev ↑e

@[simp]

theorem TauCeti.SerreGraph.restrict_tgt (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) (e : (Γ.restrict S hS).E) : (Γ.restrict S hS).tgt e = Γ.tgt ↑e

def TauCeti.SerreGraph.restrictInclusion (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) : (Γ.restrict S hS).Hom Γ

The inclusion of a restriction into the ambient graph.

@[simp]

theorem TauCeti.SerreGraph.restrictInclusion_mapV (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) (a : (Γ.restrict S hS).V) : (Γ.restrictInclusion S hS).mapV a = a

@[simp]

theorem TauCeti.SerreGraph.restrictInclusion_mapE (Γ : SerreGraph) (S : Set Γ.E) (hS : ∀ e ∈ S, Γ.rev e ∈ S) (e : (Γ.restrict S hS).E) : (Γ.restrictInclusion S hS).mapE e = ↑e

def TauCeti.SerreGraph.rose (α : Type w) : SerreGraph

The rose on a type of petals. Each petal is a loop with two distinct darts.

@[simp]

theorem TauCeti.SerreGraph.rose_src (α : Type w) (e : α × Bool) : (rose α).src e = PUnit.unit

@[simp]

theorem TauCeti.SerreGraph.rose_rev (α : Type w) (e : α × Bool) : (rose α).rev e = (e.1, !e.2)

@[simp]

theorem TauCeti.SerreGraph.rose_tgt (α : Type w) (e : α × Bool) : (rose α).tgt e = PUnit.unit

Each dart of a rose is a loop.

@[reducible, inline]

abbrev TauCeti.SerreGraph.point : SerreGraph

The Serre graph with one vertex and no edges.

@[instance_reducible]

instance TauCeti.SerreGraph.instUniqueVRose (α : Type w) : Unique (rose α).V

A rose has a single vertex.

@[instance_reducible]

instance TauCeti.SerreGraph.instDecidableEqERose (α : Type w) [DecidableEq α] : DecidableEq (rose α).E

The darts of a rose, being pairs of a petal and a direction, have decidable equality when the petals do.

def TauCeti.SerreGraph.roseGeomEdgeEquiv (α : Type w) : (rose α).GeomEdge ≃ α

The geometric edges of a rose are its petals.

@[simp]

theorem TauCeti.SerreGraph.roseGeomEdgeEquiv_toGeomEdge (α : Type w) (e : α × Bool) : (roseGeomEdgeEquiv α) ((rose α).toGeomEdge e) = e.1

theorem TauCeti.SerreGraph.rose_connected (α : Type u_1) : (rose α).Connected

Every rose is connected, including the rose without petals.

theorem TauCeti.SerreGraph.rose_isOrientation (α : Type w) : (rose α).IsOrientation {e : (rose α).E | e.2 = true}

Positive darts form an orientation of a rose.

def TauCeti.SerreGraph.segment : SerreGraph

The segment: two vertices joined by a single pair of darts. The dart b runs from the vertex b to the vertex !b.

@[simp]

theorem TauCeti.SerreGraph.segment_src (b : Bool) : segment.src b = b

@[simp]

theorem TauCeti.SerreGraph.segment_rev (b : Bool) : segment.rev b = !b

@[simp]

theorem TauCeti.SerreGraph.segment_tgt (b : Bool) : segment.tgt b = !b

def TauCeti.SerreGraph.segmentVEquiv : segment.V ≃ Bool

The vertices of the segment are the Booleans.

@[instance_reducible]

instance TauCeti.SerreGraph.instDecidableEqESegment : DecidableEq segment.E

The darts of the segment, being Booleans, have decidable equality.

@[instance_reducible]

instance TauCeti.SerreGraph.instUniqueGeomEdgeSegment : Unique segment.GeomEdge

The segment has a single geometric edge.

def SimpleGraph.toSerreGraph {V : Type u} (G : SimpleGraph V) : TauCeti.SerreGraph

The Serre graph of a simple graph has its darts as directed edges.

@[simp]

theorem SimpleGraph.toSerreGraph_src {V : Type u} (G : SimpleGraph V) (e : G.Dart) : G.toSerreGraph.src e = e.toProd.1

@[simp]

theorem SimpleGraph.toSerreGraph_rev {V : Type u} (G : SimpleGraph V) (e : G.Dart) : G.toSerreGraph.rev e = e.symm

@[simp]

theorem SimpleGraph.toSerreGraph_tgt {V : Type u} (G : SimpleGraph V) (e : G.Dart) : G.toSerreGraph.tgt e = e.toProd.2