Disjoint sums of graphs

Three gaps in Mathlib's SimpleGraph.sum API.

SimpleGraph.sum has no DecidableRel instance in Mathlib. Consequently, even when adjacency in both summands is decidable, (G ⊕g H).edgeFinset is not expressible without supplying an instance. TauCeti.instDecidableRelSumAdj supplies it by the four-way case split in the definition of SimpleGraph.sum.

Nor does it describe the graphs containing a disjoint sum: SimpleGraph.sum_le_iff says a graph on V ⊕ W contains G ⊕g H exactly when its two sides contain G and H, which is how containing a disjoint union of patterns splits into two independent containment events.

SimpleGraph.sum has no bot law in Mathlib either: TauCeti.SimpleGraph.sum_bot_bot says a disjoint sum of edgeless graphs is edgeless, the form in which a graph parameter that is multiplicative over disjoint sums is evaluated on an edgeless graph.

Main results

• TauCeti.instDecidableRelSumAdj — adjacency in a disjoint sum is decidable;
• SimpleGraph.sum_le_iff — a graph contains a disjoint sum exactly when its two sides contain the summands;
• TauCeti.SimpleGraph.sum_bot_bot — a disjoint sum of edgeless graphs is edgeless.

@[instance_reducible]

instance TauCeti.instDecidableRelSumAdj {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊕g H).Adj

Adjacency in a disjoint sum of graphs is decidable: SimpleGraph.sum splits on which sides its two arguments lie, and vertices on opposite sides are never adjacent.

Equations

• TauCeti.instDecidableRelSumAdj G H (Sum.inl u) (Sum.inl v) = inst✝¹ u v
• TauCeti.instDecidableRelSumAdj G H (Sum.inr u) (Sum.inr v) = inst✝ u v
• TauCeti.instDecidableRelSumAdj G H (Sum.inl val) (Sum.inr val_1) = isFalse ⋯
• TauCeti.instDecidableRelSumAdj G H (Sum.inr val) (Sum.inl val_1) = isFalse ⋯

@[simp]

theorem SimpleGraph.sum_le_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {K : SimpleGraph (V ⊕ W)} : G ⊕g H ≤ K ↔ G ≤ SimpleGraph.comap Sum.inl K ∧ H ≤ SimpleGraph.comap Sum.inr K

A graph on V ⊕ W contains the disjoint sum G ⊕g H exactly when its restrictions to the two sides contain G and H: the sum has no edges across the sides.

theorem TauCeti.SimpleGraph.sum_bot_bot {V : Type u_1} {W : Type u_2} : ⊥ ⊕g ⊥ = ⊥

A disjoint sum of edgeless graphs is edgeless: no edge is contributed by either summand, and none across the two sides.