English
The star of the symmetrification at a vertex u is equivalent to the sum of the star and costar at u in the original quiver.
Русский
Звезда симметризации в вершине u эквивалентна сумме звезды и косстара в исходной квиверсе в вершине u.
LaTeX
$$\operatorname{Quiver.Star}(\operatorname{Symmetrify}.of.obj(u)) \simeq \operatorname{Quiver.Star}(u) \oplus \operatorname{Quiver.Costar}(u)$$
Lean4
/-- The star of the symmetrification of a quiver at a vertex `u` is equivalent to the sum of the
star and the costar at `u` in the original quiver. -/
def symmetrifyStar (u : U) : Quiver.Star (Symmetrify.of.obj u) ≃ Quiver.Star u ⊕ Quiver.Costar u :=
Equiv.sigmaSumDistrib _ _