right_triangle

Mathlib.CategoryTheory.Adjunction.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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