instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso

English

If W is a morphism property on T and L: A ⥤ T, R: B ⥤ T, then the comma object W.commaObj L R is closed under isomorphisms.

Русский

Если W — свойство морфизмов на T, то комма-объект W.commaObj L R по отношению к L и R замкнут относительно изоморфизмов.

LaTeX

$$$\\text{IsClosedUnderIsomorphisms}(W.commaObj L R)$$$

Lean4

instance [W.RespectsIso] : (W.commaObj L R).IsClosedUnderIsomorphisms where
  of_iso {X Y} e
    h := by
    rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w, W.cancel_right_of_respectsIso]

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