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 #

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

@[inline, reducible]
abbrev SimpleGraph.Finsubgraph {V : Type u} (G : SimpleGraph V) :

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

Instances For
    @[inline, reducible]
    abbrev SimpleGraph.FinsubgraphHom {V : Type u} {W : Type v} {G : SimpleGraph V} (G' : SimpleGraph.Finsubgraph G) (F : SimpleGraph W) :
    Type (max u v)

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

    Instances For

      The finite subgraph of G generated by a single vertex.

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

        The finite subgraph of G generated by a single edge.

        Instances For

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

          Instances For

            The inverse system of finite homomorphisms.

            Instances For

              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.