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.

Equations

• SimpleGraph.Finsubgraph G = { G' : SimpleGraph.Subgraph G // Set.Finite G'.verts }

@[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.

Equations

• SimpleGraph.FinsubgraphHom G' F = (SimpleGraph.Subgraph.coe ↑G' →g F)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SimpleGraph.instSupFinsubgraph = { sup := fun (G₁ G₂ : SimpleGraph.Finsubgraph G) => { val := ↑G₁ ⊔ ↑G₂, property := (_ : Set.Finite ((↑G₁).verts ∪ (↑G₂).verts)) } }

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

Equations

• SimpleGraph.instInfFinsubgraph = { inf := fun (G₁ G₂ : SimpleGraph.Finsubgraph G) => { val := ↑G₁ ⊓ ↑G₂, property := (_ : Set.Finite (↑G₁ ⊓ ↑G₂).verts) } }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SimpleGraph.instTopFinsubgraph = { top := { val := ⊤, property := (_ : Set.Finite Set.univ) } }

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

Equations

• SimpleGraph.instSupSetFinsubgraph = { sSup := fun (s : Set (SimpleGraph.Finsubgraph G)) => { val := ⨆ G_1 ∈ s, ↑G_1, property := (_ : Set.Finite (⨆ G_1 ∈ s, ↑G_1).verts) } }

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

Equations

• SimpleGraph.instInfSetFinsubgraph = { sInf := fun (s : Set (SimpleGraph.Finsubgraph G)) => { val := ⨅ G_1 ∈ s, ↑G_1, property := (_ : Set.Finite (⨅ G_1 ∈ s, ↑G_1).verts) } }

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

Equations

• One or more equations did not get rendered due to their size.

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

The finite subgraph of G generated by a single vertex.

Equations

• SimpleGraph.singletonFinsubgraph v = { val := SimpleGraph.singletonSubgraph G v, property := (_ : Set.Finite {v}) }

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

The finite subgraph of G generated by a single edge.

Equations

• SimpleGraph.finsubgraphOfAdj e = { val := SimpleGraph.subgraphOfAdj G e, property := (_ : Set.Finite {u, v}) }

theorem SimpleGraph.singletonFinsubgraph_le_adj_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {e : G.Adj 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 : G.Adj 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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.