mathlib3 documentation

combinatorics.simple_graph.finsubgraph

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 #

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

@[reducible]
def simple_graph.finsubgraph {V : Type u} (G : simple_graph V) :

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

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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

The finite subgraph of G generated by a single vertex.

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

The finite subgraph of G generated by a single edge.

Equations

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

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

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.