Edge labellings

Stream: Is there code for X?

[Nir Paz]

Is the concept of edge labellings on simple graphs in mathlib?

I want to formalize infinite Ramsey's theorem but couldn't find anything I can use besides the basic definitions for graphs.

[Kyle Miller]

I don't believe there's anything about edge labelings in particular. You can formalize them in a number of ways:

1. functions G.edge_set -> L
2. functions Sym2 V -> L, where you only ever look at values on G.edge_set
3. functions Sym2 V -> Option L, where the image is not-none iff the input is in G.edge_set
4. functions V -> V -> L or V -> V -> Option L that are symmetric (but at this point, you probably want the next option)
5. reformalize simple graphs to be labeled simple graphs, with a function V -> V -> Option L rather than V -> V -> Prop, and, if needed, create a label-erase map to SimpleGraph V, along with lemmas carrying structure over from one to the other. (Then a labeling of a simple graph would be a LabeledSimpleGraph V L that maps to it.)

Which you choose depends on what you need out of the structure. For example, if you don't need the lattice structure on SimpleGraph, or any of the theory of subgraphs, you could probably do well with working right with symmetric V -> V -> Option L functions.

[Vincent Beffara]

6. reformalize graphs to use Serre's definition and use E -> L is also a possibility

[Yaël Dillies]

I believe @Bhavik Mehta has infinite Ramsey? Not sure anymore

[Felix Weilacher]

A formalization of infinite Ramsey's theorem probably shouldn't mention graphs. I would expect it to be about something like functions Finset Nat -> L for L some finite type.

[Felix Weilacher]

Maybe functions Sym2 Nat -> L if you are only interested in the 2-dimensional statement?

[Nir Paz]

Felix Weilacher said:

A formalization of infinite Ramsey's theorem probably shouldn't mention graphs. I would expect it to be about something like functions Finset Nat -> L for L some finite type.

I wouldn't want to work with graphs just doing it for fun, I assumed graphs were best if I wanted it to be mathlib approp. But maybe doing something like this and proving the graph version later is better

[Bhavik Mehta]

I have infinite Ramsey in Lean 3, it's linked from Freek's page. I also have edge labellings for the ramsey project. I agree that infinite hypergraph Ramsey shouldn't need to mention graphs - just like anything else about hypergraphs. My code for edge labellings is pretty close to PR-able, I just haven't got round to it: it's the top half of https://github.com/b-mehta/ExponentialRamsey/blob/master/ExponentialRamsey/Prereq/Ramsey.lean

[Bhavik Mehta]

My infinite Ramsey code is compact but impenetrable, so I'd have no objection to someone just starting fresh. I do think however that the statement I had was the correct one to formalise, and that (even for a personal project) the hypergraph version is better to do. In particular going straight for hypergraphs rather than simple graphs means the induction is quite a bit easier to run. I also don't mind trying to do this myself, but I can't give any time estimate on when I'd be able to

[Peter Nelson]

#12167 does the infinite Ramsey theorem for hypergraphs. The finite versions will follow once Konig's infinity lemma is proved.

[Kyle Miller]

I have some Lean 3 proofs of Konig's lemma, but do you need that? Could you apply a general compactness argument instead?

Here are two examples in mathlib: https://github.com/leanprover-community/mathlib4/blob/ca1a851ae33af82f567dde4f039ee30747494fd8/Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean#L119-L153 https://github.com/leanprover-community/mathlib4/blob/ca1a851ae33af82f567dde4f039ee30747494fd8/Mathlib/Combinatorics/Hall/Basic.lean#L123-L163

These are using category theory language: every inverse system of nonempty finite sets is nonempty. docs#nonempty_sections_of_finite_inverse_system