[Merged by Bors] - feat(combinatorics/simple_graph/hom): add basic definitions and lemmas for finite subgraphs

[jchoules]

We define finsubgraph and its corresponding vertex- and edge-based singletons, and prove some basic ordering lemmas on the singletons. This is primarily preparatory work for proving the De Bruijn-Erdős theorem (generalised to arbitrary finite codomain graphs).

[kmill]

Thanks for following up with this! I have a few comments for now.

[kmill]

I have a branch that defines these two graphs (not as fin_subgraphs though). I'll create a PR soon, merge in some of this PR, and add you as a co-author.

Naming-wise, the temporary names I came up with were simple_graph.singleton_subgraph and simple_graph.subgraph_of_adj, but your names seem good too.

[jchoules]

@kmill Ought I to rebase these changes onto #16435? I'm not sure what the preferred way is in this project to represent such a dependency.

[kmill]

@jchoules There are a couple of options. The first is to wait until the other PR is merged then merge master, and another is to merge the other PR if you want to get things ready ahead of time. Make sure to merge rather than rebase, otherwise you can get some odd git histories, where bors will get confused and attribute this PR to a long list of co-authors!

[jchoules]

I went for the proactive merge. Given that I still need to wrap @kmill's singleton definitions in finiteness proofs to arrive at the definitions I require for the proof here, I've opted to keep the more context-applicable names for those local versions.

Things I'm still unsure about: whether this theorem actually merits a new module; whether the module is appropriately named if so; whether its constituent defs/lemmas/theorems are appropriately located/organised.

[kmill]

Let's just say having a new module is fine. If someone decides otherwise later on it's easy enough to move. This also helps constrain how much category theory affects the combinatorics library.

[kmill]

Once things are wrapped in a namespace and the names are mathlibified, I think I'll be happy to merge it!

[kmill]

Suggested change

	/-! #### Edge deletion -/
	/-! ### Edge deletion -/

[kmill]

Suggested change

	/-! #### Induced subgraphs -/
	/-! ### Induced subgraphs -/

It looks like perhaps git did something weird when merging? (Usually sectioning in a module is at level 3, but maybe you have some other intent?)

[kmill]

Let's wrap all of your code (after or before variables as you prefer) in namespace simple_graph so that every declaration ends up in this namespace. Be sure to remove the simple_graph qualifiers on the two declarations that include it!

[kmill]

Sorry to ask you to change the name of this, but for consistency I would suggest this:

Suggested change

	def vertex_singleton (v : V) : G.fin_subgraph := ⟨simple_graph.singleton_subgraph _ v, by simp⟩
	def singleton_fin_subgraph (v : V) : G.fin_subgraph := ⟨simple_graph.singleton_subgraph _ v, by simp⟩

[kmill]

Again for consistency reasons (sorry):

Suggested change

	def edge_singleton {u v : V} (e : G.adj u v) : G.fin_subgraph :=
	def fin_subgraph_of_adj {u v : V} (e : G.adj u v) : G.fin_subgraph :=

[kmill]

Given the previous suggestions, I might name this as

Suggested change

	lemma vertex_left_le_edge {u v : V} {e : G.adj u v} : vertex_singleton u ≤ edge_singleton e :=
	lemma singleton_fin_subgraph_le_left {u v : V} {e : G.adj u v} : vertex_singleton u ≤ edge_singleton e :=

and the next lemma as singleton_fin_subgraph_le_right.

These are short forms of the way-too-long names like singleton_fin_subgraph_le_fin_subgraph_of_adj_left (I think I'm putting the "left" and "right" in the correct place, but I can't say I have every mathlib naming rule internalized)

[kmill]

If you name it like so (assuming it's been put into the simple_graph namespace as suggested), then later on rather than giving the full name you can write f.restrict h using dot notation.

Suggested change

	def fin_subgraph_hom_restrict {G' G'' : G.fin_subgraph} (h : G'' ≤ G') (f : G' →fg F) : G'' →fg F :=
	def fin_subgraph_hom.restrict {G' G'' : G.fin_subgraph} (h : G'' ≤ G') (f : G' →fg F) : G'' →fg F :=

[kmill]

This might be a mathlib name for this lemma:

Suggested change

	lemma simple_graph.exists_hom_of_all_finite_homs [finite W]
	lemma nonempty_hom_of_forall_fin_subgraph_hom [finite W]

There might also be a variant for pi rather than forall since that's more accurate, but I'd need to check how we do that. In any case, h is morally a forall since you just need it to show all the types in the inverse system are nonempty.

(I still find this lemma to be shocking that it's true. Thanks for formalizing it!)

[kmill]

You can usually combine unfold and simp, since unfold uses simp under the hood to do its unfolding.

Suggested change

	begin
	unfold vertex_singleton edge_singleton, simp,
	end
	by simp [vertex_singleton, edge_singleton]

[YaelDillies]

I think it would be much better to do something like

structure finsubgraph {V : Type u} (G : simple_graph V) :=
(verts : finset V)
(adj : V → V → Prop)
(adj_sub : ∀ {v w : V}, adj v w → G.adj v w)
(edge_vert : ∀ {v w : V}, adj v w → v ∈ verts)
(symm : symmetric adj . obviously)

and provide the coercion to subgraph G separately.

Also note that I'm changing fin_subgraph to finsubgraph to avoid confusion with fin.

[kmill]

@YaelDillies For now, I was wanting to treat finite subgraphs as a construction local to the module, and I'm not sure whether we want to have a whole theory of finsubgraph. (I guess we should make sure the main theorem statement doesn't mention fin_subgraph or ->fg.)

I can imagine a different design where we pass in set or finset as an extra argument to a generalized subgraph type constructor, for example, to save on a lot of code duplication.

[YaelDillies]

Isn't there a version for homs G → complete_graph α (aka α-colorings) that doesn't require any finiteness/countability?

It would be much better if you split this PR into finite subgraphs + compactness of homs.

[kmill]

I suppose we ought to mention what this is related to in the literature:

Suggested change

	a homomorphism from the whole of `G` to `F`. -/
	a homomorphism from the whole of `G` to `F`.
	This is the graph homomorphism version of the **De Bruijn-Erdős theorem**. -/

[YaelDillies]

To follow on my previous comment, you can get rid of the countability assumption on the big graph by considering a hom H → F (H : subgraph G, G : simple_graph α, F : simple_graph β) as a map α → β (padded with a junk value), and then applying Tychonoff (because β is compact with the discrete topology) to find a convergent subsequence, which by construction corresponds to a hom G → F.

[jchoules]

Doesn't β have to be finite to be compact under the discrete topology? That's already the only type whose size is constrained in the current proof statement.

[YaelDillies]

Can you update the PR title/description? It doesn't match the content of this PR at all anymore.

[kmill]

I'm sorry to ask you to do this, but it would be much easier for me if you revert this PR back to this commit, since I would be happy to merge it as-is: https://github.com/leanprover-community/mathlib/blob/1e3380bf80ae9fcc74de8c16bfdf6f4f9d1d4a65/src/combinatorics/simple_graph/finsubgraph.lean

The reason is that the stuff about finsubgraph doesn't make sense without it -- I have a hard time seeing finsubgraph_hom being used for anything except for its use in nonempty_hom_of_forall_finite_subgraph_hom. (I believe we should not develop finsubgraph any more if we can help it, though we can revisit this if someone finds it would be helpful.)

If there exists a reviewer who is happy to review a PR without splitting it, then you generally do not need to split it (especially for such a small PR). PRs that interleave refactors with new material should be split, but this PR is straightforward.

[kmill]

@YaelDillies What are you referring to regarding countability assumptions? This PR is (or was) the application of the Tychonoff theorem to the maximal generality you can apply it.

The key lemma it uses is https://leanprover-community.github.io/mathlib_docs/topology/category/Top/limits.html#nonempty_sections_of_fintype_inverse_system, which is a specialization of https://leanprover-community.github.io/mathlib_docs/topology/category/Top/limits.html#Top.nonempty_limit_cone_of_compact_t2_cofiltered_system to finite sets (since those are the compact discrete spaces). That lemma in turn uses the Tychonoff theorem directly, and the core part of the proof is showing that the subspace corresponding to the inverse system in the infinite product space is an intersection of nonempty closed subsets.

[jchoules]

If we're agreed that the content of the lemma is what it's desired to be, then yeah I can reinstate it no trouble. I agree that finsubgraph doesn't currently need any development beyond what's convenient for this proof, and with your and Yaël's earlier remarks that it would benefit from restructuring if it were to enter public use in future.

[YaelDillies]

Sorry Kyle, I think I got variables-confused once again.

[kmill]

Thanks!

bors r+

[bors]

Build failed (retrying...):

• Lint style

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests