minors of simple graphs

Stream: graph theory

[Kyle Miller]

Is there a type for intervals in a lattice? This is a way to model minors of a simple graph, where the lower bound is the contracted edges and the upper bound is the edges that haven't been deleted.

This makes commutativity of contraction and deletion rather straightforward, since it's essentially the fact that inf and sup distribute.

Then if it's needed, you can realize a minor as a simple_graph by quotienting the upper graph by the lower graph and removing isolated vertices and self loops.

namespace simple_graph

structure minor (V : Type*) :=
(A B : simple_graph V)
(le : A ≤ B)

variables {V : Type*}

/-- The minors of a graph are those that are contained withn it. -/
def minors (G : simple_graph V) : set (minor V) :=
{M | M.B ≤ G}

namespace minor
variables {G : simple_graph V}

/-- The vertex type for the realization of a minor is the support of the
top graph modulo the adjacency relation of the bottom graph. -/
def realize_verts (M : minor V) := @quot M.B.support (λ v w, M.A.adj v w)

/-- Realize the minor as a simple graph, deleting all isolated vertices and self-loops that would form. -/
def realize (M : minor V) : simple_graph M.realize_verts :=
{ adj := λ v w, v ≠ w ∧ ∃ v' w', quot.mk _ v' = v ∧ quot.mk _ w' = w ∧ M.A.adj v' w',
  symm := begin
    intros v w,
    dsimp,
    rintro ⟨h1, h2⟩,
    use ne.symm h1,
    obtain ⟨v', w', hv', hw', ha⟩ := h2,
    use [w', v', hw', hv', M.A.symm ha],
  end,
  loopless := begin
    rintros v ⟨h1, h2⟩,
    exact h1 rfl,
  end }

def sup (M M' : minor V) : minor V :=
{ A := M.A ⊔ M'.A,
  B := M.B ⊔ M'.B,
  le := sup_le_sup M.le M'.le }

def inf (M M' : minor V) : minor V :=
{ A := M.A ⊓ M'.A,
  B := M.B ⊓ M'.B,
  le := inf_le_inf M.le M'.le }

def compl (M : minor V) : minor V :=
{ A := M.Bᶜ,
  B := M.Aᶜ,
  le := compl_le_compl M.le }

def incl (G : simple_graph V) : minor V :=
{ A := ⊥,
  B := G,
  le := bot_le }

-- now we have
-- 1. edge deletion = inf (incl G) (compl H), where H is the graph with the edges we want to delete
-- 2. edge contraction = sup (incl G) H, where H is the graph with the edges we want to contract

end minor

end simple_graph

[Kyle Miller]

Intervals in a lattice also form a lattice, right? (The operations are in the code block above.)

[Bryan Gin-ge Chen]

There's: https://leanprover-community.github.io/mathlib_docs/order/lattice_intervals.html

[Kyle Miller]

Thanks, those at least give the lattice structure of a particular interval, which is helpful (in particular docs#set.Icc.bounded_lattice), but there's additional structure on the set of intervals themselves (i.e., on the set of all morphisms of the poset category).

I haven't actually checked carefully if there's a partial order on intervals that works, but I was guessing it'd be [a,b] <= [c,d] iff a <= c and b <= d, which corresponds to [a,c] and [b,d] forming a commuting square in the category.