Induced subgraphs

This module restricts a chip-firing graph to a nonempty finite set of vertices. Raw edge occurrences are filtered before their endpoints are bundled into the subtype, so parallel edges are retained without identification.

noncomputable def Utilities.inducedEdges (G : CFGraph) (S : Finset G.V) : Multiset (G.V × G.V)

The raw edges of G whose two endpoints belong to S.

Equations

• Utilities.inducedEdges G S = Multiset.filter (fun (edge : G.V × G.V) => edge.1 ∈ S ∧ edge.2 ∈ S) G.edges

def Utilities.restrictInducedEdge (G : CFGraph) (S : Finset G.V) (edge : G.V × G.V) (hEdge : edge.1 ∈ S ∧ edge.2 ∈ S) : ↥S × ↥S

Bundle both endpoints of an edge as vertices of the inducing set.

Equations

• Utilities.restrictInducedEdge G S edge hEdge = (⟨edge.1, ⋯⟩, ⟨edge.2, ⋯⟩)

@[reducible, inline]

noncomputable abbrev Utilities.inducedSubgraph (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : CFGraph

The subgraph of G induced by the nonempty finite vertex set S.

Equations

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

@[simp]

theorem Utilities.inducedSubgraph_vertices (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : (inducedSubgraph G S hS).V = ↥S

@[simp]

theorem Utilities.inducedSubgraph_edges (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : (inducedSubgraph G S hS).edges = Multiset.pmap (restrictInducedEdge G S) (inducedEdges G S) ⋯

def Utilities.inducedSubgraphInclusion (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : (inducedSubgraph G S hS).V → G.V

The inclusion of the induced vertex set into the original graph.

Equations

• Utilities.inducedSubgraphInclusion G S hS x = ↑x

@[simp]

theorem Utilities.inducedSubgraphInclusion_apply (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) (x : (inducedSubgraph G S hS).V) : inducedSubgraphInclusion G S hS x = ↑x

theorem Utilities.inducedSubgraphInclusion_injective (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : Function.Injective (inducedSubgraphInclusion G S hS)

theorem Utilities.inducedSubgraph_edge_card (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : (inducedSubgraph G S hS).edges.card = (inducedEdges G S).card

theorem Utilities.inducedSubgraph_edge_card_eq_filter (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : (inducedSubgraph G S hS).edges.card = (Multiset.filter (fun (edge : G.V × G.V) => edge.1 ∈ S ∧ edge.2 ∈ S) G.edges).card

The edge count of an induced subgraph is the number of ambient edge occurrences whose two endpoints lie in the inducing set. This public form is useful for occurrence-level certificate calculations; in particular, it does not pass through a set of endpoint pairs and therefore retains parallel edges.

@[simp]

theorem Utilities.num_edges_inducedSubgraph (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) (x y : ↥S) : numEdges (inducedSubgraph G S hS) x y = numEdges G ↑x ↑y

Inducing on S preserves edge multiplicities between vertices of S.

theorem Utilities.inducedSubgraph_vertex_card (G : CFGraph) (S : Finset G.V) (hS : S.Nonempty) : Fintype.card (inducedSubgraph G S hS).V = S.card