symmetrifyCostar — Mathlib

English

The costar of the symmetrification at a vertex u is equivalent to the sum of the costar and the star at u in the original quiver.

Русский

Костар симметризованной версии в вершине u эквивалентен сумме костара и звезды в исходной квиверсе в вершине u.

LaTeX

$$\operatorname{Quiver.Costar}(\operatorname{Symmetrify}.of.obj(u)) \simeq \operatorname{Quiver.Costar}(u) \oplus \operatorname{Quiver.Star}(u)$$

Lean4

/-- The costar of the symmetrification of a quiver at a vertex `u` is equivalent to the sum of the
costar and the star at `u` in the original quiver. -/
def symmetrifyCostar (u : U) : Quiver.Costar (Symmetrify.of.obj u) ≃ Quiver.Costar u ⊕ Quiver.Star u :=
  Equiv.sigmaSumDistrib _ _

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