symm_i — Mathlib

English

For a precylinder P on A, the symmetry morphism i of the cylinder is obtained by composing P.i with the braiding morphism on A ⊔ A, i.e., i = (coprod.braiding A A).hom ∘ i.

Русский

Для прециллиндра P над A симметрия цилиндра определяется композицией i с браидингом копродукта: i = (coprod.braiding A A).hom ∘ i.

LaTeX

$$$P.\text{symm}.i = (\operatorname{coprod.braiding} \\ A \\ A).\mathrm{hom} \circ P.i$$$

Lean4

@[simp, reassoc]
theorem symm_i [HasBinaryCoproducts C] : P.symm.i = (coprod.braiding A A).hom ≫ P.i := by cat_disch

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