braiding_hom_fst — Mathlib

English

For bilimits P,Q with braiding, the hom component of braiding composed with t.fst equals s.snd.

Русский

Для билилимитов P,Q с браидингом композиция гомоморфизма браидинга с t.fst равна s.snd.

LaTeX

$$$$ (braiding\\ P\\ Q)_{\\mathrm{hom}} \\circ t.fst = s.snd. $$$$

Lean4

@[reassoc (attr := simp)]
theorem braiding_hom_fst : (braiding P Q).hom ≫ t.fst = s.snd :=
  P.conePointUniqueUpToIso_hom_comp _ ⟨.right⟩

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