# Documentation

Mathlib.Combinatorics.SimpleGraph.Finsubgraph

# 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 : ) :

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

Instances For
@[inline, reducible]
abbrev SimpleGraph.FinsubgraphHom {V : Type u} {W : Type v} {G : } (G' : ) (F : ) :
Type (max u v)

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

Instances For
instance SimpleGraph.instSupFinsubgraph {V : Type u} {G : } :
instance SimpleGraph.instInfFinsubgraph {V : Type u} {G : } :
instance SimpleGraph.instTopFinsubgraph {V : Type u} {G : } [] :
instance SimpleGraph.instSupSetFinsubgraph {V : Type u} {G : } [] :
instance SimpleGraph.instInfSetFinsubgraph {V : Type u} {G : } [] :
def SimpleGraph.singletonFinsubgraph {V : Type u} {G : } (v : V) :

The finite subgraph of G generated by a single vertex.

Instances For
def SimpleGraph.finsubgraphOfAdj {V : Type u} {G : } {u : V} {v : V} (e : ) :

The finite subgraph of G generated by a single edge.

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

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

Instances For
def SimpleGraph.finsubgraphHomFunctor {V : Type u} {W : Type v} (G : ) (F : ) :

The inverse system of finite homomorphisms.

Instances For
theorem SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom {V : Type u} {W : Type v} {G : } {F : } [] (h : (G' : ) → Set.Finite G'.verts) :

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.