instReflectsIsomorphismsFunctorObjWhiskeringRight

English

If F : D ⥤ E reflects isomorphisms, then the whiskering-right construction yields a functor that reflects isomorphisms.

Русский

Если F : D ⥤ E отражает изоморфизмы, то конструкция whiskerRight справа образует функтор, отражающий изоморфизмы.

LaTeX

$$$\\text{(whiskeringRight } C\, D\, E).\\mathrm{obj}\\ F \\;\\text{ ReflectsIsomorphisms}.$$$

Lean4

instance (F : D ⥤ E) [F.ReflectsIsomorphisms] : ((whiskeringRight C D E).obj F).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro Z
    rw [← isIso_iff_of_reflects_iso _ F]
    change IsIso ((((whiskeringRight C D E).obj F).map f).app Z)
    infer_instance

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