bounded_lattice (simple_graph V)

Stream: graph theory

[Kyle Miller]

Here's another thing in case someone is looking for something to do. Once #8223 is merged, you can follow the structure of the bounded_lattice G.subgraph instance to define the bounded_lattice (simple_graph V) instance. (This is the lattice of spanning subgraphs of the complete graph.)

Eventually, there should also be a way to go back and forth from spanning subgraphs in G.subgraph to simple_graph V, along with lemmas showing how the subgraph-of relation is preserved.

[Eric Rodriguez]

I was just messing with this (turns out to be an easy copy+paste for the first half)

[Eric Rodriguez]

but for the second half I'm not sure what'd be the best approach; we can just make a simple_graph with some spanning H's adj and call it spanning_coe or something, but feel like that's going to cause more lemmas or something; any further ideas?

[Eric Rodriguez]

(Also, thoughts on changing the defn of is_spanning to H.verts = set.univ? Not sure which is preferred, just a random thought)

[Kyle Miller]

Eric Rodriguez said:

(Also, thoughts on changing the defn of is_spanning to H.verts = set.univ? Not sure which is preferred, just a random thought)

I'd written it like that first, but then I changed it, then thought about changing it back. I'm not sure what's best here... I left it this way just because it seemed like it might be more useful getting a proof that a vertex is an element of H.verts, but if the equality with set.univ proves more useful may as well change it.

[Kyle Miller]

Eric Rodriguez said:

but for the second half I'm not sure what'd be the best approach; we can just make a simple_graph with some spanning H's adj and call it spanning_coe or something, but feel like that's going to cause more lemmas or something; any further ideas?

Going with that name, I'd imagined something like this:

@[simps]
def spanning_coe (G' : subgraph G) (h : G'.is_spanning) : simple_graph V :=
{ adj := G'.adj,
  sym := G'.sym,
  loopless := λ v hv, G.loopless v (G'.adj_sub hv) }

Maybe the only additional things you'd want (for now) are a corresponding isomorphism between G'.coe and G'.spanning_coe h.

[Kyle Miller]

You know, for spanning_coe it makes sense to drop the h hypothesis. Only the isomorphism will need G'.is_spanning.

[Kyle Miller]

I was also imagining a few definitions and lemmas like

@[simps] def simple_graph.to_subgraph {G : simple_graph V} (H : simple_graph V) (h : H ≤ G) :
  G.subgraph := sorry
def simple_graph.to_subgraph.is_spanning {G : simple_graph V} (H : simple_graph V) (h : H ≤ G) :
  (H.to_subgraph h).is_spanning := sorry
lemma subgraph.spanning_coe_is_subgraph_of_is_subgraph (H H' : subgraph G) (h : H ≤ H') :
  H.spanning_coe ≤ H'.spanning_coe := sorry

but it's perfectly fine just PRing the bounded_lattice instance and leaving these to when they're actually needed.

[Eric Rodriguez]

#8330

[Eric Rodriguez]

@Eric Wieser thinks it's a good idea to replace complete_graph and empty_graph (in the aforementioned PR) with ⊤ and ⊥ and i'd be tempted to agree; does anyone have issues with that?

[Kyle Miller]

Eric Rodriguez said:

Eric Wieser thinks it's a good idea to replace complete_graph and empty_graph (in the aforementioned PR) with ⊤ and ⊥ and i'd be tempted to agree; does anyone have issues with that?

I think complete_graph V is nice, rather than ⊤ : simple_graph V, but feel free to remove them.

[Kyle Miller]

I don't think you can rewrite through an abbreviation, but if you could, defining complete_graph V to be an abbreviation for ⊤ might have been a nice synonym.

[Eric Wieser]

Right, the best you can do is have one form simp to the other

[Eric Wieser]

But at that point, either complete_graph appears in no lemma statements, or we have to copy all the API about top to a new API about complete_graph

[Yaël Dillies]

Note that for set α and finset α we use ∅ and univ instead of ⊥ and ⊤. Could we bring in the same approach?

[Kyle Miller]

Very obliquely related to @Yaël Dillies's question, I've been wondering whether mathlib has a way to create the sub-bounded-lattice of all things less than or equal to a particular thing. This would be useful to create the lattice of spanning subgraphs of a particular graph. (The relationship to the question is that this new lattice has its own empty graph.)

[Yakov Pechersky]

Isn't that just the bounded lattice of (coe_sort H) where H : subgraph G?

[Kyle Miller]

@Yakov Pechersky Graphs and subgraphs don't have coe_sort, unlike subobjects of algebraic objects. For the case of bounded_lattice (simple_graph V), it would need to be a bounded lattice instance for something like {G' : simple_graph V // G' ≤ G}. (I'm not very familiar with mathlib's lattice instances.)

[Kyle Miller]

Maybe it's docs#set.Iic.bounded_lattice

[Eric Rodriguez]

Yaël Dillies said:

Note that for set α and finset α we use ∅ and univ instead of ⊥ and ⊤. Could we bring in the same approach?

univ could also be done, and ∅ is just another notation typeclass so again can be done; I'm not so sure about ∅, though; it's nice seeing it and it meaning "definitely set in some form"

[Yaël Dillies]

I didn't mean to reuse univ and ∅! I meant that we could keep complete_graph and empty_graph and have them defeq to ⊥ and ⊤ (and maybe some more technicalities I am unaware of).

[Eric Wieser]

Finset can afford to make that choice because it also chooses to use different symbols for all the lattice operations, so the cost is already paid

[Yakov Pechersky]

Also \empty is relevant for the insert operation.

[Eric Wieser]

Having two ways to write one thing means you either have to simp one form into the other, or write twice as many lemmas

[Eric Wieser]

If you decide to simp top into complete_graph, then you have to copy every lemma like docs#le_top. Finset does this (docs#subset_univ), but only due to a strong convention for using a different notation which I don't think applies to graphs