Contracting edges

Lax871432.Contractions · concepts/Lax871432/Contractions.lean · lax-871432

definition

Loading review…

Natural Language Statement

Definition

A graph $K$ is obtained from a simple graph $F$ by contracting edges when the vertices of $K$ are the classes of a partition $\mathcal{R}$ of $V(F)$ into parts inducing connected subgraphs, two distinct classes being adjacent in $K$ exactly when $F$ joins a vertex of one to a vertex of the other. In the notation of the paper, $K \cong F/\mathcal{R}$ .

Concept map

1 concept; 6 descendants hidden

100%

Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 4 of this submission's paper

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
2
3	/-!
4	---
5	title: Contracting edges
6	type: definition
7	---
8	A graph $K$ is obtained from a simple graph $F$ by contracting edges when the vertices of
9	$K$ are the classes of a partition $\mathcal{R}$ of $V(F)$ into parts inducing connected
10	subgraphs, two distinct classes being adjacent in $K$ exactly when $F$ joins a vertex of one
11	to a vertex of the other. In the notation of the paper, $K \cong F/\mathcal{R}$ .
12
13	# Implementation notes
14
15	The partition is presented by the map sending a vertex of $F$ to its class, rather than as a
16	quotient type, so that $K$ may be any graph isomorphic to $F/\mathcal{R}$ and no transport
17	along a quotient is needed. Surjectivity of that map is not assumed: it follows, since a
18	connected graph is nonempty.
19
20	Contracting edges differs from taking minors, `Lax68.GraphMinors.IsMinor`, in two ways: the
21	classes must cover all of $V(F)$ , and every adjacency of $F$ between distinct classes must be
22	present in $K$ , not merely permitted.
23	-/
24
25	namespace Lax871432.Contractions
26
27	/-- A presentation of `K` as the graph obtained from `F` by contracting the edges inside the
28	classes of a partition of `V(F)` into connected parts. -/
29	structure Contraction {V W : Type*} (K : SimpleGraph W) (F : SimpleGraph V) where
30	/-- The vertex of `K` a vertex of `F` is contracted to. -/
31	proj : V → W
32	/-- Each class induces a connected — in particular nonempty — subgraph of `F`. -/
33	connected : ∀ w, (F.induce {v \| proj v = w}).Connected
34	/-- Distinct classes are adjacent in `K` exactly when `F` joins them. -/
35	adj_iff : ∀ a b, K.Adj a b ↔ a ≠ b ∧ ∃ x y, F.Adj x y ∧ proj x = a ∧ proj y = b
36
37	/-- `K` is obtained from `F` by contracting edges. -/
38	def IsContraction {V W : Type*} (K : SimpleGraph W) (F : SimpleGraph V) : Prop :=
39	Nonempty (Contraction K F)
40
41	end Lax871432.Contractions
42

Implementation notes

The partition is presented by the map sending a vertex of $F$ to its class, rather than as a quotient type, so that $K$ may be any graph isomorphic to $F/\mathcal{R}$ and no transport along a quotient is needed. Surjectivity of that map is not assumed: it follows, since a connected graph is nonempty.

Contracting edges differs from taking minors, $Lax68.GraphMinors.IsMinor$ , in two ways: the classes must cover all of $V(F)$ , and every adjacency of $F$ between distinct classes must be present in $K$ , not merely permitted.

Builds on

none

Used by

Lax871432.ClosureProperties

From Mathlib

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Contracting edges

Flags

Flag this concept