Stream: graph theory

Topic: bounded_lattice (simple_graph V)

Kyle Miller (Jul 14 2021 at 16:40):

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 (Jul 14 2021 at 20:21):

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

Eric Rodriguez (Jul 14 2021 at 20:22):

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 (Jul 14 2021 at 20:23):

(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 (Jul 14 2021 at 20:32):

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 (Jul 14 2021 at 20:36):

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 :=
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 (Jul 14 2021 at 20:38):

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

Kyle Miller (Jul 14 2021 at 20:48):

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.

#8330

Eric Rodriguez (Jul 16 2021 at 14:38):

@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 (Jul 16 2021 at 16:33):

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 (Jul 16 2021 at 16:35):

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 (Jul 16 2021 at 16:54):

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

Eric Wieser (Jul 16 2021 at 16:58):

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 (Jul 16 2021 at 18:26):

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

Kyle Miller (Jul 16 2021 at 18:48):

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 (Jul 16 2021 at 18:53):

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

Kyle Miller (Jul 16 2021 at 19:03):

@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 (Jul 16 2021 at 19:06):

Maybe it's docs#set.Iic.bounded_lattice

Eric Rodriguez (Jul 16 2021 at 19:17):

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 (Jul 16 2021 at 19:39):

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 (Jul 16 2021 at 20:11):

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 (Jul 16 2021 at 20:11):

Also \empty is relevant for the insert operation.

Eric Wieser (Jul 16 2021 at 20:11):

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 (Jul 16 2021 at 20:13):

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

Last updated: Dec 20 2023 at 11:08 UTC