whiskerLeft_iff

Mathlib.CategoryTheory.Monoidal.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.whiskerLeft_iff

English

Left whiskering with tensor unit is injective: 𝟙_C ◁ f = 𝟙_C ◁ g iff f = g.

Русский

Левый whisker по тензорной единице инъективен: 𝟙_C ◁ f = 𝟙_C ◁ g ⇔ f = g.

LaTeX

$$$ 𝟙_C \triangleleft f = 𝟙_C \triangleleft g \; \iff\; f = g. $$$

Lean4

theorem whiskerLeft_iff {X Y : C} (f g : X ⟶ Y) : 𝟙_ C ◁ f = 𝟙_ C ◁ g ↔ f = g := by simp

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

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

Разделы

Аффилиация

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