left_triangle

Mathlib.CategoryTheory.Adjunction.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.left_triangle

English

The unit and counit of an adjunction satisfy the left triangle identity.

Русский

Единица и кушин (counit) сопряжённости удовлетворяют левому треугольнику.

LaTeX

$$$\text{whiskerRight}\; \text{adj.unit} \; F \; \gg \text{whiskerLeft}\; \text{adj.counit} \\ = \\mathrm{Id}$$$

Lean4

@[simp]
theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _ := by ext; simp

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

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

Разделы

Аффилиация

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