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.boxProd_neighborSet {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β) : SimpleGraph.neighborSet (G □ H) x = SimpleGraph.neighborSet G x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ SimpleGraph.neighborSet H x.2

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem SimpleGraph.boxProdAssoc_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : SimpleGraph α) (H : SimpleGraph β) (I : SimpleGraph γ) (p : α × β × γ) : (RelIso.symm (SimpleGraph.boxProdAssoc G 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 : (α × β) × γ) : (SimpleGraph.boxProdAssoc G H I) p = (p.1.1, p.1.2, p.2)

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

• SimpleGraph.boxProdAssoc G H I = { toEquiv := Equiv.prodAssoc α β γ, map_rel_iff' := ⋯ }

@[simp]

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

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

• SimpleGraph.boxProdLeft G H b = { toEmbedding := { toFun := fun (a : α) => (a, b), inj' := ⋯ }, map_rel_iff' := ⋯ }

@[simp]

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

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

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

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

Equations

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

instance SimpleGraph.boxProdFintypeNeighborSet {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β) [Fintype ↑(SimpleGraph.neighborSet G x.1)] [Fintype ↑(SimpleGraph.neighborSet H x.2)] : Fintype ↑(SimpleGraph.neighborSet (G □ H) 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 : SimpleGraph α} {H : SimpleGraph β} (x : α × β) [Fintype ↑(SimpleGraph.neighborSet G x.1)] [Fintype ↑(SimpleGraph.neighborSet H x.2)] [Fintype ↑(SimpleGraph.neighborSet (G □ H) x)] : SimpleGraph.neighborFinset (G □ H) x = Finset.disjUnion (SimpleGraph.neighborFinset G x.1 ×ˢ {x.2}) ({x.1} ×ˢ SimpleGraph.neighborFinset H x.2) ⋯

theorem SimpleGraph.boxProd_degree {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β) [Fintype ↑(SimpleGraph.neighborSet G x.1)] [Fintype ↑(SimpleGraph.neighborSet H x.2)] [Fintype ↑(SimpleGraph.neighborSet (G □ H) x)] : SimpleGraph.degree (G □ H) x = SimpleGraph.degree G x.1 + SimpleGraph.degree H x.2