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) graphG
has a homomorphism to some finite graphF
, then there is also a homomorphismG →g F
.
Notations #
→fg
is a module-local variant on →g
where the domain is a finite subgraph of some supergraph
G
.
Implementation notes #
The proof here uses compactness as formulated in nonempty_sections_of_finite_inverse_system
. For
finite subgraphs G'' ≤ G'
, the inverse system finsubgraphHomFunctor
restricts homomorphisms
G' →fg F
to domain G''
.
The subtype of G.subgraph
comprising those subgraphs with finite vertex sets.
Instances For
A graph homomorphism from a finite subgraph of G to F.
Instances For
The finite subgraph of G generated by a single vertex.
Instances For
The finite subgraph of G generated by a single edge.
Instances For
Given a homomorphism from a subgraph to F
, construct its restriction to a sub-subgraph.
Instances For
The inverse system of finite homomorphisms.
Instances For
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 G
to F
.