inv_comp_inv — Mathlib

English

The square of the unit morphism equals the identity: ι ∘ ι = id_A.

Русский

Двойное применение единичного морфизма дает тождественный морфизм: ι ∘ ι = id_A.

LaTeX

$$$\iota \circ \iota = \mathrm{id}_A$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_comp_inv (A : C) [GrpObj A] : ι ≫ ι = 𝟙 A :=
  by
  apply lift_left_mul_ext ι[A]
  rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]

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