# Documentation

Mathlib.Combinatorics.SimpleGraph.Prod

# Graph products #

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 #

• SimpleGraph.boxProd: The box product.

## Notation #

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

## TODO #

Define all other graph products!

def SimpleGraph.boxProd {α : Type u_1} {β : Type u_2} (G : ) (H : ) :
SimpleGraph (α × β)

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₂.

Instances For

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₂.

Instances For
@[simp]
theorem SimpleGraph.boxProd_adj {α : Type u_1} {β : Type u_2} {G : } {H : } {x : α × β} {y : α × β} :
SimpleGraph.Adj (G H) x y SimpleGraph.Adj G x.fst y.fst x.snd = y.snd SimpleGraph.Adj H x.snd y.snd x.fst = y.fst
theorem SimpleGraph.boxProd_adj_left {α : Type u_1} {β : Type u_2} {G : } {H : } {a₁ : α} {b : β} {a₂ : α} :
theorem SimpleGraph.boxProd_adj_right {α : Type u_1} {β : Type u_2} {G : } {H : } {a : α} {b₁ : β} {b₂ : β} :
theorem SimpleGraph.boxProd_neighborSet {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) :
@[simp]
theorem SimpleGraph.boxProdComm_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) :
∀ (a : α × β), ↑() a =
@[simp]
theorem SimpleGraph.boxProdComm_symm_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) :
∀ (a : β × α), ↑() a =
def SimpleGraph.boxProdComm {α : Type u_1} {β : Type u_2} (G : ) (H : ) :
G H ≃g H G

The box product is commutative up to isomorphism. Equiv.prodComm as a graph isomorphism.

Instances For
@[simp]
theorem SimpleGraph.boxProdAssoc_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : ) (H : ) (I : ) (p : α × β × γ) :
↑() p = ((p.fst, p.snd.fst), p.snd.snd)
@[simp]
theorem SimpleGraph.boxProdAssoc_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : ) (H : ) (I : ) (p : (α × β) × γ) :
↑() p = (p.fst.fst, p.fst.snd, p.snd)
def SimpleGraph.boxProdAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : ) (H : ) (I : ) :
G H I ≃g G (H I)

The box product is associative up to isomorphism. Equiv.prodAssoc as a graph isomorphism.

Instances For
@[simp]
theorem SimpleGraph.boxProdLeft_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) (b : β) (a : α) :
↑() a = (a, b)
def SimpleGraph.boxProdLeft {α : Type u_1} {β : Type u_2} (G : ) (H : ) (b : β) :
G ↪g G H

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

Instances For
@[simp]
theorem SimpleGraph.boxProdRight_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) (a : α) (snd : β) :
↑() snd = (a, snd)
def SimpleGraph.boxProdRight {α : Type u_1} {β : Type u_2} (G : ) (H : ) (a : α) :
H ↪g G H

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

Instances For
def SimpleGraph.Walk.boxProdLeft {α : Type u_1} {β : Type u_2} {G : } (H : ) {a₁ : α} {a₂ : α} (b : β) :
SimpleGraph.Walk G a₁ a₂SimpleGraph.Walk (G H) (a₁, b) (a₂, b)

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

Instances For
def SimpleGraph.Walk.boxProdRight {α : Type u_1} {β : Type u_2} (G : ) {H : } {b₁ : β} {b₂ : β} (a : α) :
SimpleGraph.Walk H b₁ b₂SimpleGraph.Walk (G H) (a, b₁) (a, b₂)

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

Instances For
def SimpleGraph.Walk.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } [] [DecidableRel G.Adj] {x : α × β} {y : α × β} :
SimpleGraph.Walk (G H) x ySimpleGraph.Walk G 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
Instances For
def SimpleGraph.Walk.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : } {H : } [] [DecidableRel H.Adj] {x : α × β} {y : α × β} :
SimpleGraph.Walk (G H) x ySimpleGraph.Walk H 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
Instances For
@[simp]
theorem SimpleGraph.Walk.ofBoxProdLeft_boxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } {b : β} [] [DecidableRel G.Adj] {a₁ : α} {a₂ : α} (w : SimpleGraph.Walk G a₁ a₂) :
@[simp]
theorem SimpleGraph.Walk.ofBoxProdLeft_boxProdRight {α : Type u_1} {G : } {a : α} [] [DecidableRel G.Adj] {b₁ : α} {b₂ : α} (w : SimpleGraph.Walk G b₁ b₂) :
theorem SimpleGraph.Preconnected.boxProd {α : Type u_1} {β : Type u_2} {G : } {H : } (hG : ) (hH : ) :
theorem SimpleGraph.Preconnected.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } [] (h : ) :
theorem SimpleGraph.Preconnected.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : } {H : } [] (h : ) :
theorem SimpleGraph.Connected.boxProd {α : Type u_1} {β : Type u_2} {G : } {H : } (hG : ) (hH : ) :
theorem SimpleGraph.Connected.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } (h : SimpleGraph.Connected (G H)) :
theorem SimpleGraph.Connected.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : } {H : } (h : SimpleGraph.Connected (G H)) :
@[simp]
theorem SimpleGraph.boxProd_connected {α : Type u_1} {β : Type u_2} {G : } {H : } :
instance SimpleGraph.boxProdFintypeNeighborSet {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) [Fintype ↑(SimpleGraph.neighborSet G x.fst)] [Fintype ↑(SimpleGraph.neighborSet H x.snd)] :
theorem SimpleGraph.boxProd_neighborFinset {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) [Fintype ↑(SimpleGraph.neighborSet G x.fst)] [Fintype ↑(SimpleGraph.neighborSet H x.snd)] [Fintype ↑(SimpleGraph.neighborSet (G H) x)] :
SimpleGraph.neighborFinset (G H) x = Finset.disjUnion ( ×ˢ {x.snd}) ({x.fst} ×ˢ ) (_ : Disjoint ( ×ˢ {x.snd}) ({x.fst} ×ˢ ))
theorem SimpleGraph.boxProd_degree {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) [Fintype ↑(SimpleGraph.neighborSet G x.fst)] [Fintype ↑(SimpleGraph.neighborSet H x.snd)] [Fintype ↑(SimpleGraph.neighborSet (G H) x)] :