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

@[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 }
Instances For
    @[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
    Instances For
      instance SimpleGraph.Finsubgraph.instOrderBot {V : Type u} {G : SimpleGraph V} :
      OrderBot G.Finsubgraph
      Equations
      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]
      @[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₂
      Equations
      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_1s, 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_1s, G_1, }
      @[simp]
      @[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_1s, G_1
      @[simp]
      theorem SimpleGraph.Finsubgraph.coe_sInf {V : Type u} {G : SimpleGraph V} [Finite V] (s : Set G.Finsubgraph) :
      (sInf s) = G_1s, 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)
      Equations
      def SimpleGraph.singletonFinsubgraph {V : Type u} {G : SimpleGraph V} (v : V) :
      G.Finsubgraph

      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) :
        G.Finsubgraph

        The finite subgraph of G generated by a single edge.

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

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

          Equations
          Instances For
            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.
            Instances For
              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.FiniteG'.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.