hom_inv_id — Mathlib

English

The inv morphism composes with hom to give the identity on mappingCone g; this confirms the inverse relation.

Русский

Инверсная композиция inv и hom даёт тождество на mappingCone g, что подтверждает обратную связь.

LaTeX

$$$\text{hom } f\, g \; \circ \; \text{inv } f\, g = \mathrm{id}_{\operatorname{mappingCone} g}$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_id : hom f g ≫ inv f g = 𝟙 _ := by
  ext n
  simp [hom, inv, lift_desc_f _ _ _ _ _ _ _ n (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

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