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 β) (u v : α ⊕ β) : (G ⊕g H).Adj u v = match u, v 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_apply {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (a✝ : α ⊕ β) : SimpleGraph.Iso.sumComm a✝ = a✝.swap

@[simp]

theorem SimpleGraph.Iso.sumComm_symm_apply {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (a✝ : β ⊕ α) : (RelIso.symm SimpleGraph.Iso.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 SimpleGraph.Iso.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✝ : (α ⊕ β) ⊕ γ) : SimpleGraph.Iso.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 : α) : SimpleGraph.Embedding.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 : β) : SimpleGraph.Embedding.sumInr u = Sum.inr u