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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SimpleGraph.«term_⊕g_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_⊕g_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕g ") (Lean.ParserDescr.cat `term 61))

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.

Equations

• SimpleGraph.Iso.sumComm = { toEquiv := Equiv.sumComm α β, map_rel_iff' := ⋯ }

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

Equations

• SimpleGraph.Iso.sumAssoc = { toEquiv := Equiv.sumAssoc α β γ, map_rel_iff' := ⋯ }

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

Equations

• SimpleGraph.Embedding.sumInl = { toFun := fun (u : α) => Sum.inl u, inj' := ⋯, map_rel_iff' := ⋯ }

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

Equations

• SimpleGraph.Embedding.sumInr = { toFun := fun (u : β) => Sum.inr u, inj' := ⋯, map_rel_iff' := ⋯ }

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

Equations

• cG.sum cH = { toFun := Sum.elim ⇑cG ⇑cH, map_rel' := ⋯ }

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

Equations

• c.sumLeft = SimpleGraph.Hom.comp c SimpleGraph.Embedding.sumInl.toHom

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

Equations

• c.sumRight = SimpleGraph.Hom.comp c SimpleGraph.Embedding.sumInr.toHom

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• cG.sumFin cH = ((G.recolorOfEmbedding (Fin.castLEEmb ⋯)) cG).sum ((H.recolorOfEmbedding (Fin.castLEEmb ⋯)) cH)

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