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


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 (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