Zulip Chat Archive

Stream: graph theory

Topic: compactness for graph homomorphisms

Joanna Choules (Aug 29 2022 at 22:30):

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 (Aug 29 2022 at 23:36):

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⟩, _


((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 (Aug 30 2022 at 09:15):

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 (Sep 04 2022 at 00:39):

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 (Sep 05 2022 at 11:28):

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 (Sep 05 2022 at 11:32):

It's #16382

Last updated: Dec 20 2023 at 11:08 UTC