One-Card Extension Search Space

This module starts the finite-search API behind the optimization view of graph reconstruction. Fix a card C. Every candidate reconstruction extending C is obtained by adding one new vertex and choosing the set of old vertices adjacent to it.

The new vertex is represented by none; old vertices are represented by some v.

Main definitions

• SimpleGraph.addVertexWithNeighbors — add one new vertex adjacent exactly to a prescribed set of old vertices.
• SimpleGraph.deleteVert_addVertexWithNeighbors_none_iso — deleting the new vertex recovers the original card.
• SimpleGraph.addVertex_deleteVert_iso — every graph is obtained from any one of its cards by adding the deleted vertex back with its attachment set.
• SimpleGraph.addVertex_card_iso — the same representation transported across an arbitrary card isomorphism.

def SimpleGraph.addVertexWithNeighbors {V : Type u_1} (C : SimpleGraph V) (S : Set V) : SimpleGraph (Option V)

Add one new vertex, represented by none, to C, adjacent exactly to the old vertices in S.

Equations

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

@[simp]

theorem SimpleGraph.addVertexWithNeighbors_adj_some_some {V : Type u_1} (C : SimpleGraph V) (S : Set V) (a b : V) : (C.addVertexWithNeighbors S).Adj (some a) (some b) ↔ C.Adj a b

@[simp]

theorem SimpleGraph.addVertexWithNeighbors_adj_none_some {V : Type u_1} (C : SimpleGraph V) (S : Set V) (a : V) : (C.addVertexWithNeighbors S).Adj none (some a) ↔ a ∈ S

@[simp]

theorem SimpleGraph.addVertexWithNeighbors_adj_some_none {V : Type u_1} (C : SimpleGraph V) (S : Set V) (a : V) : (C.addVertexWithNeighbors S).Adj (some a) none ↔ a ∈ S

@[simp]

theorem SimpleGraph.addVertexWithNeighbors_not_adj_none_none {V : Type u_1} (C : SimpleGraph V) (S : Set V) : ¬(C.addVertexWithNeighbors S).Adj none none

def SimpleGraph.deleteNewVertexEquiv {V : Type u_1} : { w : Option V // w ≠ none } ≃ V

Vertices remaining after deleting the new none vertex are equivalent to the old vertices.

Equations

• SimpleGraph.deleteNewVertexEquiv = { toFun := fun (w : { w : Option V // w ≠ none }) => (↑w).get ⋯, invFun := fun (v : V) => ⟨some v, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def SimpleGraph.deleteVert_addVertexWithNeighbors_none_iso {V : Type u_1} (C : SimpleGraph V) (S : Set V) : (C.addVertexWithNeighbors S).deleteVert none ≃g C

Deleting the newly added vertex recovers the original card.

Equations

• C.deleteVert_addVertexWithNeighbors_none_iso S = { toEquiv := SimpleGraph.deleteNewVertexEquiv, map_rel_iff' := ⋯ }

def SimpleGraph.deleteVertAttachment {V : Type u_1} (G : SimpleGraph V) (v : V) : Set { w : V // w ≠ v }

The neighbors of the deleted vertex, as a subset of the deleted card.

Equations

• G.deleteVertAttachment v = {w : { w : V // w ≠ v } | G.Adj v ↑w}

def SimpleGraph.addVertex_deleteVert_iso {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (v : V) : (G.deleteVert v).addVertexWithNeighbors (G.deleteVertAttachment v) ≃g G

Any graph is obtained from one of its vertex-deleted cards by adding the deleted vertex back with the appropriate attachment set.

Equations

• G.addVertex_deleteVert_iso v = { toEquiv := Equiv.optionSubtypeNe v, map_rel_iff' := ⋯ }

def SimpleGraph.cardAttachment {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {C : SimpleGraph W} {v : V} (e : G.deleteVert v ≃g C) : Set W

Transport the deleted-vertex attachment set across a card isomorphism.

Equations

• SimpleGraph.cardAttachment e = {w : W | G.Adj v ↑(e.symm.toEquiv w)}

def SimpleGraph.addVertex_card_iso {V : Type u_1} {W : Type u_2} [DecidableEq V] {G : SimpleGraph V} {C : SimpleGraph W} {v : V} (e : G.deleteVert v ≃g C) : C.addVertexWithNeighbors (cardAttachment e) ≃g G

If C is isomorphic to a card G - v, then G is represented by adding one vertex to C with the transported attachment set.

Equations

• SimpleGraph.addVertex_card_iso e = { toEquiv := e.symm.optionCongr.trans (Equiv.optionSubtypeNe v), map_rel_iff' := ⋯ }

theorem SimpleGraph.SameDeck.exists_addVertexWithNeighbors_iso {V : Type u_1} [DecidableEq V] {G H : SimpleGraph V} (h : G.SameDeck H) (v : V) : ∃ (S : Set { w : V // w ≠ v }), Nonempty ((G.deleteVert v).addVertexWithNeighbors S ≃g H)

A same-deck graph lies in the one-card extension search space of each matched card.