leftAdjointMate_id — Mathlib

English

Similarly, the left adjoint mate of identity is the identity on the left dual: ᘁ(id X) = id (ᘁX).

Русский

Аналогично, левая сопряженная композиция единичного отображения равна единице на левой двойнике: ᘁ(id X) = id (ᘁX).

LaTeX

$$$$ (\\!ᘁ\\!)(\\mathrm{id}_X) = \\mathrm{id}_{X^{\\ast\\!}} $$$$

Lean4

@[simp]
theorem leftAdjointMate_id {X : C} [HasLeftDual X] : (ᘁ(𝟙 X)) = 𝟙 (ᘁX) := by simp [leftAdjointMate]

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