generators_connected — Mathlib

English

For a connected free groupoid, its generating quiver is rooted-connected with respect to any chosen root r; in particular, every vertex is reachable from the root by a path in the generating quiver.

Русский

Для связного свободного группоида порождающая квивера образует rooted-connected относительно любого выбранного корня r; каждую вершину можно достичь из корня по пути в порождающей квивере.

LaTeX

$$$$\operatorname{RootedConnected}(\mathrm{symgen}(r)).$$$$

Lean4

/-- Given a connected free groupoid, its generating quiver is rooted-connected. -/
instance generators_connected (G) [Groupoid.{u, u} G] [IsConnected G] [IsFreeGroupoid G] (r : G) :
    RootedConnected (symgen r) :=
  ⟨fun b => path_nonempty_of_hom (CategoryTheory.nonempty_hom_of_preconnected_groupoid r b)⟩

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