Homomorphisms from finite subgraphs #
This file defines the type of finite subgraphs of a
SimpleGraph and proves a compactness result
for homomorphisms to a finite codomain.
Main statements #
SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom: If every finite subgraph of a (possibly infinite) graph
Ghas a homomorphism to some finite graph
F, then there is also a homomorphism
G →g F.
→fg is a module-local variant on
→g where the domain is a finite subgraph of some supergraph
Implementation notes #
The proof here uses compactness as formulated in
G'' ≤ G', the inverse system
finsubgraphHomFunctor restricts homomorphisms
G' →fg F to domain
Given a homomorphism from a subgraph to
F, construct its restriction to a sub-subgraph.
If every finite subgraph of a graph
G has a homomorphism to a finite graph
F, then there is
a homomorphism from the whole of