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 : SimpleGraph V) : Type u

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

Equations

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

@[reducible, inline]

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

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

Equations

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

instance SimpleGraph.instOrderBotFinsubgraph {V : Type u} {G : SimpleGraph V} : OrderBot G.Finsubgraph

Equations

• SimpleGraph.instOrderBotFinsubgraph = OrderBot.mk ⋯

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

Equations

• SimpleGraph.instSupFinsubgraph = { sup := fun (G₁ G₂ : G.Finsubgraph) => ⟨↑G₁ ⊔ ↑G₂, ⋯⟩ }

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

Equations

• SimpleGraph.instInfFinsubgraph = { inf := fun (G₁ G₂ : G.Finsubgraph) => ⟨↑G₁ ⊓ ↑G₂, ⋯⟩ }

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

Equations

• SimpleGraph.instDistribLatticeFinsubgraph = Function.Injective.distribLattice (fun (a : { G' : G.Subgraph // G'.verts.Finite }) => ↑a) ⋯ ⋯ ⋯

instance SimpleGraph.instTopFinsubgraphOfFinite {V : Type u} {G : SimpleGraph V} [Finite V] : Top G.Finsubgraph

Equations

• SimpleGraph.instTopFinsubgraphOfFinite = { top := ⟨⊤, ⋯⟩ }

instance SimpleGraph.instSupSetFinsubgraphOfFinite {V : Type u} {G : SimpleGraph V} [Finite V] : SupSet G.Finsubgraph

Equations

• SimpleGraph.instSupSetFinsubgraphOfFinite = { sSup := fun (s : Set G.Finsubgraph) => ⟨⨆ G_1 ∈ s, ↑G_1, ⋯⟩ }

instance SimpleGraph.instInfSetFinsubgraphOfFinite {V : Type u} {G : SimpleGraph V} [Finite V] : InfSet G.Finsubgraph

Equations

• SimpleGraph.instInfSetFinsubgraphOfFinite = { sInf := fun (s : Set G.Finsubgraph) => ⟨⨅ G_1 ∈ s, ↑G_1, ⋯⟩ }

instance SimpleGraph.instCompletelyDistribLatticeFinsubgraphOfFinite {V : Type u} {G : SimpleGraph V} [Finite V] : CompletelyDistribLattice G.Finsubgraph

Equations

• SimpleGraph.instCompletelyDistribLatticeFinsubgraphOfFinite = Function.Injective.completelyDistribLattice (fun (a : { G' : G.Subgraph // G'.verts.Finite }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

The finite subgraph of G generated by a single vertex.

Equations

• SimpleGraph.singletonFinsubgraph v = ⟨G.singletonSubgraph v, ⋯⟩

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

The finite subgraph of G generated by a single edge.

Equations

• SimpleGraph.finsubgraphOfAdj e = ⟨G.subgraphOfAdj e, ⋯⟩

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' : G.Finsubgraph} {G'' : G.Finsubgraph} (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

• SimpleGraph.FinsubgraphHom.restrict h f = { toFun := fun (x : ↑(↑G'').verts) => match x with | ⟨v, hv⟩ => f.toFun ⟨v, ⋯⟩, map_rel' := ⋯ }

def SimpleGraph.finsubgraphHomFunctor {V : Type u} {W : Type v} (G : SimpleGraph V) (F : SimpleGraph W) : 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.

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' : G.Subgraph) → G'.verts.Finite → G'.coe →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.