inv_hom_id — Mathlib

English

For P : Bimod R S, the inverse followed by the forward hom equals the identity on P.X, reflecting the coherence of the left unitor in the bimodule setting.

Русский

Для P : Bimod R S, обратный затем прямой морфизм hom равен тождественному отображению на 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 [one_actLeft, Iso.inv_hom_id]

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