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''.

source

@[reducible]

def simple_graph.finsubgraph {V : Type u} (G : simple_graph V) :

Type u

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

source

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

source

@[protected, instance]

def simple_graph.finsubgraph.order_bot {V : Type u} {G : simple_graph V} :

order_bot G.finsubgraph

Equations

simple_graph.finsubgraph.order_bot = {bot := ⟨⊥, _⟩, bot_le := _}

source

@[protected, instance]

def simple_graph.finsubgraph.has_sup {V : Type u} {G : simple_graph V} :

has_sup G.finsubgraph

Equations

simple_graph.finsubgraph.has_sup = {sup := λ (G₁ G₂ : G.finsubgraph), ⟨↑G₁ ⊔ ↑G₂, _⟩}

source

@[protected, instance]

def simple_graph.finsubgraph.has_inf {V : Type u} {G : simple_graph V} :

has_inf G.finsubgraph

Equations

simple_graph.finsubgraph.has_inf = {inf := λ (G₁ G₂ : G.finsubgraph), ⟨↑G₁ ⊓ ↑G₂, _⟩}

source

@[protected, instance]

def simple_graph.finsubgraph.distrib_lattice {V : Type u} {G : simple_graph V} :

distrib_lattice G.finsubgraph

Equations

simple_graph.finsubgraph.distrib_lattice = function.injective.distrib_lattice coe simple_graph.finsubgraph.distrib_lattice._proof_1 simple_graph.finsubgraph.distrib_lattice._proof_2 simple_graph.finsubgraph.distrib_lattice._proof_3

source

@[protected, instance]

def simple_graph.finsubgraph.has_top {V : Type u} {G : simple_graph V} [finite V] :

has_top G.finsubgraph

Equations

simple_graph.finsubgraph.has_top = {top := ⟨⊤, _⟩}

source

@[protected, instance]

def simple_graph.finsubgraph.has_Sup {V : Type u} {G : simple_graph V} [finite V] :

has_Sup G.finsubgraph

Equations

simple_graph.finsubgraph.has_Sup = {Sup := λ (s : set G.finsubgraph), ⟨⨆ (G_1 : G.finsubgraph) (H : G_1 ∈ s), ↑G_1, _⟩}

source

@[protected, instance]

def simple_graph.finsubgraph.has_Inf {V : Type u} {G : simple_graph V} [finite V] :

has_Inf G.finsubgraph

Equations

simple_graph.finsubgraph.has_Inf = {Inf := λ (s : set G.finsubgraph), ⟨⨅ (G_1 : G.finsubgraph) (H : G_1 ∈ s), ↑G_1, _⟩}

source

@[protected, instance]

def simple_graph.finsubgraph.complete_distrib_lattice {V : Type u} {G : simple_graph V} [finite V] :

complete_distrib_lattice G.finsubgraph

Equations

simple_graph.finsubgraph.complete_distrib_lattice = function.injective.complete_distrib_lattice coe 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

source

def simple_graph.singleton_finsubgraph {V : Type u} {G : simple_graph V} (v : V) :

G.finsubgraph

The finite subgraph of G generated by a single vertex.

Equations

simple_graph.singleton_finsubgraph v = ⟨G.singleton_subgraph v, _⟩

source

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

G.finsubgraph

The finite subgraph of G generated by a single edge.

Equations

simple_graph.finsubgraph_of_adj e = ⟨G.subgraph_of_adj e, _⟩

source

theorem simple_graph.singleton_finsubgraph_le_adj_left {V : Type u} {G : simple_graph V} {u v : V} {e : G.adj u v} :

simple_graph.singleton_finsubgraph u ≤ simple_graph.finsubgraph_of_adj e

source

theorem simple_graph.singleton_finsubgraph_le_adj_right {V : Type u} {G : simple_graph V} {u v : V} {e : G.adj u v} :

simple_graph.singleton_finsubgraph v ≤ simple_graph.finsubgraph_of_adj e

source

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 : simple_graph.finsubgraph_hom G' F) :

simple_graph.finsubgraph_hom G'' F

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

Equations

simple_graph.finsubgraph_hom.restrict h f = {to_fun := λ (_x : ↥(G''.val.verts)), simple_graph.finsubgraph_hom.restrict._match_1 h f _x, map_rel' := _}
simple_graph.finsubgraph_hom.restrict._match_1 h f ⟨v, hv⟩ = f.to_fun ⟨v, _⟩

source

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

G.finsubgraph_hom_functor F = {obj := λ (G' : (G.finsubgraph)ᵒᵖ), simple_graph.finsubgraph_hom (opposite.unop G') F, map := λ (G' G'' : (G.finsubgraph)ᵒᵖ) (g : G' ⟶ G'') (f : simple_graph.finsubgraph_hom (opposite.unop G') F), simple_graph.finsubgraph_hom.restrict _ f, map_id' := _, map_comp' := _}

source

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) :

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.