mathlib3 documentation

combinatorics.simple_graph.prod

Graph products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the box product of graphs and other product constructions. The box product of G and H is the graph on the product of the vertices such that x and y are related iff they agree on one component and the other one is related via either G or H. For example, the box product of two edges is a square.

Main declarations #

simple_graph.box_prod: The box product.

Notation #

G □ H: The box product of G and H.

TODO #

Define all other graph products!

def simple_graph.box_prod {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) :

simple_graph (α × β)

Box product of simple graphs. It relates (a₁, b) and (a₂, b) if G relates a₁ and a₂, and (a, b₁) and (a, b₂) if H relates b₁ and b₂.

Equations

G □ H = {adj := λ (x y : α × β), G.adj x.fst y.fst ∧ x.snd = y.snd ∨ H.adj x.snd y.snd ∧ x.fst = y.fst, symm := _, loopless := _}

@[simp]

theorem simple_graph.box_prod_adj {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {x y : α × β} :

(G □ H).adj x y ↔ G.adj x.fst y.fst ∧ x.snd = y.snd ∨ H.adj x.snd y.snd ∧ x.fst = y.fst

@[simp]

theorem simple_graph.box_prod_adj_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {a₁ a₂ : α} {b : β} :

(G □ H).adj (a₁, b) (a₂, b) ↔ G.adj a₁ a₂

@[simp]

theorem simple_graph.box_prod_adj_right {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {a : α} {b₁ b₂ : β} :

(G □ H).adj (a, b₁) (a, b₂) ↔ H.adj b₁ b₂

theorem simple_graph.box_prod_neighbor_set {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (x : α × β) :

(G □ H).neighbor_set x = G.neighbor_set x.fst ×ˢ {x.snd} ∪ {x.fst} ×ˢ H.neighbor_set x.snd

@[simp]

theorem simple_graph.box_prod_comm_symm_apply {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (ᾰ : β × α) :

⇑(rel_iso.symm (G.box_prod_comm H)) ᾰ = ᾰ.swap

def simple_graph.box_prod_comm {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) :

G □ H ≃g H □ G

The box product is commutative up to isomorphism. equiv.prod_comm as a graph isomorphism.

Equations

G.box_prod_comm H = {to_equiv := equiv.prod_comm α β, map_rel_iff' := _}

@[simp]

theorem simple_graph.box_prod_comm_apply {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (ᾰ : α × β) :

⇑(G.box_prod_comm H) ᾰ = ᾰ.swap

@[simp]

theorem simple_graph.box_prod_assoc_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : simple_graph α) (H : simple_graph β) (I : simple_graph γ) (p : α × β × γ) :

⇑(rel_iso.symm (G.box_prod_assoc H I)) p = ((p.fst, p.snd.fst), p.snd.snd)

@[simp]

theorem simple_graph.box_prod_assoc_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : simple_graph α) (H : simple_graph β) (I : simple_graph γ) (p : (α × β) × γ) :

⇑(G.box_prod_assoc H I) p = (p.fst.fst, p.fst.snd, p.snd)

def simple_graph.box_prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : simple_graph α) (H : simple_graph β) (I : simple_graph γ) :

G □ H □ I ≃g G □ (H □ I)

The box product is associative up to isomorphism. equiv.prod_assoc as a graph isomorphism.

Equations

G.box_prod_assoc H I = {to_equiv := equiv.prod_assoc α β γ, map_rel_iff' := _}

def simple_graph.box_prod_left {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (b : β) :

G ↪g G □ H

The embedding of G into G □ H given by b.

Equations

G.box_prod_left H b = {to_embedding := {to_fun := λ (a : α), (a, b), inj' := _}, map_rel_iff' := _}

@[simp]

theorem simple_graph.box_prod_left_apply {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (b : β) (a : α) :

⇑(G.box_prod_left H b) a = (a, b)

def simple_graph.box_prod_right {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (a : α) :

H ↪g G □ H

The embedding of H into G □ H given by a.

Equations

G.box_prod_right H a = {to_embedding := {to_fun := prod.mk a, inj' := _}, map_rel_iff' := _}

@[simp]

theorem simple_graph.box_prod_right_apply {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (a : α) (snd : β) :

⇑(G.box_prod_right H a) snd = (a, snd)

@[protected]

def simple_graph.walk.box_prod_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} (H : simple_graph β) {a₁ a₂ : α} (b : β) :

G.walk a₁ a₂ → (G □ H).walk (a₁, b) (a₂, b)

Turn a walk on G into a walk on G □ H.

Equations

simple_graph.walk.box_prod_left H b = simple_graph.walk.map (G.box_prod_left H b).to_hom

@[protected]

def simple_graph.walk.box_prod_right {α : Type u_1} {β : Type u_2} (G : simple_graph α) {H : simple_graph β} {b₁ b₂ : β} (a : α) :

H.walk b₁ b₂ → (G □ H).walk (a, b₁) (a, b₂)

Turn a walk on H into a walk on G □ H.

Equations

simple_graph.walk.box_prod_right G a = simple_graph.walk.map (G.box_prod_right H a).to_hom

def simple_graph.walk.of_box_prod_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} [decidable_eq β] [decidable_rel G.adj] {x y : α × β} :

(G □ H).walk x y → G.walk x.fst y.fst

Project a walk on G □ H to a walk on G by discarding the moves in the direction of H.

Equations

(simple_graph.walk.cons h w).of_box_prod_left = or.by_cases h (λ (hG : G.adj x.fst a_6.fst ∧ x.snd = a_6.snd), simple_graph.walk.cons _ w.of_box_prod_left) (λ (hH : H.adj x.snd a_6.snd ∧ x.fst = a_6.fst), show G.walk x.fst z.fst, from _.mpr w.of_box_prod_left)
simple_graph.walk.nil.of_box_prod_left = simple_graph.walk.nil

def simple_graph.walk.of_box_prod_right {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} [decidable_eq α] [decidable_rel H.adj] {x y : α × β} :

(G □ H).walk x y → H.walk x.snd y.snd

Project a walk on G □ H to a walk on H by discarding the moves in the direction of G.

Equations

(simple_graph.walk.cons h w).of_box_prod_right = _.by_cases (λ (hH : H.adj x.snd a_15.snd ∧ x.fst = a_15.fst), simple_graph.walk.cons _ w.of_box_prod_right) (λ (hG : G.adj x.fst a_15.fst ∧ x.snd = a_15.snd), show H.walk x.snd z.snd, from _.mpr w.of_box_prod_right)
simple_graph.walk.nil.of_box_prod_right = simple_graph.walk.nil

@[simp]

theorem simple_graph.walk.of_box_prod_left_box_prod_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {b : β} [decidable_eq β] [decidable_rel G.adj] {a₁ a₂ : α} (w : G.walk a₁ a₂) :

(simple_graph.walk.box_prod_left H b w).of_box_prod_left = w

@[simp]

theorem simple_graph.walk.of_box_prod_left_box_prod_right {α : Type u_1} {G : simple_graph α} {a : α} [decidable_eq α] [decidable_rel G.adj] {b₁ b₂ : α} (w : G.walk b₁ b₂) :

(simple_graph.walk.box_prod_right G a w).of_box_prod_right = w

@[protected]

theorem simple_graph.preconnected.box_prod {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (hG : G.preconnected) (hH : H.preconnected) :

(G □ H).preconnected

@[protected]

theorem simple_graph.preconnected.of_box_prod_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} [nonempty β] (h : (G □ H).preconnected) :

@[protected]

theorem simple_graph.preconnected.of_box_prod_right {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} [nonempty α] (h : (G □ H).preconnected) :

@[protected]

theorem simple_graph.connected.box_prod {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (hG : G.connected) (hH : H.connected) :

(G □ H).connected

@[protected]

theorem simple_graph.connected.of_box_prod_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (h : (G □ H).connected) :

@[protected]

theorem simple_graph.connected.of_box_prod_right {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (h : (G □ H).connected) :

@[simp]

theorem simple_graph.box_prod_connected {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} :

(G □ H).connected ↔ G.connected ∧ H.connected

@[protected, instance]

def simple_graph.box_prod_fintype_neighbor_set {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (x : α × β) [fintype ↥(G.neighbor_set x.fst)] [fintype ↥(H.neighbor_set x.snd)] :

fintype ↥((G □ H).neighbor_set x)

Equations

simple_graph.box_prod_fintype_neighbor_set x = fintype.of_equiv ↥((G.neighbor_finset x.fst ×ˢ {x.snd}).disj_union ({x.fst} ×ˢ H.neighbor_finset x.snd) _) ((equiv.refl (α × β)).subtype_equiv _)

theorem simple_graph.box_prod_neighbor_finset {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (x : α × β) [fintype ↥(G.neighbor_set x.fst)] [fintype ↥(H.neighbor_set x.snd)] [fintype ↥((G □ H).neighbor_set x)] :

(G □ H).neighbor_finset x = (G.neighbor_finset x.fst ×ˢ {x.snd}).disj_union ({x.fst} ×ˢ H.neighbor_finset x.snd) _

theorem simple_graph.box_prod_degree {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (x : α × β) [fintype ↥(G.neighbor_set x.fst)] [fintype ↥(H.neighbor_set x.snd)] [fintype ↥((G □ H).neighbor_set x)] :

(G □ H).degree x = G.degree x.fst + H.degree x.snd