symmetrifyStar — Mathlib

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 _ _

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