Graph Orientation

This module introduces conversion operations between Digraphs and SimpleGraphs, by forgetting the edge orientations of Digraph.

Main Definitions

• Digraph.toSimpleGraphInclusive: Converts a Digraph to a SimpleGraph by creating an undirected edge if either orientation exists in the digraph.
• Digraph.toSimpleGraphStrict: Converts a Digraph to a SimpleGraph by creating an undirected edge only if both orientations exist in the digraph.

TODO

• Show that there is an isomorphism between loopless complete digraphs and oriented graphs.
• Define more ways to orient a SimpleGraph.
• Provide lemmas on how toSimpleGraphInclusive and toSimpleGraphStrict relate to other lattice structures on SimpleGraphs and Digraphs.

Tags

digraph, simple graph, oriented graphs

Orientation-forgetting maps on digraphs

def Digraph.toSimpleGraphInclusive {V : Type u_1} (G : Digraph V) : SimpleGraph V

Orientation-forgetting map from Digraph to SimpleGraph that gives an unoriented edge if either orientation is present.

Equations

• G.toSimpleGraphInclusive = SimpleGraph.fromRel G.Adj

def Digraph.toSimpleGraphStrict {V : Type u_1} (G : Digraph V) : SimpleGraph V

Orientation-forgetting map from Digraph to SimpleGraph that gives an unoriented edge if both orientations are present.

Equations

• G.toSimpleGraphStrict = { Adj := fun (v w : V) => v ≠ w ∧ G.Adj v w ∧ G.Adj w v, symm := ⋯, loopless := ⋯ }

theorem Digraph.toSimpleGraphStrict_subgraph_toSimpleGraphInclusive {V : Type u_1} (G : Digraph V) : G.toSimpleGraphStrict ≤ G.toSimpleGraphInclusive

theorem Digraph.toSimpleGraphInclusive_mono {V : Type u_1} : Monotone Digraph.toSimpleGraphInclusive

theorem Digraph.toSimpleGraphStrict_mono {V : Type u_1} : Monotone Digraph.toSimpleGraphStrict

@[simp]

theorem Digraph.toSimpleGraphInclusive_top {V : Type u_1} : ⊤.toSimpleGraphInclusive = ⊤

@[simp]

theorem Digraph.toSimpleGraphStrict_top {V : Type u_1} : ⊤.toSimpleGraphStrict = ⊤

@[simp]

theorem Digraph.toSimpleGraphInclusive_bot {V : Type u_1} : ⊥.toSimpleGraphInclusive = ⊥

@[simp]

theorem Digraph.toSimpleGraphStrict_bot {V : Type u_1} : ⊥.toSimpleGraphStrict = ⊥