whiskerLeft_mem

Mathlib.CategoryTheory.Localization.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.whiskerLeft_mem

English

In a monoidal setting, whiskering on the left preserves the W-property of morphisms.

Русский

В моноидальной обстановке слева взвешенное гложение сохраняет свойство W морфизмов.

LaTeX

$$$W g \Rightarrow W(X \triangleleft g)$$$

Lean4

theorem whiskerLeft_mem (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (X ◁ g) :=
  IsMonoidal.whiskerLeft _ _ hg

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

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

Разделы

Аффилиация

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