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 (max 0 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.Finsubgraph.instOrderBot {V : Type u} {G : SimpleGraph V} : OrderBot G.Finsubgraph

Equations

• SimpleGraph.Finsubgraph.instOrderBot = OrderBot.mk ⋯

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

Equations

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

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

Equations

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

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

Equations

• SimpleGraph.Finsubgraph.instSDiff = { sdiff := fun (G₁ G₂ : G.Finsubgraph) => ⟨↑G₁ \ ↑G₂, ⋯⟩ }

@[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.Finsubgraph) (G₂ : G.Finsubgraph) : ↑(G₁ ⊔ G₂) = ↑G₁ ⊔ ↑G₂

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

• SimpleGraph.Finsubgraph.instHasCompl = { compl := fun (G' : G.Finsubgraph) => ⟨(↑G')ᶜ, ⋯⟩ }

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

Equations

• SimpleGraph.Finsubgraph.instHNot = { hnot := fun (G' : G.Finsubgraph) => ⟨￢↑G', ⋯⟩ }

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

Equations

• SimpleGraph.Finsubgraph.instHImp = { himp := fun (G₁ G₂ : G.Finsubgraph) => ⟨↑G₁ ⇨ ↑G₂, ⋯⟩ }

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

Equations

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

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

Equations

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

@[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.Finsubgraph) (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

Equations

• SimpleGraph.Finsubgraph.instCompletelyDistribLattice = 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.