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

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