English
The inverse system finsubgraphHomFunctor assigns to every finite subgraph G' of G the type of homomorphisms G' → F, and to every inclusion between subgraphs a corresponding restriction map, forming a contravariant functor from the opposite of G.Finsubgraph to Type.
Русский
Обратная система finsubgraphHomFunctor ставит в соответствие каждому конечному подграфу G' графа G тип гомоморфизмов G' → F, а каждому вложению между подграфами — ограничение гомоморфизмов, образуя контравариантный функтор из противоположной категории G.Finsubgraph в Type.
LaTeX
$$$$ \\text{finsubgraphHomFunctor}(G,F): G.Finsubgraph^{op} \\to \\mathbf{Type}_{\\max(u,v)} $$ with \\; \\mathrm{obj}(G') = G'.\\mathrm{unop} \\tofg F, \\; \\mathrm{map}(g) = f.\\mathrm{restrict}(\\dots). $$$$
Lean4
/-- The inverse system of finite homomorphisms. -/
def finsubgraphHomFunctor (G : SimpleGraph V) (F : SimpleGraph W) : G.Finsubgraphᵒᵖ ⥤ Type max u v
where
obj G' := G'.unop →fg F
map g f := f.restrict (CategoryTheory.leOfHom g.unop)
