Plane graphs

There is no PlaneGraph type. A plane graph is an abstract G : Graph Plane β together with a drawing drawing : β → ℝ → Plane, related by IsDrawing G drawing. The abstract graph stays itself, so every combinatorial theorem of Schoenflies/Graph/ applies with nothing to project through, and "a plane graph realises an abstract finite graph" is true by construction rather than by a theorem. Bundling would put a record projection inside every combinatorial citation.

The vertices being plane points is what makes the definition short: that the vertices are distinct is not a clause, it is what V(G) : Set Plane already means.

IsDrawing has three clauses. Each edge is drawn by an injective continuous parametrization on [0, 1] whose endpoint values are the two ends of that edge; an edge's arc meets the vertex set only at those two ends; and two distinct edges meet only at vertices incident with both. The second and third are the blueprint's "distinct edges of a plane graph meet only at shared vertices", split so that unique_edge_at — away from the vertices a point of the drawing lies on exactly one edge — falls out directly. That corollary is the form the polygonal overlay wants.

The first clause names the parametrization, not merely its image. The weaker reading — "the point set of an edge is an arc between its ends" — suffices for everything about faces, and fails for the polygonal redrawing, which must speak of the last parameter at which an edge is inside a given square. edge_isArcBetween recovers the weaker reading, so consumers needing only that are unaffected.

Blueprint

• IsDrawing — a plane graph, as an abstract graph plus a drawing.
• IsDrawing.edge_param, IsDrawing.edge_isArcBetween — the parametrization, and its image.
• IsDrawing.arcs_meet_at_vertex, IsDrawing.unique_edge_at — distinct edges meet only at shared vertices; away from the vertices, a point lies on exactly one edge.
• pointSet, IsDrawing.isCompact_pointSet, exterior, isOpen_exterior — what a plane graph occupies, and the open set its faces live in.
• face — the component of the exterior through a point off the drawing. Named by a point rather than indexed, so no face has to be produced before it is spoken about.

def Graph.edgeArc {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (e : β) : Set Schoenflies.Plane

The point set of a single edge: the image of its parametrization on [0, 1].

Equations

• Graph.edgeArc drawing e = drawing e '' unitInterval

structure Graph.IsDrawing {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) : Prop

A drawing of an abstract graph in the plane.

The vertices are already plane points, so a drawing only has to say how the edges run.

• edge_param ⦃e : β⦄ : e ∈ G.edgeSet → ContinuousOn (drawing e) unitInterval ∧ Set.InjOn (drawing e) unitInterval ∧ G.IsLink e (drawing e 0) (drawing e 1)

  Each edge is drawn by an injective continuous parametrization on [0, 1] whose two endpoints are the ends of that edge.

  This says more than "the point set edgeArc drawing e is an arc between the ends". That weaker clause makes two drawings with the same point sets indistinguishable, which is fine for the face theory and useless for the redrawing argument: "the last parameter at which this edge is inside the square at v" is meaningless unless drawing e is itself the parametrization. edge_isArcBetween below recovers the weaker statement.

  Stated orientation-free — G.IsLink e (drawing e 0) (drawing e 1) — because IsLink is symmetric, so pinning drawing e 0 to a named end of a given link would force the two ends to coincide.

• vertex_mem_edgeArc ⦃e : β⦄ ⦃x y v : Schoenflies.Plane⦄ : G.IsLink e x y → v ∈ G.vertexSet → v ∈ edgeArc drawing e → v = x ∨ v = y

  An edge's arc meets the vertex set only at its own two ends.

• edge_inter ⦃e f : β⦄ : e ∈ G.edgeSet → f ∈ G.edgeSet → e ≠ f → ∀ ⦃p : Schoenflies.Plane⦄, p ∈ edgeArc drawing e → p ∈ edgeArc drawing f → p ∈ G.vertexSet ∧ G.Inc e p ∧ G.Inc f p

  Two distinct edges meet only at vertices incident with both.

theorem Graph.IsDrawing.edge_isArcBetween {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) ⦃e : β⦄ ⦃x y : Schoenflies.Plane⦄ (hl : G.IsLink e x y) : Schoenflies.IsArcBetween (edgeArc drawing e) x y

The point set of an edge is an arc between its two ends — the weaker reading of edge_param, and the one the face theory uses.

theorem Graph.IsDrawing.isArc_edgeArc {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e : β} (he : e ∈ G.edgeSet) : Schoenflies.IsArc (edgeArc drawing e)

theorem Graph.IsDrawing.isCompact_edgeArc {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e : β} (he : e ∈ G.edgeSet) : IsCompact (edgeArc drawing e)

theorem Graph.IsDrawing.arcs_meet_at_vertex {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e f : β} (he : e ∈ G.edgeSet) (hf : f ∈ G.edgeSet) (hef : e ≠ f) {p : Schoenflies.Plane} (hpe : p ∈ edgeArc drawing e) (hpf : p ∈ edgeArc drawing f) : p ∈ G.vertexSet

The blueprint's "distinct edges of a plane graph meet only at shared vertices".

theorem Graph.IsDrawing.unique_edge_at {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e f : β} (he : e ∈ G.edgeSet) (hf : f ∈ G.edgeSet) {p : Schoenflies.Plane} (hpV : p ∉ G.vertexSet) (hpe : p ∈ edgeArc drawing e) (hpf : p ∈ edgeArc drawing f) : e = f

Away from the vertices, a point of the drawing lies on exactly one edge. This is the form the polygonal overlay wants.

What a plane graph occupies

def Graph.pointSet {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) : Set Schoenflies.Plane

The point set of a plane graph: its vertices together with all of its edge arcs.

Equations

• G.pointSet drawing = G.vertexSet ∪ ⋃ e ∈ G.edgeSet, Graph.edgeArc drawing e

theorem Graph.vertexSet_subset_pointSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} : G.vertexSet ⊆ G.pointSet drawing

theorem Graph.edgeArc_subset_pointSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {e : β} (he : e ∈ G.edgeSet) : edgeArc drawing e ⊆ G.pointSet drawing

theorem Graph.IsDrawing.isCompact_pointSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) : IsCompact (G.pointSet drawing)

A finite plane graph occupies a compact set: finitely many points and finitely many compact arcs.

theorem Graph.IsDrawing.isClosed_pointSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) : IsClosed (G.pointSet drawing)

def Graph.exterior {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) : Set Schoenflies.Plane

The exterior of a plane graph: everything the drawing does not occupy.

Equations

• G.exterior drawing = (G.pointSet drawing)ᶜ

theorem Graph.IsDrawing.isOpen_exterior {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) : IsOpen (G.exterior drawing)

def Graph.face {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (base : Schoenflies.Plane) : Set Schoenflies.Plane

A face of a plane graph, named by a point of the exterior rather than indexed: no face has to be produced before it can be spoken about.

Equations

• G.face drawing base = connectedComponentIn (G.exterior drawing) base

theorem Graph.face_subset_exterior {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (base : Schoenflies.Plane) : G.face drawing base ⊆ G.exterior drawing

theorem Graph.mem_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {base : Schoenflies.Plane} (h : base ∈ G.exterior drawing) : base ∈ G.face drawing base

theorem Graph.IsDrawing.isOpen_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (base : Schoenflies.Plane) : IsOpen (G.face drawing base)

theorem Graph.isConnected_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {base : Schoenflies.Plane} (h : base ∈ G.exterior drawing) : IsConnected (G.face drawing base)

theorem Graph.face_eq_or_disjoint {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (b c : Schoenflies.Plane) : G.face drawing b = G.face drawing c ∨ Disjoint (G.face drawing b) (G.face drawing c)

Faces partition the exterior: two faces either coincide or are disjoint.