Documentation

Mathlib.Combinatorics.SimpleGraph.Finsubgraph

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.

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

    Equations
    Instances For
      Equations
      • SimpleGraph.instOrderBotFinsubgraphLeSubgraphToLEToPreorderToPartialOrderToCompleteSemilatticeInfToCompleteLatticeInstCompletelyDistribLatticeSubgraphFiniteVerts = OrderBot.mk
      Equations
      • SimpleGraph.instSupFinsubgraph = { sup := fun (G₁ G₂ : SimpleGraph.Finsubgraph G) => { val := G₁ G₂, property := } }
      Equations
      • SimpleGraph.instInfFinsubgraph = { inf := fun (G₁ G₂ : SimpleGraph.Finsubgraph G) => { val := G₁ G₂, property := } }
      Equations
      Equations
      • SimpleGraph.instTopFinsubgraph = { top := { val := , property := } }
      Equations
      • SimpleGraph.instSupSetFinsubgraph = { sSup := fun (s : Set (SimpleGraph.Finsubgraph G)) => { val := ⨆ G_1 ∈ s, G_1, property := } }
      Equations
      • SimpleGraph.instInfSetFinsubgraph = { sInf := fun (s : Set (SimpleGraph.Finsubgraph G)) => { val := ⨅ G_1 ∈ s, G_1, property := } }
      Equations

      The finite subgraph of G generated by a single vertex.

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

        The finite subgraph of G generated by a single edge.

        Equations
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The inverse system of finite homomorphisms.

            Equations
            • One or more equations did not get rendered due to their size.
            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.