inv_hom_id — Mathlib

English

The inverse followed by the forward right unitor morphism equals the identity on P.X, expressing the inverse relationship in the right unitor.

Русский

Обратный затем прямой правого унитора равен тождественному отображению на P.X.

LaTeX

$$$$ \operatorname{inv}(P) \circ \operatorname{hom}(P) = \mathrm{id}_{P.X}. $$$$

Lean4

theorem inv_hom_id : inv P ≫ hom P = 𝟙 _ := by
  dsimp [hom, inv]
  slice_lhs 3 4 => rw [coequalizer.π_desc]
  rw [actRight_one, Iso.inv_hom_id]

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