# mathlib3documentation

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 β) :

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
@[simp]
theorem simple_graph.box_prod_adj {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {x y : α × β} :
@[simp]
theorem simple_graph.box_prod_adj_left {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {a₁ a₂ : α} {b : β} :
@[simp]
theorem simple_graph.box_prod_adj_right {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} {a : α} {b₁ b₂ : β} :
theorem simple_graph.box_prod_neighbor_set {α : Type u_1} {β : Type u_2} {G : simple_graph α} {H : simple_graph β} (x : α × β) :
@[simp]
theorem simple_graph.box_prod_comm_symm_apply {α : Type u_1} {β : Type u_2} (G : simple_graph α) (H : simple_graph β) (ᾰ : β × α) :
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
@[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
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
@[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
@[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
@[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
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
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
@[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₂) :
@[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₂) :
@[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) :
@[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) :
@[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 β} :
@[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)] :
Equations
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