# Zulip Chat Archive

## 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 :=
{ 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 (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.

#### Eric Rodriguez (Jul 16 2021 at 10:25):

#### 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: Aug 03 2023 at 10:10 UTC