imageSubobjectCompIso_inv_arrow — Mathlib

English

The inv-arrow compatibility: (imageSubobjectCompIso f h).inv ≫ (imageSubobject (f ≫ h)).arrow = (imageSubobject f).arrow ≫ inv h.

Русский

Совместимость обратной стрелки: (imageSubobjectCompIso f h).inv ≫ (imageSubobject (f ≫ h)).arrow = (imageSubobject f).arrow ≫ inv h.

LaTeX

$$$(\mathrm{imageSubobjectCompIso}(f,h).\mathrm{inv}}) \circ (\mathrm{imageSubobject}(f \circ h)).\mathrm{arrow} = (\mathrm{imageSubobject} f).\\mathrm{arrow} \circ (\mathrm{inv} \, h)$$$

Lean4

@[reassoc (attr := simp)]
theorem imageSubobjectCompIso_inv_arrow (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
    (imageSubobjectCompIso f h).inv ≫ (imageSubobject (f ≫ h)).arrow = (imageSubobject f).arrow ≫ h := by
  simp [imageSubobjectCompIso]

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