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

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

@[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

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.

@[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

@[simp]

theorem SimpleGraph.boxProdComm_apply {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a✝ : α × β) : (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.

@[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)

@[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)

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.

@[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.

@[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.Iso.boxProdSumDistrib {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂) : G □ (H₁ ⊕g H₂) ≃g G □ H₁ ⊕g G □ H₂

The box product distributes over the disjoint sum of graphs.

@[simp]

theorem SimpleGraph.Iso.boxProdSumDistrib_symm_apply {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂) (a✝ : V × W₁ ⊕ V × W₂) : (RelIso.symm (boxProdSumDistrib G H₁ H₂)) a✝ = ((Equiv.sumProdDistrib W₁ W₂ V).symm (Sum.map Prod.swap Prod.swap a✝)).swap

@[simp]

theorem SimpleGraph.Iso.boxProdSumDistrib_apply {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂) (a✝ : V × (W₁ ⊕ W₂)) : (boxProdSumDistrib G H₁ H₂) a✝ = Sum.map Prod.swap Prod.swap ((Equiv.sumProdDistrib W₁ W₂ V) a✝.swap)

@[simp]

theorem SimpleGraph.Iso.boxProdSumDistrib_toEquiv {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂) : (boxProdSumDistrib G H₁ H₂).toEquiv = Equiv.prodSumDistrib V W₁ W₂

def SimpleGraph.Iso.sumBoxProdDistrib {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W) : (G₁ ⊕g G₂) □ H ≃g G₁ □ H ⊕g G₂ □ H

The box product distributes over the disjoint sum of graphs.

@[simp]

theorem SimpleGraph.Iso.sumBoxProdDistrib_symm_apply {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W) (s : V₁ × W ⊕ V₂ × W) : (RelIso.symm (sumBoxProdDistrib G₁ G₂ H)) s = Sum.elim (Prod.map Sum.inl id) (Prod.map Sum.inr id) s

@[simp]

theorem SimpleGraph.Iso.sumBoxProdDistrib_apply {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W) (p : (V₁ ⊕ V₂) × W) : (sumBoxProdDistrib G₁ G₂ H) p = Sum.map (fun (x : V₁) => (x, p.2)) (fun (x : V₂) => (x, p.2)) p.1

@[simp]

theorem SimpleGraph.Iso.sumBoxProdDistrib_toEquiv {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W) : (sumBoxProdDistrib G₁ G₂ H).toEquiv = Equiv.sumProdDistrib V₁ V₂ W

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.

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.

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.

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.

@[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

@[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

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)

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) ⋯

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

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

@[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