conjugateEquiv_id — Mathlib

English

The conjugation correspondence sends the identity morphism to the identity: conjugateEquiv adj1 adj1 (id_l1) = id_r1.

Русский

Сопряжение переводит тождественный морфизм в тождественный: conjugateEquiv adj1 adj1 (id_{l1}) = id_{r1}.

LaTeX

$$$$ \\text{conjugateEquiv } adj_1\\ adj_1(\\mathrm{id}_{l_1}) = \\mathrm{id}_{r_1}. $$$$

Lean4

@[simp]
theorem conjugateEquiv_id : conjugateEquiv adj₁ adj₁ (𝟙 _) = 𝟙 _ :=
  by
  rw [conjugateEquiv_apply, mateEquiv_apply']
  calc
    _ = 𝟙 _ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 _ := by bicategory
    _ = 𝟙 r₁ := by
      rw [adj₁.right_triangle]
      bicategory

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