instSubsingleton

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Braided.instSubsingleton

English

There is at most one braiding on a functor F between braided categories; i.e., the braiding structure on F is unique.

Русский

У функторы F между braid-структурированными категориями существует не более одной braiding.

LaTeX

$$$$|\mathrm{Braided}(F)| \le 1.$$$$

Lean4

instance : Subsingleton F.Braided :=
  (Braided.toMonoidal_injective F).subsingleton

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru