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''.

@[inline, reducible]

abbrev SimpleGraph.Finsubgraph {V : Type u} (G : SimpleGraph V) : Type u

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

@[inline, reducible]

abbrev SimpleGraph.FinsubgraphHom {V : Type u} {W : Type v} {G : SimpleGraph V} (G' : SimpleGraph.Finsubgraph G) (F : SimpleGraph W) : Type (max u v)

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

instance SimpleGraph.instOrderBotFinsubgraphLeSubgraphToLEToPreorderToPartialOrderToCompleteSemilatticeInfToCompleteLatticeInstCompletelyDistribLatticeSubgraphFiniteVerts {V : Type u} {G : SimpleGraph V} : OrderBot (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instSupFinsubgraph {V : Type u} {G : SimpleGraph V} : Sup (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instInfFinsubgraph {V : Type u} {G : SimpleGraph V} : Inf (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instDistribLatticeFinsubgraph {V : Type u} {G : SimpleGraph V} : DistribLattice (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instTopFinsubgraph {V : Type u} {G : SimpleGraph V} [Finite V] : Top (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instSupSetFinsubgraph {V : Type u} {G : SimpleGraph V} [Finite V] : SupSet (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instInfSetFinsubgraph {V : Type u} {G : SimpleGraph V} [Finite V] : InfSet (SimpleGraph.Finsubgraph G)

instance SimpleGraph.instCompletelyDistribLatticeFinsubgraph {V : Type u} {G : SimpleGraph V} [Finite V] : CompletelyDistribLattice (SimpleGraph.Finsubgraph G)

def SimpleGraph.singletonFinsubgraph {V : Type u} {G : SimpleGraph V} (v : V) : SimpleGraph.Finsubgraph G

The finite subgraph of G generated by a single vertex.

def SimpleGraph.finsubgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (e : SimpleGraph.Adj G u v) : SimpleGraph.Finsubgraph G

The finite subgraph of G generated by a single edge.

theorem SimpleGraph.singletonFinsubgraph_le_adj_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {e : SimpleGraph.Adj G u v} : SimpleGraph.singletonFinsubgraph u ≤ SimpleGraph.finsubgraphOfAdj e

theorem SimpleGraph.singletonFinsubgraph_le_adj_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {e : SimpleGraph.Adj G u v} : SimpleGraph.singletonFinsubgraph v ≤ SimpleGraph.finsubgraphOfAdj e

def SimpleGraph.FinsubgraphHom.restrict {V : Type u} {W : Type v} {G : SimpleGraph V} {F : SimpleGraph W} {G' : SimpleGraph.Finsubgraph G} {G'' : SimpleGraph.Finsubgraph G} (h : G'' ≤ G') (f : SimpleGraph.FinsubgraphHom G' F) : SimpleGraph.FinsubgraphHom G'' F

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

def SimpleGraph.finsubgraphHomFunctor {V : Type u} {W : Type v} (G : SimpleGraph V) (F : SimpleGraph W) : CategoryTheory.Functor (SimpleGraph.Finsubgraph G)ᵒᵖ (Type (max u v))

The inverse system of finite homomorphisms.

theorem SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom {V : Type u} {W : Type v} {G : SimpleGraph V} {F : SimpleGraph W} [Finite W] (h : (G' : SimpleGraph.Subgraph G) → Set.Finite G'.verts → SimpleGraph.Subgraph.coe G' →g F) : Nonempty (G →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.