reflectsIsomorphisms_of_comp — Mathlib

English

IsIso f is equivalent to IsIso (F.map f) when F reflects isomorphisms.

Русский

IsIso f эквивалентно IsIso (F.map f), если F отражает изоморфизмы.

LaTeX

$$$IsIso (F.map f) \\iff IsIso f \\text{ under } F.ReflectsIsomorphisms.$$$

Lean4

theorem reflectsIsomorphisms_of_comp (F : C ⥤ D) (G : D ⥤ E) [(F ⋙ G).ReflectsIsomorphisms] : F.ReflectsIsomorphisms
    where
  reflects f
    _ := by
    rw [← isIso_iff_of_reflects_iso _ (F ⋙ G)]
    dsimp
    infer_instance

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