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

Equations
• G H = { Adj := fun (x y : α × β) => G.Adj x.1 y.1 x.2 = y.2 H.Adj x.2 y.2 x.1 = y.1, symm := , loopless := }
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₂.

Equations
Instances For
@[simp]
theorem SimpleGraph.boxProd_adj {α : Type u_1} {β : Type u_2} {G : } {H : } {x : α × β} {y : α × β} :
(G H).Adj x y G.Adj x.1 y.1 x.2 = y.2 H.Adj x.2 y.2 x.1 = y.1
theorem SimpleGraph.boxProd_adj_left {α : Type u_1} {β : Type u_2} {G : } {H : } {a₁ : α} {b : β} {a₂ : α} :
(G H).Adj (a₁, b) (a₂, b) G.Adj a₁ a₂
theorem SimpleGraph.boxProd_adj_right {α : Type u_1} {β : Type u_2} {G : } {H : } {a : α} {b₁ : β} {b₂ : β} :
(G H).Adj (a, b₁) (a, b₂) H.Adj b₁ b₂
theorem SimpleGraph.boxProd_neighborSet {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) :
(G H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} {x.1} ×ˢ H.neighborSet x.2
@[simp]
theorem SimpleGraph.boxProdComm_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) :
∀ (a : α × β), (G.boxProdComm H) a = a.swap
@[simp]
theorem SimpleGraph.boxProdComm_symm_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) :
∀ (a : β × α), (RelIso.symm (G.boxProdComm H)) a = a.swap
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.

Equations
• G.boxProdComm H = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.boxProdAssoc_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : ) (H : ) (I : ) (p : α × β × γ) :
(RelIso.symm (G.boxProdAssoc H I)) p = ((p.1, p.2.1), p.2.2)
@[simp]
theorem SimpleGraph.boxProdAssoc_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : ) (H : ) (I : ) (p : (α × β) × γ) :
(G.boxProdAssoc H I) p = (p.1.1, p.1.2, p.2)
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.

Equations
• G.boxProdAssoc H I = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.boxProdLeft_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) (b : β) (a : α) :
(G.boxProdLeft H b) 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.

Equations
• G.boxProdLeft H b = { toFun := fun (a : α) => (a, b), inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem SimpleGraph.boxProdRight_apply {α : Type u_1} {β : Type u_2} (G : ) (H : ) (a : α) (snd : β) :
(G.boxProdRight H a) 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.

Equations
• G.boxProdRight H a = { toFun := , inj' := , map_rel_iff' := }
Instances For
def SimpleGraph.Walk.boxProdLeft {α : Type u_1} {β : Type u_2} {G : } (H : ) {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
Instances For
def SimpleGraph.Walk.boxProdRight {α : Type u_1} {β : Type u_2} (G : ) {H : } {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
Instances For
def SimpleGraph.Walk.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } [] [DecidableRel G.Adj] {x : α × β} {y : α × β} :
(G H).Walk x yG.Walk x.1 y.1

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

Equations
• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.ofBoxProdLeft = SimpleGraph.Walk.nil
Instances For
def SimpleGraph.Walk.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : } {H : } [] [DecidableRel H.Adj] {x : α × β} {y : α × β} :
(G H).Walk x yH.Walk x.2 y.2

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

Equations
• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.ofBoxProdRight = SimpleGraph.Walk.nil
Instances For
@[simp]
theorem SimpleGraph.Walk.ofBoxProdLeft_boxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } {b : β} [] [DecidableRel G.Adj] {a₁ : α} {a₂ : α} (w : G.Walk a₁ a₂) :
().ofBoxProdLeft = w
@[simp]
theorem SimpleGraph.Walk.ofBoxProdLeft_boxProdRight {α : Type u_1} {G : } {a : α} [] [DecidableRel G.Adj] {b₁ : α} {b₂ : α} (w : G.Walk b₁ b₂) :
().ofBoxProdRight = w
theorem SimpleGraph.Preconnected.boxProd {α : Type u_1} {β : Type u_2} {G : } {H : } (hG : G.Preconnected) (hH : H.Preconnected) :
(G H).Preconnected
theorem SimpleGraph.Preconnected.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } [] (h : (G H).Preconnected) :
G.Preconnected
theorem SimpleGraph.Preconnected.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : } {H : } [] (h : (G H).Preconnected) :
H.Preconnected
theorem SimpleGraph.Connected.boxProd {α : Type u_1} {β : Type u_2} {G : } {H : } (hG : G.Connected) (hH : H.Connected) :
(G H).Connected
theorem SimpleGraph.Connected.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : } {H : } (h : (G H).Connected) :
G.Connected
theorem SimpleGraph.Connected.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : } {H : } (h : (G H).Connected) :
H.Connected
@[simp]
theorem SimpleGraph.boxProd_connected {α : Type u_1} {β : Type u_2} {G : } {H : } :
(G H).Connected G.Connected H.Connected
instance SimpleGraph.boxProdFintypeNeighborSet {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] :
Fintype ((G H).neighborSet x)
Equations
• One or more equations did not get rendered due to their size.
theorem SimpleGraph.boxProd_neighborFinset {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] [Fintype ((G H).neighborSet x)] :
(G H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2)
theorem SimpleGraph.boxProd_degree {α : Type u_1} {β : Type u_2} {G : } {H : } (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] [Fintype ((G H).neighborSet x)] :
(G H).degree x = G.degree x.1 + H.degree x.2