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.

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

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

instance SimpleGraph.Finsubgraph.instMax {V : Type u} {G : SimpleGraph V} : Max G.Finsubgraph

instance SimpleGraph.Finsubgraph.instMin {V : Type u} {G : SimpleGraph V} : Min G.Finsubgraph

instance SimpleGraph.Finsubgraph.instSDiff {V : Type u} {G : SimpleGraph V} : SDiff G.Finsubgraph

@[simp]

theorem SimpleGraph.Finsubgraph.coe_bot {V : Type u} {G : SimpleGraph V} : ↑⊥ = ⊥

@[simp]

theorem SimpleGraph.Finsubgraph.coe_sup {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⊔ G₂) = ↑G₁ ⊔ ↑G₂

@[simp]

theorem SimpleGraph.Finsubgraph.coe_inf {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⊓ G₂) = ↑G₁ ⊓ ↑G₂

@[simp]

theorem SimpleGraph.Finsubgraph.coe_sdiff {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Finsubgraph) : ↑(G₁ \ G₂) = ↑G₁ \ ↑G₂

instance SimpleGraph.Finsubgraph.instGeneralizedCoheytingAlgebra {V : Type u} {G : SimpleGraph V} : GeneralizedCoheytingAlgebra G.Finsubgraph

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

instance SimpleGraph.Finsubgraph.instHasCompl {V : Type u} {G : SimpleGraph V} [Finite V] : HasCompl G.Finsubgraph

instance SimpleGraph.Finsubgraph.instHNot {V : Type u} {G : SimpleGraph V} [Finite V] : HNot G.Finsubgraph

instance SimpleGraph.Finsubgraph.instHImp {V : Type u} {G : SimpleGraph V} [Finite V] : HImp G.Finsubgraph

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

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

@[simp]

theorem SimpleGraph.Finsubgraph.coe_top {V : Type u} {G : SimpleGraph V} [Finite V] : ↑⊤ = ⊤

@[simp]

theorem SimpleGraph.Finsubgraph.coe_compl {V : Type u} {G : SimpleGraph V} [Finite V] (G' : G.Finsubgraph) : ↑G'ᶜ = (↑G')ᶜ

@[simp]

theorem SimpleGraph.Finsubgraph.coe_hnot {V : Type u} {G : SimpleGraph V} [Finite V] (G' : G.Finsubgraph) : ↑(￢G') = ￢↑G'

@[simp]

theorem SimpleGraph.Finsubgraph.coe_himp {V : Type u} {G : SimpleGraph V} [Finite V] (G₁ G₂ : G.Finsubgraph) : ↑(G₁ ⇨ G₂) = ↑G₁ ⇨ ↑G₂

@[simp]

theorem SimpleGraph.Finsubgraph.coe_sSup {V : Type u} {G : SimpleGraph V} [Finite V] (s : Set G.Finsubgraph) : ↑(sSup s) = ⨆ G_1 ∈ s, ↑G_1

@[simp]

theorem SimpleGraph.Finsubgraph.coe_sInf {V : Type u} {G : SimpleGraph V} [Finite V] (s : Set G.Finsubgraph) : ↑(sInf s) = ⨅ G_1 ∈ s, ↑G_1

@[simp]

theorem SimpleGraph.Finsubgraph.coe_iSup {V : Type u} {G : SimpleGraph V} [Finite V] {ι : Sort u_1} (f : ι → G.Finsubgraph) : ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

@[simp]

theorem SimpleGraph.Finsubgraph.coe_iInf {V : Type u} {G : SimpleGraph V} [Finite V] {ι : Sort u_1} (f : ι → G.Finsubgraph) : ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

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

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

The finite subgraph of G generated by a single vertex.

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

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} {e : G.Adj u v} : singletonFinsubgraph u ≤ finsubgraphOfAdj e

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

def SimpleGraph.FinsubgraphHom.restrict {V : Type u} {W : Type v} {G : SimpleGraph V} {F : SimpleGraph W} {G' G'' : G.Finsubgraph} (h : G'' ≤ G') (f : FinsubgraphHom G' F) : 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 G.Finsubgraphᵒᵖ (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' : 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.