English
A wide subquiver of a quiver G is equivalently viewed as a total set of arrows; there is a bijection between WideSubquiver V and Set (Total V). The forward map sends a wide subquiver H to the set {e | e.hom ∈ H(e.left,e.right)} and the inverse sends a set S to {e | Total.mk a b e ∈ S}.
Русский
Расширенный подквир G эквивалентен совокупности всех стрелок; существует биекция между WideSubquiver V и Set(Total V). Прямое отображение отправляет подквир H в множество {e | e.hom ∈ H(e.left,e.right)}, а обратное отправляет множество S в {e | Total.mk a b e ∈ S}.
LaTeX
$$$ \\mathrm{wideSubquiverEquivSetTotal} : \\mathrm{WideSubquiver}(V) \\simeq \\mathrm{Set}(\\mathrm{Total}(V)) $$$
Lean4
/-- A wide subquiver of `G` can equivalently be viewed as a total set of arrows. -/
def wideSubquiverEquivSetTotal {V} [Quiver V] : WideSubquiver V ≃ Set (Total V)
where
toFun H := {e | e.hom ∈ H e.left e.right}
invFun S a b := {e | Total.mk a b e ∈ S}
