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 : SimpleGraph α) (H : SimpleGraph β) : 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 := ⋯ }

def SimpleGraph.«term_□_» : Lean.TrailingParserDescr

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

• SimpleGraph.«term_□_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_□_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " □ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem SimpleGraph.boxProd_adj {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {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 : SimpleGraph α} {H : SimpleGraph β} {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 : SimpleGraph α} {H : SimpleGraph β} {a : α} {b₁ b₂ : β} : (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂

theorem SimpleGraph.neighborSet_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β) : (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

@[deprecated SimpleGraph.neighborSet_boxProd (since := "2025-05-08")]

theorem SimpleGraph.boxProd_neighborSet {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β) : (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

Alias of SimpleGraph.neighborSet_boxProd.

def SimpleGraph.boxProdComm {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) : G □ H ≃g H □ G

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

Equations

• G.boxProdComm H = { toEquiv := Equiv.prodComm α β, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.boxProdComm_apply {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a✝ : α × β) : (G.boxProdComm H) a✝ = a✝.swap

@[simp]

theorem SimpleGraph.boxProdComm_symm_apply {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a✝ : β × α) : (RelIso.symm (G.boxProdComm H)) a✝ = a✝.swap

def SimpleGraph.boxProdAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : SimpleGraph α) (H : SimpleGraph β) (I : SimpleGraph γ) : 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 := Equiv.prodAssoc α β γ, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.boxProdAssoc_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : SimpleGraph α) (H : SimpleGraph β) (I : SimpleGraph γ) (p : (α × β) × γ) : (G.boxProdAssoc H I) p = (p.1.1, p.1.2, p.2)

@[simp]

theorem SimpleGraph.boxProdAssoc_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : SimpleGraph α) (H : SimpleGraph β) (I : SimpleGraph γ) (p : α × β × γ) : (RelIso.symm (G.boxProdAssoc H I)) p = ((p.1, p.2.1), p.2.2)

def SimpleGraph.boxProdLeft {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (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' := ⋯ }

@[simp]

theorem SimpleGraph.boxProdLeft_apply {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (b : β) (a : α) : (G.boxProdLeft H b) a = (a, b)

def SimpleGraph.boxProdRight {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a : α) : H ↪g G □ H

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

Equations

• G.boxProdRight H a = { toFun := Prod.mk a, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.boxProdRight_apply {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a : α) (snd : β) : (G.boxProdRight H a) snd = (a, snd)

def SimpleGraph.Walk.boxProdLeft {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (H : SimpleGraph β) {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

• SimpleGraph.Walk.boxProdLeft H b = SimpleGraph.Walk.map (G.boxProdLeft H b).toHom

def SimpleGraph.Walk.boxProdRight {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) {H : SimpleGraph β} {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

• SimpleGraph.Walk.boxProdRight G a = SimpleGraph.Walk.map (G.boxProdRight H a).toHom

def SimpleGraph.Walk.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [DecidableEq β] [DecidableRel G.Adj] {x y : α × β} : (G □ H).Walk x y → G.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

def SimpleGraph.Walk.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [DecidableEq α] [DecidableRel H.Adj] {x y : α × β} : (G □ H).Walk x y → H.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

@[simp]

theorem SimpleGraph.Walk.ofBoxProdLeft_boxProdLeft {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [DecidableEq β] [DecidableRel G.Adj] {a₁ a₂ : α} {b : β} (w : G.Walk a₁ a₂) : (Walk.boxProdLeft H b w).ofBoxProdLeft = w

@[simp]

theorem SimpleGraph.Walk.ofBoxProdRight_boxProdRight {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [DecidableRel G.Adj] {a b₁ b₂ : α} (w : G.Walk b₁ b₂) : (Walk.boxProdRight G a w).ofBoxProdRight = w

@[deprecated SimpleGraph.Walk.ofBoxProdRight_boxProdRight (since := "2025-03-30")]

theorem SimpleGraph.Walk.ofBoxProdLeft_boxProdRight {α : Type u_1} {G : SimpleGraph α} [DecidableEq α] [DecidableRel G.Adj] {a b₁ b₂ : α} (w : G.Walk b₁ b₂) : (Walk.boxProdRight G a w).ofBoxProdRight = w

Alias of SimpleGraph.Walk.ofBoxProdRight_boxProdRight.

@[irreducible]

theorem SimpleGraph.Walk.length_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {a₁ a₂ : α} {b₁ b₂ : β} [DecidableEq α] [DecidableEq β] [DecidableRel G.Adj] [DecidableRel H.Adj] (w : (G □ H).Walk (a₁, b₁) (a₂, b₂)) : w.length = w.ofBoxProdLeft.length + w.ofBoxProdRight.length

theorem SimpleGraph.Preconnected.boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (hG : G.Preconnected) (hH : H.Preconnected) : (G □ H).Preconnected

theorem SimpleGraph.Preconnected.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [Nonempty β] (h : (G □ H).Preconnected) : G.Preconnected

theorem SimpleGraph.Preconnected.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [Nonempty α] (h : (G □ H).Preconnected) : H.Preconnected

theorem SimpleGraph.Connected.boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (hG : G.Connected) (hH : H.Connected) : (G □ H).Connected

theorem SimpleGraph.Connected.ofBoxProdLeft {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (h : (G □ H).Connected) : G.Connected

theorem SimpleGraph.Connected.ofBoxProdRight {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (h : (G □ H).Connected) : H.Connected

@[simp]

theorem SimpleGraph.connected_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : (G □ H).Connected ↔ G.Connected ∧ H.Connected

@[deprecated SimpleGraph.connected_boxProd (since := "2025-05-08")]

theorem SimpleGraph.boxProd_connected {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : (G □ H).Connected ↔ G.Connected ∧ H.Connected

Alias of SimpleGraph.connected_boxProd.

instance SimpleGraph.boxProdFintypeNeighborSet {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (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.neighborFinset_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (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) ⋯

@[deprecated SimpleGraph.neighborFinset_boxProd (since := "2025-05-08")]

theorem SimpleGraph.boxProd_neighborFinset {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (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) ⋯

Alias of SimpleGraph.neighborFinset_boxProd.

theorem SimpleGraph.degree_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (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

@[deprecated SimpleGraph.degree_boxProd (since := "2025-05-08")]

theorem SimpleGraph.boxProd_degree {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (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

Alias of SimpleGraph.degree_boxProd.

theorem SimpleGraph.reachable_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x y : α × β} : (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

@[deprecated SimpleGraph.reachable_boxProd (since := "2025-05-08")]

theorem SimpleGraph.boxProd_reachable {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x y : α × β} : (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Alias of SimpleGraph.reachable_boxProd.

@[simp]

theorem SimpleGraph.edist_boxProd {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x y : α × β) : (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

@[deprecated SimpleGraph.edist_boxProd (since := "2025-05-08")]

theorem SimpleGraph.boxProd_edist {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x y : α × β) : (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Alias of SimpleGraph.edist_boxProd.