Pulling a simple graph back along an embedding #

Pulling a simple graph back along an embedding f : V ↪ W forgets everything outside the window f '' V, and pushing the result forward again recovers exactly what the window sees: the intersection of the graph with the complete graph supported on that window. Since pushing forward along an embedding is injective, prescribing a pullback is therefore the same as prescribing that intersection — a condition on an induced subgraph turned into a condition on edges.

The window of a graph on ℕ spanned by the first n labels is the pullback along Fin.val; it is how a graph on an infinite label set is read as a finite sample.

Main definitions #

SimpleGraph.restrictFin — the initial n-label window of a graph on ℕ.

Main results #

SimpleGraph.map_comap_eq_inf_map_top — pushing a pullback forward cuts the graph down to the window;
SimpleGraph.comap_eq_iff_inf_map_top — prescribing a pullback is prescribing that intersection;
SimpleGraph.map_sup — pushing forward along any map commutes with joins;
SimpleGraph.restrictFin_adj — two labels are joined in a window exactly when they are joined in the graph;
SimpleGraph.comap_restrictFin_castLE — a window of a longer window is the shorter window.

source

@[simp]

theorem SimpleGraph.map_comap_eq_inf_map_top {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) :

SimpleGraph.map (⇑f) (SimpleGraph.comap (⇑f) G) = G ⊓ SimpleGraph.map ⇑f ⊤

Pushing a pullback forward again cuts the graph down to the window seen by the embedding.

source

theorem SimpleGraph.comap_eq_iff_inf_map_top {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) (H : SimpleGraph V) :

SimpleGraph.comap (⇑f) G = H ↔ G ⊓ SimpleGraph.map ⇑f ⊤ = SimpleGraph.map (⇑f) H

A pullback along an embedding is prescribed exactly by prescribing the intersection of the graph with the window seen by the embedding.

source

@[simp]

theorem SimpleGraph.map_sup {V : Type u_1} {W : Type u_2} (f : V → W) (G H : SimpleGraph V) :

SimpleGraph.map f (G ⊔ H) = SimpleGraph.map f G ⊔ SimpleGraph.map f H

Pushing a graph forward along any map commutes with joins: an edge of the image of G ⊔ H is the image of an edge of G or of an edge of H.

source

def SimpleGraph.restrictFin (G : SimpleGraph ℕ) (n : ℕ) :

SimpleGraph (Fin n)

The window of a graph on ℕ spanned by the first n labels.

Equations

G.restrictFin n = SimpleGraph.comap (fun (i : Fin n) => ↑i) G

Instances For

source

@[simp]

theorem SimpleGraph.restrictFin_adj {n : ℕ} (G : SimpleGraph ℕ) (a b : Fin n) :

(G.restrictFin n).Adj a b ↔ G.Adj ↑a ↑b

source

theorem SimpleGraph.comap_restrictFin {m n : ℕ} (G : SimpleGraph ℕ) (f : Fin m → Fin n) :

SimpleGraph.comap f (G.restrictFin n) = SimpleGraph.comap (fun (i : Fin m) => ↑(f i)) G

Pulling a window back along a map of finite labels is pulling the graph back along the composite labels.

source

@[simp]

theorem SimpleGraph.comap_restrictFin_castAdd (G : SimpleGraph ℕ) (k l : ℕ) :

SimpleGraph.comap (Fin.castAdd l) (G.restrictFin (k + l)) = G.restrictFin k

The first of two consecutive windows of a window is the window.

source

@[simp]

theorem SimpleGraph.comap_restrictFin_natAdd (G : SimpleGraph ℕ) (k l : ℕ) :

SimpleGraph.comap (Fin.natAdd k) (G.restrictFin (k + l)) = SimpleGraph.comap (fun (i : Fin l) => k + ↑i) G

The second of two consecutive windows of a window is the window at the offset.

source

@[simp]

theorem SimpleGraph.comap_val (G : SimpleGraph ℕ) (n : ℕ) :

SimpleGraph.comap (fun (i : Fin n) => ↑i) G = G.restrictFin n

Pulling back along the coercion of finite labels is taking the window.

source

@[simp]

theorem SimpleGraph.comap_restrictFin_castLE {m n : ℕ} (G : SimpleGraph ℕ) (h : m ≤ n) :

SimpleGraph.comap (Fin.castLE h) (G.restrictFin n) = G.restrictFin m

A window of a longer window is the shorter window: pulling the length-n window back along the inclusion of Fin m in Fin n is the length-m window.

source