Disjoint sum of graphs

This file defines the disjoint sum of graphs. The disjoint sum of G : SimpleGraph α and H : SimpleGraph β is a graph on α ⊕ β where u and v are adjacent if and only if they are both in G and adjacent in G, or they are both in H and adjacent in H.

Main declarations

• SimpleGraph.Sum: The disjoint sum of graphs.

Notation

• G ⊕g H: The disjoint sum of G and H.

def SimpleGraph.sum {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α ⊕ β)

Disjoint sum of G and H.

@[simp]

theorem SimpleGraph.sum_adj {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (x✝ x✝¹ : α ⊕ β) : (G ⊕g H).Adj x✝ x✝¹ = match x✝, x✝¹ with | Sum.inl u, Sum.inl v => G.Adj u v | Sum.inr u, Sum.inr v => H.Adj u v | x, x_1 => False

def SimpleGraph.«term_⊕g_» : Lean.TrailingParserDescr

Disjoint sum of G and H.

def SimpleGraph.Iso.sumComm {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : G ⊕g H ≃g H ⊕g G

The disjoint sum is commutative up to isomorphism. Iso.sumComm as a graph isomorphism.

@[simp]

theorem SimpleGraph.Iso.sumComm_symm_apply {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (a✝ : β ⊕ α) : (RelIso.symm sumComm) a✝ = a✝.swap

@[simp]

theorem SimpleGraph.Iso.sumComm_apply {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (a✝ : α ⊕ β) : sumComm a✝ = a✝.swap

def SimpleGraph.Iso.sumAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} {I : SimpleGraph γ} : G ⊕g H ⊕g I ≃g G ⊕g (H ⊕g I)

The disjoint sum is associative up to isomorphism. Iso.sumAssoc as a graph isomorphism.

@[simp]

theorem SimpleGraph.Iso.sumAssoc_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} {I : SimpleGraph γ} (a✝ : α ⊕ β ⊕ γ) : (RelIso.symm sumAssoc) a✝ = Sum.elim (Sum.inl ∘ Sum.inl) (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr) a✝

@[simp]

theorem SimpleGraph.Iso.sumAssoc_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} {I : SimpleGraph γ} (a✝ : (α ⊕ β) ⊕ γ) : sumAssoc a✝ = Sum.elim (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl)) (Sum.inr ∘ Sum.inr) a✝

def SimpleGraph.Embedding.sumInl {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : G ↪g G ⊕g H

The embedding of G into G ⊕g H.

@[simp]

theorem SimpleGraph.Embedding.sumInl_apply {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (u : α) : sumInl u = Sum.inl u

def SimpleGraph.Embedding.sumInr {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : H ↪g G ⊕g H

The embedding of H into G ⊕g H.

@[simp]

theorem SimpleGraph.Embedding.sumInr_apply {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (u : β) : sumInr u = Sum.inr u

def SimpleGraph.Coloring.sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} (cG : G.Coloring γ) (cH : H.Coloring γ) : (G ⊕g H).Coloring γ

Color G ⊕g H with colorings of G and H

def SimpleGraph.Coloring.sumLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} (c : (G ⊕g H).Coloring γ) : G.Coloring γ

Get coloring of G from coloring of G ⊕g H

def SimpleGraph.Coloring.sumRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} (c : (G ⊕g H).Coloring γ) : H.Coloring γ

Get coloring of H from coloring of G ⊕g H

@[simp]

theorem SimpleGraph.Coloring.sumLeft_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumLeft = cG

@[simp]

theorem SimpleGraph.Coloring.sumRight_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumRight = cH

@[simp]

theorem SimpleGraph.Coloring.sum_sumLeft_sumRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} (c : (G ⊕g H).Coloring γ) : c.sumLeft.sum c.sumRight = c

def SimpleGraph.Coloring.sumEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {G : SimpleGraph α} {H : SimpleGraph β} : (G ⊕g H).Coloring γ ≃ G.Coloring γ × H.Coloring γ

Bijection between (G ⊕g H).Coloring γ and G.Coloring γ × H.Coloring γ

def SimpleGraph.Coloring.sumFin {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {n m : ℕ} (cG : G.Coloring (Fin n)) (cH : H.Coloring (Fin m)) : (G ⊕g H).Coloring (Fin (max n m))

Color G ⊕g H with Fin (n + m) given a coloring of G with Fin n and a coloring of H with Fin m

theorem SimpleGraph.Colorable.sum_max {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {n m : ℕ} (hG : G.Colorable n) (hH : H.Colorable m) : (G ⊕g H).Colorable (max n m)

theorem SimpleGraph.Colorable.of_sum_left {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {n : ℕ} (h : (G ⊕g H).Colorable n) : G.Colorable n

theorem SimpleGraph.Colorable.of_sum_right {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {n : ℕ} (h : (G ⊕g H).Colorable n) : H.Colorable n

@[simp]

theorem SimpleGraph.colorable_sum {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {n : ℕ} : (G ⊕g H).Colorable n ↔ G.Colorable n ∧ H.Colorable n

theorem SimpleGraph.chromaticNumber_le_sum_left {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : G.chromaticNumber ≤ (G ⊕g H).chromaticNumber

theorem SimpleGraph.chromaticNumber_le_sum_right {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : H.chromaticNumber ≤ (G ⊕g H).chromaticNumber

@[simp]

theorem SimpleGraph.chromaticNumber_sum {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} : (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber