compactness for graph homomorphisms

Stream: graph theory

[Joanna Choules]

Joanna Choules said:

Kyle Miller said:

I guess there's a more general result, which is if G' is a finite graph and if every finite subgraph of G has a homomorphism to G', then there is a homomorphism from G to G'.

Do you happen to know if this is already being worked on currently? I thought I would try the proof myself out of curiosity, and I've been making reasonable headway, but I'm conscious of not duplicating effort.

After a substantial hiatus, I've picked this up again, but there are certain parts of the Hall theorem proof whose type-correctness I don't quite understand (and which, perhaps more importantly, I can't seem to replicate in my own proof).

In particular, at https://github.com/leanprover-community/mathlib/blob/b490ab4ac99873a41a6fc5731cb548728d6df9d5/src/combinatorics/hall/basic.lean#L156, why does Lean let us apply the injectivity of uii' directly to an equality of type ((hall_matchings_functor t).map _ uii').val ⟨i, _⟩ = ((hall_matchings_functor t).map _ uii').val ⟨i', _⟩, especially considering that the morphisms passed to map (underscored here for brevity) are different on the LHS and RHS (and, indeed, not even of the same type)?

[Junyan Xu]

By unfolding the definitions I see that

(hall_matchings_functor t).map x uii'

is by definition

hall_matchings_on.restrict t (category_theory.le_of_hom x.unop) uii'

which is by definition

⟨λ i, uii'.val ⟨i, x i.property⟩, _⟩

so

((hall_matchings_functor t).map _ uii').val ⟨i, _⟩

is defeq to

uii'.val ⟨i, _⟩

So uii'.property.1 h is a proof of ⟨i, _⟩ = ⟨i', _⟩ and
subtype.mk_eq_mk.mp (uii'.property.1 h) is a proof of i = i'.

[Joanna Choules]

Ah ok, so I have to make sure that the type checker can reach through to the restriction function - I'll see what I can do about that. Thanks!

[Joanna Choules]

The proof is finished now; I'll submit a PR for it within the next day or two.
[cc. @Kyle Miller - I should (fingers crossed) be able to knock out the specialisation to colorings without too much trouble, assuming it doesn't already exist as its own lemma?]

[Joanna Choules]

The PR is up - I added Kyle Miller as a potential reviewer but I'd be glad of anyone's eyes who'd like to look it over.

[Kevin Buzzard]

It's #16382