symmetry' — Mathlib

English

The braiding isomorphism for a binary coproduct is symmetric: coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = id_{P ⨿ Q}.

Русский

Симметрия браидинга двойственного копродукта: coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙_(P ⨿ Q).

LaTeX

$$$ \\operatorname{coprod.desc} \\operatorname{coprod.inr} \\operatorname{coprod.inl} \\circ \\operatorname{coprod.desc} \\operatorname{coprod.inr} \\operatorname{coprod.inl} = \\mathrm{Id}_{P \\sqcup Q}$$$

Lean4

@[reassoc]
theorem symmetry' (P Q : C) : coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q) :=
  (coprod.braiding _ _).hom_inv_id

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