Defining the ends

Stream: graph theory

[Rémi Bottinelli]

Hey,

I'm trying to define the ends of a graph and have written some code towards that **here**.
As of now, there is a working (up to a few sorrys) definition of the ends, but nothing is proved about them.
I feel like the code structure is far from ideal, and would like to get some feedback in order to have a better base to work on.

If anyone is up for having a look, here are a few questions I have:

• I'm defining the set of ends manually as a set of functions satisfying some commutation properties, but it's really just a filtered (co?)limit.
  Are there built-ins I should use for that? In particular, at some point I'd like to say that this limit is entirely defined by any "cofinal" subdiagram, for which it would be easier to just pluck a lemma from somewhere else.

• At line 507, if I replace the λ ⟨f,f_comm⟩, by λ f,, then LEAN gets stuck at parsing this line, and I have no idea why.

• Related to the bullet above, when defining functions by destructuring in a lambda like that, I get _match hypothesis in all the proofs and I'm not sure how to deal with them properly to prove things.
• I'm still mystified by the proper use of parameters and variables, which makes my code very dirty. Same thing for instances.
• Am I right assuming that is_connected is not built-in the simple_graph api yet?

Thanks :)

[Kyle Miller]

simple_graph.connected is in #12574, which I think @Bhavik Mehta is happy with, but it won't be in mathlib until that's merged

[Kyle Miller]

Nice to see work on ends. Quite a while back I'd defined them as (effectively) a limit on subgraphs induced by cofinite vertex subsets, using the pi_0 functor (implemented specially for graphs). I didn't do much with it and didn't like how it was going, and it's probably safe to assume that particular code is lost.

[Kyle Miller]

Maybe looking at some of the code around docs#nonempty_sections_of_fintype_inverse_system might give ideas for how to put things in terms of (cofiltered) limits. I'm only pointing toward this one because I'm familiar with it.

[Kyle Miller]

For line 507, if you're wanting to pattern match like that, it's usually better to use match directly or to use a definition's built-in match syntax:

def to_ends_for (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  ends → ends_for ℱ H ℱ_cofin
| ⟨f, f_comm⟩ := ...

[Kyle Miller]

Incidentally, you can write that whole definition as

def to_ends_for (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  ends → ends_for ℱ H ℱ_cofin
| ⟨f, f_comm⟩ := ⟨λ K, f ⟨K, H K.property⟩, λ K L hKL,
                  f_comm (set.inclusion H K) (set.inclusion H L) hKL⟩

[Kyle Miller]

Regarding parameters vs variables: I suggest that you use variables unless you know parameters would make things nicer. I don't think I've contributed code that's used parameters, for what it's worth. (You could search the mathlib repository for parameter to see how they're used.)

[Kyle Miller]

I forgot to mention: one reason I pointed out docs#nonempty_sections_of_fintype_inverse_system is that it might be useful for things about ends, since it's the category theory version of Konig's lemma, so for example given an end I think you can use it to prove there's an infinite ray to that end.

[Rémi Bottinelli]

Great, thanks for all the feedback :)

[Rémi Bottinelli]

Re. the pi_0 approach: it might indeed be the case that a more high-level definition makes more sense… I'm not sure

[Rémi Bottinelli]

Kyle Miller said:

Incidentally, you can write that whole definition as

def to_ends_for (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  ends → ends_for ℱ H ℱ_cofin
| ⟨f, f_comm⟩ := ⟨λ K, f ⟨K, H K.property⟩, λ K L hKL,
                  f_comm (set.inclusion H K) (set.inclusion H L) hKL⟩

It seems that doing this, I can't unfold the def anymore. Why would that be?

[Kyle Miller]

There's another PR for connected components in the works (#12766, @Bhavik Mehta and I were just trying to decide how to set it up) and it would be nice to have a followup PR about functoriality properties. I think @Joseph Hua was working on induced subgraphs. We will also have a way to map walks from a subgraph to a supergraph (I was planning on getting to that eventually). Once all that is in, then one way to organize a formalization of ends is in terms of the limit of connected components of induced subgraphs of cofinite vertex sets in a fairly direct way.

That all said, it's probably better not to wait -- your being the vanguard is helpful to see what's missing and to see what kinds of theorems the library should support. I like to avoid PRing definitions unless they've proven themselves in theorems.

[Kyle Miller]

Rémi Bottinelli said:

It seems that doing this, I can't unfold the def anymore. Why would that be?

It's because of the equation lemmas it generates are different. Try doing #print prefix simple_graph.ends.to_ends_for (I'm guessing the namespace there) before and after the change.

[Kyle Miller]

If you really want to unfold, I think tactic#delta should work. But, if you're unfolding, you might instead think about what you're trying to accomplish by unfolding and write a lemma that accomplishes what you want directly.

[Rémi Bottinelli]

but aren't you going to unfold in the lemma in that case? As far as I managed, it seemed except for simple simp doing things for me, I always need one unfold.

[Kyle Miller]

Yeah, you'll need to unfold things sometimes, it's just worth thinking about whether you're doing this because you're missing specialized lemmas.

One I tried to write is

lemma to_ends_for_def (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) (e : ends) :
  (to_ends_for ℱ H ℱ_cofin e).val = λ (K : ℱ), e.1 ⟨K, H K.property⟩ :=
begin
  sorry
end

but it seems to cause Lean to hang, and I'm not sure why.

[Kyle Miller]

By the way, did you take a look at the equation lemmas?

Abbreviated:

#print prefix simple_graph.connected_outside.ends.to_ends_for.equations

to_ends_for ℱ H ℱ_cofin ⟨f, f_comm⟩ = ⟨λ (K : ↥ℱ), f ⟨↑K, _⟩, _⟩

This means that when you unfold, you need the ends argument to be a constructor. One way to use it is to do cases on that argument first. For example:

lemma to_of_ends_for_is_id  (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  (to_ends_for ℱ H ℱ_cofin) ∘ (of_ends_for ℱ H ℱ_cofin) = id :=
begin
  apply funext,
  rintros ⟨g, hg⟩,
  simp [of_ends_for, to_ends_for],
  sorry
end

[Kyle Miller]

(You can collapse the apply/rintros lines into a single ext1 ⟨g, hg⟩)

[Rémi Bottinelli]

ah, it sort of makes sense that since the definition of to_ends_for is in terms of a constructor, you need to unfold it likwise.

[Rémi Bottinelli]

Re. equations lemmas: So, whenever I want to unfold/simp a def, if things don't go as well as I'd like, I should inspect #print prefix path.to.def.equations to see if there is one that applies?

[Rémi Bottinelli]

lemma to_of_ends_for_is_id  (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  (to_ends_for ℱ H ℱ_cofin) ∘ (of_ends_for ℱ H ℱ_cofin) = id :=
begin
  apply funext,
  rintros ⟨g, g_comm⟩,
  simp [of_ends_for, to_ends_for],
  apply funext,
  rintros F,
  apply g_comm,
end

Here we go, thanks!

[Kyle Miller]

Yeah, that's what I usually do to debug definitions.

[Kyle Miller]

Shorter but equivalent proof:

begin
  ext1 ⟨g, g_comm⟩,
  simp [of_ends_for, to_ends_for],
  ext1 F,
  apply g_comm,
end

[Kyle Miller]

To make that mathlib-ready, you'd want to get rid of that "non-terminal simp". I replaced simp with squeeze_simp to get a suggestion:

begin
  ext1 ⟨g, g_comm⟩,
  simp only [of_ends_for, to_ends_for, comp_app, id.def, subtype.mk_eq_mk],
  ext1 F,
  apply g_comm,
end

[Rémi Bottinelli]

non-terminal simp means a simp which uses unknown assumptions?

[Rémi Bottinelli]

And both directions (to_of and of_to) work with the same proof, perfect!

[Kyle Miller]

That, and also it's not the last tactic in a block. To make mathlib easier to maintain, every time you use simp you need to either use simp only or make it clear what it's supposed to simp into.

[Kyle Miller]

This way, if someone adds or removes a simp lemma, in the first case it won't break your proof, and in the second they'll have an easier time fixing your proof.

[Rémi Bottinelli]

That makes sense, OK

[Kyle Miller]

You'll probably find an application version of this lemma to be more useful, so you probably should factor it out:

@[simp]
lemma to_of_ends_for_apply  (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val)
  (e : ends_for ℱ H ℱ_cofin) :
  to_ends_for ℱ H ℱ_cofin (of_ends_for ℱ H ℱ_cofin e) = e :=
begin
  obtain ⟨g, g_comm⟩ := e,
  simp only [of_ends_for, to_ends_for, comp_app, id.def, subtype.mk_eq_mk],
  ext1 F,
  apply g_comm,
end

lemma to_of_ends_for_is_id  (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  (to_ends_for ℱ H ℱ_cofin) ∘ (of_ends_for ℱ H ℱ_cofin) = id :=
begin
  ext1 e,
  simp,
end

[Kyle Miller]

But then again, even better would be to package these up using docs#equiv so you get these sorts of lemmas "for free".

def to_ends_for' (ℱ ⊆ finsubsets) (ℱ_cofin : ∀ K : finsubsets, ∃ F : ℱ, K.val ⊆ F.val) :
  ends ≃ ends_for ℱ H ℱ_cofin :=
{ to_fun := to_ends_for ℱ H ℱ_cofin,
  inv_fun := of_ends_for ℱ H ℱ_cofin,
  left_inv := begin
    rintro ⟨g, g_comm⟩,
    simp only [of_ends_for, to_ends_for, comp_app, id.def, subtype.mk_eq_mk],
    ext1 F,
    apply g_comm,
  end,
  right_inv := begin
    rintro ⟨g, g_comm⟩,
    simp only [of_ends_for, to_ends_for, comp_app, id.def, subtype.mk_eq_mk],
    ext1 F,
    apply g_comm,
  end }

[Rémi Bottinelli]

Kyle Miller said:

There's another PR for connected components in the works (#12766, Bhavik Mehta and I were just trying to decide how to set it up) and it would be nice to have a followup PR about functoriality properties. I think Joseph Hua was working on induced subgraphs. We will also have a way to map walks from a subgraph to a supergraph (I was planning on getting to that eventually). Once all that is in, then one way to organize a formalization of ends is in terms of the limit of connected components of induced subgraphs of cofinite vertex sets in a fairly direct way.

That all said, it's probably better not to wait -- your being the vanguard is helpful to see what's missing and to see what kinds of theorems the library should support. I like to avoid PRing definitions unless they've proven themselves in theorems.

About this. Can you ping me as soon as the necessary definitions for this approach are there, so that I can migrate when that makes sense?

[Rémi Bottinelli]

lol, if each of your new message results in a new piece of code like that, I'll have a fully fledged formalization by noon :)

[Rémi Bottinelli]

(I did have equiv in mind, but thought the two composites being the identity was somewhat of a necessary intermediary step anyway)

[Rémi Bottinelli]

Btw, I was wondering if some kind of "inductive equational" definition for the ends of a graph as

  Ends(\emptyset) = \emptyset
  \forall K finite, \Ends(X) = \bigsqcup_{C : components of X-K} \Ends(C)

could make sense. This specific definition doesn't work since setting Ends(X) = \emptyset for all X is a solution.

[Rémi Bottinelli]

Great news: the empty set has no ends:

lemma ends_empty_graph : is_empty V → is_empty (ends G) :=
begin
  rintros ⟨no_V⟩,
  apply is_empty.mk,
  rintros ⟨f,f_comm⟩,
  rcases f ⟨∅,set.finite_empty⟩ with ⟨a,⟨b,_⟩,is_inf⟩,
  exact no_V b,
end

[Rémi Bottinelli]

Thinking about it some more, proving that ends X = \bigsqcup_{C : components of X-K} ends Cis going to require some back and forth and glue code for induced subgraphs, using the plain approach I chose, while the pi₀ one is probably going to make it almost trivial.

[Rémi Bottinelli]

Hey, we (@Anand Rao and I) have refactored our definition of ends, and I've whipped up a PR here. Would very much welcome opinions on whether this is an agreeable formulation.

The idea, instead of formalizing everything up to Freudenthal-Hopf, and then being hopeless to ever get all of it in mathlib (which was the strategy until now), is to instead just make minimal PRs merged as soon as possible: this seems to work better in my limited experience.

[Rémi Bottinelli]

Waiting for the PR to move, I've tried to prove that the subtype of ends choosing a particular connected component is equivalent to the type of ends of that particular component here.
The proof works, but I feel like this is way too long for such a simple statement, and there should be a way to get it way shorter, without as many auxiliary definitions and lemmas.
Also, I got into some strange behaviours:

• simplifying using dif_pos h doesn't work, but doing a split_ifs does.
• rw works while simp and simp_rw don't (I expect it to be due to rw being better at matching lemmas where not all arguments are given).

This all looks like I'm not taking the right approach.