# mathlib3documentation

combinatorics.simple_graph.finsubgraph

# Homomorphisms from finite subgraphs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the type of finite subgraphs of a simple_graph and proves a compactness result for homomorphisms to a finite codomain.

## Main statements #

• simple_graph.exists_hom_of_all_finite_homs: 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 finsubgraph_hom_functor restricts homomorphisms G' →fg F to domain G''.

@[reducible]
def simple_graph.finsubgraph {V : Type u} (G : simple_graph V) :

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

@[reducible]
def simple_graph.finsubgraph_hom {V : Type u} {W : Type v} {G : simple_graph V} (G' : G.finsubgraph) (F : simple_graph W) :
Type (max u v)

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
• simple_graph.finsubgraph.complete_distrib_lattice = simple_graph.finsubgraph.complete_distrib_lattice._proof_1 simple_graph.finsubgraph.complete_distrib_lattice._proof_2 simple_graph.finsubgraph.complete_distrib_lattice._proof_3 simple_graph.finsubgraph.complete_distrib_lattice._proof_4 simple_graph.finsubgraph.complete_distrib_lattice._proof_5 simple_graph.finsubgraph.complete_distrib_lattice._proof_6 simple_graph.finsubgraph.complete_distrib_lattice._proof_7
def simple_graph.singleton_finsubgraph {V : Type u} {G : simple_graph V} (v : V) :

The finite subgraph of G generated by a single vertex.

Equations
def simple_graph.finsubgraph_of_adj {V : Type u} {G : simple_graph V} {u v : V} (e : G.adj u v) :

The finite subgraph of G generated by a single edge.

Equations
theorem simple_graph.singleton_finsubgraph_le_adj_left {V : Type u} {G : simple_graph V} {u v : V} {e : G.adj u v} :
theorem simple_graph.singleton_finsubgraph_le_adj_right {V : Type u} {G : simple_graph V} {u v : V} {e : G.adj u v} :
def simple_graph.finsubgraph_hom.restrict {V : Type u} {W : Type v} {G : simple_graph V} {F : simple_graph W} {G' G'' : G.finsubgraph} (h : G'' G') (f : F) :

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

Equations
def simple_graph.finsubgraph_hom_functor {V : Type u} {W : Type v} (G : simple_graph V) (F : simple_graph W) :
(G.finsubgraph)ᵒᵖ Type (max u v)

The inverse system of finite homomorphisms.

Equations
theorem simple_graph.nonempty_hom_of_forall_finite_subgraph_hom {V : Type u} {W : Type v} {G : simple_graph V} {F : simple_graph W} [finite W] (h : Π (G' : G.subgraph), G'.verts.finite G'.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.