nonempty_hom_of_forall_finite_subgraph_hom

English

If every finite subgraph of G admits a homomorphism to a finite graph F, then there exists a homomorphism from G to F.

Русский

Если каждый конечный подграф графа G допускает гомоморфизм в конечный граф F, то существует гомоморфизм от G в F.

LaTeX

$$$$ \\forall G' : G.\\mathrm{Subgraph}, \\; G'.\\mathrm{verts}.\\mathrm{Finite} \\Rightarrow (G'.\\mathrm{coe} \\tofg F) $$ implies \\; \\exists \\phi: G \\tog F. $$$$

Lean4

/-- 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`. -/
theorem nonempty_hom_of_forall_finite_subgraph_hom [Finite W] (h : ∀ G' : G.Subgraph, G'.verts.Finite → G'.coe →g F) :
    Nonempty (G →g F) := by
  -- Obtain a `Fintype` instance for `W`.

  cases nonempty_fintype W
  haveI : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' =>
    ⟨h G'.unop G'.unop.property⟩
  haveI : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') :=
    by
    intro G'
    haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
    haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype
    exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
  obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
  refine ⟨⟨fun v => ?_, ?_⟩⟩
  · -- Map each vertex using the homomorphism provided for its singleton subgraph.
    exact
      (u (Opposite.op (singletonFinsubgraph v))).toFun
        ⟨v, by
          unfold singletonFinsubgraph
          simp⟩
  · -- Prove that the above mapping preserves adjacency.

    intro v v' e
    simp only
      /- The homomorphism for each edge's singleton subgraph agrees with those for its source and
              target vertices. -/

    have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
    have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
    rw [← hu hv, ← hu hv']
      -- Porting note: was `apply Hom.map_adj`

    apply
      Hom.map_adj (u _)
        ?_
          -- `v` and `v'` are definitionally adjacent in `finsubgraphOfAdj e`

    simp [finsubgraphOfAdj]

Похожие утверждения