Operations on cotree representations

Complementation exchanges union and join. A partition with no cross edges allows two cotree representations to be assembled into a representation of the whole graph, using Mathlib's sum of graph isomorphisms.

def SimpleGraph.Iso.complement {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) : Gᶜ ≃g Hᶜ

Complementation transports graph isomorphisms.

Equations

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

def SimpleGraph.Cotree.complement : Cotree → Cotree

Exchange union and join at every internal node.

Equations

• SimpleGraph.Cotree.empty.complement = SimpleGraph.Cotree.empty
• SimpleGraph.Cotree.leaf.complement = SimpleGraph.Cotree.leaf
• (l.union r).complement = l.complement.join r.complement
• (l.join r).complement = l.complement.union r.complement

@[simp]

theorem SimpleGraph.Cotree.complement_complement (t : Cotree) : t.complement.complement = t

Exchanging union and join twice returns the original cotree.

noncomputable def SimpleGraph.Cotree.complementIso (t : Cotree) : t.complement.graph ≃g t.graphᶜ

The complement cotree represents the complement graph.

Equations

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

noncomputable def SimpleGraph.CotreeRepresentation.compl {V : Type u_1} {G : SimpleGraph V} (R : G.CotreeRepresentation) : Gᶜ.CotreeRepresentation

A cotree representation can be complemented without reconstructing the graph.

Equations

• R.compl = { cotree := R.cotree.complement, iso := RelIso.trans R.cotree.complementIso R.iso.complement }

def SimpleGraph.CotreeRepresentation.mapIso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (R : G.CotreeRepresentation) (f : G ≃g H) : H.CotreeRepresentation

Relabel a cotree representation along a graph isomorphism.

Equations

• R.mapIso f = { cotree := R.cotree, iso := RelIso.trans R.iso f }

def SimpleGraph.CotreeRepresentation.sum {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (L : G.CotreeRepresentation) (R : H.CotreeRepresentation) : (G ⊕g H).CotreeRepresentation

Build a disjoint-union representation directly from the supplied cotrees.

Equations

• L.sum R = { cotree := L.cotree.union R.cotree, iso := L.iso.sumCongr R.iso }

def SimpleGraph.CotreeRepresentation.graphJoin {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (L : G.CotreeRepresentation) (R : H.CotreeRepresentation) : (G.graphJoin H).CotreeRepresentation

Build a join representation directly from the supplied cotrees.

Equations

• L.graphJoin R = { cotree := L.cotree.join R.cotree, iso := (L.iso.complement.sumCongr R.iso.complement).complement }

@[simp]

theorem SimpleGraph.graphJoin_adj_inl {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (a b : V) : (G.graphJoin H).Adj (Sum.inl a) (Sum.inl b) ↔ G.Adj a b

Joining preserves adjacency within the left child.

@[simp]

theorem SimpleGraph.graphJoin_adj_inr {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (a b : W) : (G.graphJoin H).Adj (Sum.inr a) (Sum.inr b) ↔ H.Adj a b

Joining preserves adjacency within the right child.

@[simp]

theorem SimpleGraph.graphJoin_adj_inl_inr {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (a : V) (b : W) : (G.graphJoin H).Adj (Sum.inl a) (Sum.inr b)

Every left vertex is adjacent to every right vertex in a join.

@[simp]

theorem SimpleGraph.graphJoin_adj_inr_inl {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (a : W) (b : V) : (G.graphJoin H).Adj (Sum.inr a) (Sum.inl b)

Every right vertex is adjacent to every left vertex in a join.

@[simp]

theorem SimpleGraph.CotreeRepresentation.sum_cotree {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (L : G.CotreeRepresentation) (R : H.CotreeRepresentation) : (L.sum R).cotree = L.cotree.union R.cotree

The union constructor retains its two supplied cotrees.

@[simp]

theorem SimpleGraph.CotreeRepresentation.graphJoin_cotree {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (L : G.CotreeRepresentation) (R : H.CotreeRepresentation) : (L.graphJoin R).cotree = L.cotree.join R.cotree

The join constructor retains its two supplied cotrees.

def SimpleGraph.CotreeRepresentation.ofIsEmpty {V : Type u_1} [IsEmpty V] (G : SimpleGraph V) : G.CotreeRepresentation

An empty vertex type has the empty cotree representation.

Equations

• SimpleGraph.CotreeRepresentation.ofIsEmpty G = { cotree := SimpleGraph.Cotree.empty, iso := id { toEquiv := Equiv.equivOfIsEmpty PEmpty.{1} V, map_rel_iff' := ⋯ } }

noncomputable def SimpleGraph.CotreeRepresentation.ofSubsingleton {V : Type u_1} [Subsingleton V] [Nonempty V] (G : SimpleGraph V) : G.CotreeRepresentation

A one-vertex graph has a one-leaf cotree representation.

Equations

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

noncomputable def SimpleGraph.isoSumInduce {V : Type u_1} {G : SimpleGraph V} (s : Set V) (hcross : ∀ u ∈ s, ∀ v ∉ s, ¬G.Adj u v) : induce s G ⊕g induce sᶜ G ≃g G

A vertex partition with no cross edges gives an isomorphism from the disjoint union of its induced pieces to the original graph.

Equations

• SimpleGraph.isoSumInduce s hcross = { toEquiv := Equiv.Set.sumCompl s, map_rel_iff' := ⋯ }

noncomputable def SimpleGraph.CotreeRepresentation.unionInduce {V : Type u_1} {G : SimpleGraph V} (s : Set V) (hcross : ∀ u ∈ s, ∀ v ∉ s, ¬G.Adj u v) (L : (induce s G).CotreeRepresentation) (R : (induce sᶜ G).CotreeRepresentation) : G.CotreeRepresentation

Assemble representations of two separated induced pieces.

Equations

• SimpleGraph.CotreeRepresentation.unionInduce s hcross L R = { cotree := L.cotree.union R.cotree, iso := RelIso.trans (L.iso.sumCongr R.iso) (SimpleGraph.isoSumInduce s hcross) }