# 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 G has a homomorphism to some finite graph F, then there is also a homomorphism G →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''.

@[reducible, inline]
abbrev SimpleGraph.Finsubgraph {V : Type u} (G : ) :

The subtype of G.subgraph comprising those subgraphs with finite vertex sets.

Equations
• G.Finsubgraph = { G' : G.Subgraph // G'.verts.Finite }
Instances For
@[reducible, inline]
abbrev SimpleGraph.FinsubgraphHom {V : Type u} {W : Type v} {G : } (G' : G.Finsubgraph) (F : ) :
Type (max u v)

A graph homomorphism from a finite subgraph of G to F.

Equations
Instances For
instance SimpleGraph.instOrderBotFinsubgraph {V : Type u} {G : } :
OrderBot G.Finsubgraph
Equations
• SimpleGraph.instOrderBotFinsubgraph =
instance SimpleGraph.instSupFinsubgraph {V : Type u} {G : } :
Sup G.Finsubgraph
Equations
• SimpleGraph.instSupFinsubgraph = { sup := fun (G₁ G₂ : G.Finsubgraph) => G₁ G₂, }
instance SimpleGraph.instInfFinsubgraph {V : Type u} {G : } :
Inf G.Finsubgraph
Equations
• SimpleGraph.instInfFinsubgraph = { inf := fun (G₁ G₂ : G.Finsubgraph) => G₁ G₂, }
instance SimpleGraph.instDistribLatticeFinsubgraph {V : Type u} {G : } :
DistribLattice G.Finsubgraph
Equations
instance SimpleGraph.instTopFinsubgraphOfFinite {V : Type u} {G : } [] :
Top G.Finsubgraph
Equations
• SimpleGraph.instTopFinsubgraphOfFinite = { top := , }
instance SimpleGraph.instSupSetFinsubgraphOfFinite {V : Type u} {G : } [] :
SupSet G.Finsubgraph
Equations
• SimpleGraph.instSupSetFinsubgraphOfFinite = { sSup := fun (s : Set G.Finsubgraph) => G_1s, G_1, }
instance SimpleGraph.instInfSetFinsubgraphOfFinite {V : Type u} {G : } [] :
InfSet G.Finsubgraph
Equations
• SimpleGraph.instInfSetFinsubgraphOfFinite = { sInf := fun (s : Set G.Finsubgraph) => G_1s, G_1, }
Equations
def SimpleGraph.singletonFinsubgraph {V : Type u} {G : } (v : V) :
G.Finsubgraph

The finite subgraph of G generated by a single vertex.

Equations
• = G.singletonSubgraph v,
Instances For
def SimpleGraph.finsubgraphOfAdj {V : Type u} {G : } {u : V} {v : V} (e : G.Adj u v) :
G.Finsubgraph

The finite subgraph of G generated by a single edge.

Equations
Instances For
theorem SimpleGraph.singletonFinsubgraph_le_adj_left {V : Type u} {G : } {u : V} {v : V} {e : G.Adj u v} :
theorem SimpleGraph.singletonFinsubgraph_le_adj_right {V : Type u} {G : } {u : V} {v : V} {e : G.Adj u v} :
def SimpleGraph.FinsubgraphHom.restrict {V : Type u} {W : Type v} {G : } {F : } {G' : G.Finsubgraph} {G'' : G.Finsubgraph} (h : G'' G') (f : ) :

Given a homomorphism from a subgraph to F, construct its restriction to a sub-subgraph.

Equations
• = { toFun := fun (x : (G'').verts) => match x with | v, hv => f.toFun v, , map_rel' := }
Instances For
def SimpleGraph.finsubgraphHomFunctor {V : Type u} {W : Type v} (G : ) (F : ) :
CategoryTheory.Functor G.Finsubgraphᵒᵖ (Type (max u v))

The inverse system of finite homomorphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom {V : Type u} {W : Type v} {G : } {F : } [] (h : (G' : G.Subgraph) → G'.verts.FiniteG'.coe →g F) :

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.