map_hom_ofInv_id — Mathlib

English

The other half of the inverse relation also yields the identity: L.map s ≫ (ofInv s hs).map L hL = id.

Русский

Обратная связь даёт тождество: L.map s ≫ (ofInv s hs).map L hL = id.

LaTeX

$$L.map s \circ (\mathrm{ofInv}(s,hs).map L hL) = \mathrm{id}$$

Lean4

@[reassoc (attr := simp)]
theorem map_hom_ofInv_id (s : Y ⟶ X) (hs : W s) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    L.map s ≫ (ofInv s hs).map L hL = 𝟙 _ := by
  letI := hL _ hs
  simp [map]

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