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_3} {W : Type u_5} (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_3} {W : Type u_5} (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_3} {W : Type u_5} {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_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (a✝ : W ⊕ V) : (RelIso.symm sumComm) a✝ = a✝.swap

@[simp]

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

def SimpleGraph.Iso.sumAssoc {U : Type u_1} {V : Type u_3} {W : Type u_5} {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_apply {U : Type u_1} {V : Type u_3} {W : Type u_5} {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✝

@[simp]

theorem SimpleGraph.Iso.sumAssoc_symm_apply {U : Type u_1} {V : Type u_3} {W : Type u_5} {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✝

def SimpleGraph.Embedding.sumInl {V : Type u_3} {W : Type u_5} {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_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (u : V) : sumInl u = Sum.inl u

def SimpleGraph.Embedding.sumInr {V : Type u_3} {W : Type u_5} {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_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (u : W) : sumInr u = Sum.inr u

def SimpleGraph.Hom.sum {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G →g G') (g : H →g H') : G ⊕g H →g G' ⊕g H'

Given homomorphisms f : G →g G' and g : H →g H', returns a homomorphism from G ⊕g H to G' ⊕g H' that applies f to the left component and g to the right component.

Equations

• f.sum g = { toFun := Sum.map ⇑f ⇑g, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.Hom.sum_apply {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G →g G') (g : H →g H') (a✝ : V ⊕ W) : (f.sum g) a✝ = Sum.map (⇑f) (⇑g) a✝

theorem SimpleGraph.Hom.sum_comp_sumComm {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G →g G') (g : H →g H') : (f.sum g).comp Iso.sumComm.toHom = Iso.sumComm.toHom.comp (g.sum f)

theorem SimpleGraph.Hom.sum_sum_comp_sumAssoc {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'} (f : G →g G') (g : H →g H') (h : I →g I') : (f.sum (g.sum h)).comp Iso.sumAssoc.toHom = Iso.sumAssoc.toHom.comp ((f.sum g).sum h)

def SimpleGraph.Embedding.sum {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H'

Given embeddings f : G ↪g G' and g : H ↪g H', returns an embedding from G ⊕g H to G' ⊕g H' that applies f to the left component and g to the right component.

Equations

• f.sum g = { toFun := Sum.map ⇑f ⇑g, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Embedding.sum_apply {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H') (a✝ : V ⊕ W) : (f.sum g) a✝ = Sum.map (⇑f) (⇑g) a✝

theorem SimpleGraph.Embedding.toHom_sum {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H') : (f.sum g).toHom = f.toHom.sum g.toHom

theorem SimpleGraph.Embedding.sum_comp_sumComm {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H') : (g.sum f).comp Iso.sumComm.toEmbedding = Iso.sumComm.toEmbedding.comp (f.sum g)

theorem SimpleGraph.Embedding.sum_sum_comp_sumAssoc {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'} (f : G ↪g G') (g : H ↪g H') (h : I ↪g I') : (f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding = Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)

def SimpleGraph.Iso.sumCongr {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') : G ⊕g H ≃g G' ⊕g H'

Given isomorphisms f : G ≃g G' and g : H ≃g H', returns an isomorphism from G ⊕g H to G' ⊕g H' that applies f to the left component and g to the right component.

Equations

• f.sumCongr g = { toEquiv := f.sumCongr g.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.Iso.sumCongr_symm_apply {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') (a✝ : V' ⊕ W') : (RelIso.symm (f.sumCongr g)) a✝ = Sum.map (⇑f.symm) (⇑g.symm) a✝

@[simp]

theorem SimpleGraph.Iso.sumCongr_apply {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') (a✝ : V ⊕ W) : (f.sumCongr g) a✝ = Sum.map (⇑f) (⇑g) a✝

@[simp]

theorem SimpleGraph.Iso.sumCongr_toEquiv {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') : (f.sumCongr g).toEquiv = f.sumCongr g.toEquiv

theorem SimpleGraph.Iso.toHom_sumCongr {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') : (f.sumCongr g).toHom = f.toHom.sum g.toHom

theorem SimpleGraph.Iso.toEmbedding_sumCongr {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') : (f.sumCongr g).toEmbedding = f.toEmbedding.sum g.toEmbedding

theorem SimpleGraph.Iso.sumComm_comp_sumCongr {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') : sumComm.comp (f.sumCongr g) = (g.sumCongr f).comp sumComm

theorem SimpleGraph.Iso.sumAssoc_comp_sumCongr {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'} (f : G ≃g G') (g : H ≃g H') (h : I ≃g I') : sumAssoc.comp ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc

theorem SimpleGraph.Reachable.sum_sup_edge {V : Type u_3} {W : Type u_5} {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_3} {W : Type u_5} {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_3} {W : Type u_5} {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_3} {W : Type u_5} {γ : Type u_7} {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_3} {W : Type u_5} {γ : Type u_7} {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_3} {W : Type u_5} {γ : Type u_7} {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_3} {W : Type u_5} {γ : Type u_7} {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_3} {W : Type u_5} {γ : Type u_7} {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_3} {W : Type u_5} {γ : Type u_7} {G : SimpleGraph V} {H : SimpleGraph W} (c : (G ⊕g H).Coloring γ) : c.sumLeft.sum c.sumRight = c

def SimpleGraph.Coloring.sumEquiv {V : Type u_3} {W : Type u_5} {γ : Type u_7} {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_3} {W : Type u_5} {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_3} {W : Type u_5} {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_3} {W : Type u_5} {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_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {n : ℕ} (h : (G ⊕g H).Colorable n) : H.Colorable n

@[simp]

theorem SimpleGraph.colorable_sum {V : Type u_3} {W : Type u_5} {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_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} : G.chromaticNumber ≤ (G ⊕g H).chromaticNumber

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

@[simp]

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

theorem SimpleGraph.neighborSet_sum_inl {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (v : V) : (G ⊕g H).neighborSet (Sum.inl v) = Sum.inl '' G.neighborSet v

theorem SimpleGraph.neighborSet_sum_inr {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (w : W) : (G ⊕g H).neighborSet (Sum.inr w) = Sum.inr '' H.neighborSet w

@[implicit_reducible]

instance SimpleGraph.instLocallyFiniteSumSumOfDecidableEq {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} [DecidableEq V] [DecidableEq W] [G.LocallyFinite] [H.LocallyFinite] : (G ⊕g H).LocallyFinite

Equations

• SimpleGraph.instLocallyFiniteSumSumOfDecidableEq v✝ = Sum.casesOn v✝ (fun (v : V) => ⋯.mpr inferInstance) fun (w : W) => ⋯.mpr inferInstance