Disjoint sum of graphs

This file defines the disjoint sum of graphs. The disjoint sum of G : SimpleGraph V and H : SimpleGraph W is a graph on V ⊕ W 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 {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) : SimpleGraph (V ⊕ W)

Disjoint sum of G and H.

Equations

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

@[simp]

theorem SimpleGraph.sum_adj {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) (x✝ x✝¹ : V ⊕ W) : (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 {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} : 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 V W, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

def SimpleGraph.Iso.sumAssoc {V : Type u_1} {W : Type u_2} {U : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U} : 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 V W U, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Iso.sumAssoc_symm_apply {V : Type u_1} {W : Type u_2} {U : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U} (a✝ : V ⊕ W ⊕ U) : (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 {V : Type u_1} {W : Type u_2} {U : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U} (a✝ : (V ⊕ W) ⊕ U) : sumAssoc a✝ = Sum.elim (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl)) (Sum.inr ∘ Sum.inr) a✝

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

The embedding of G into G ⊕g H.

Equations

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

@[simp]

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

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

The embedding of H into G ⊕g H.

Equations

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

@[simp]

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

theorem SimpleGraph.Reachable.sum_sup_edge {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {v v' : V} {w w' : W} (hv : G.Reachable v v') (hw : H.Reachable w w') : ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v') (Sum.inr w')

theorem SimpleGraph.Preconnected.sum_sup_edge {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {v : V} {w : W} (hG : G.Preconnected) (hH : H.Preconnected) : ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Preconnected

theorem SimpleGraph.Connected.sum_sup_edge {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {v : V} {w : W} (hG : G.Connected) (hH : H.Connected) : ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected

def SimpleGraph.Coloring.sum {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} (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 {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} (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 {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} (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 {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumLeft = cG

@[simp]

theorem SimpleGraph.Coloring.sumRight_sum {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumRight = cH

@[simp]

theorem SimpleGraph.Coloring.sum_sumLeft_sumRight {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} (c : (G ⊕g H).Coloring γ) : c.sumLeft.sum c.sumRight = c

def SimpleGraph.Coloring.sumEquiv {V : Type u_1} {W : Type u_2} {γ : Type u_4} {G : SimpleGraph V} {H : SimpleGraph W} : (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 {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {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 {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {n m : ℕ} (hG : G.Colorable n) (hH : H.Colorable m) : (G ⊕g H).Colorable (max n m)

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

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

@[simp]

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

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

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

@[simp]

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