symmetrifyCostar — Mathlib

English

For every u, the star map of φ.symmetrify at u equals the conjugation of Sum.map by the symmetrification isomorphism.

Русский

Для каждого узла u отображение звезды φ.symmetrify в точке u равняется конъюгации отображения Sum.map через изоморфизм симметризации.

LaTeX

$$φ.symmetrify.star u = (Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ Quiver.symmetrifyStar (φ.obj u)$$

Lean4

protected theorem symmetrifyCostar (u : U) :
    φ.symmetrify.costar u =
      (Quiver.symmetrifyCostar _).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ Quiver.symmetrifyCostar u :=
  by
  rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyCostar (φ.obj u))]
  ext ⟨v, f | g⟩ <;>
        -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyCostar]`
        simp only [Quiver.symmetrifyCostar, Function.comp_apply] <;>
      erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
    simp

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