reflectsIsomorphisms_forget₂ — Mathlib

English

If forget C reflects isomorphisms, then forget₂ C D also reflects isomorphisms.

Русский

Если forget C отражает изоморфизмы, то forget₂ C D тоже отражает изоморфизмы.

LaTeX

$$$\\text{forget C}.\\text{ReflectsIsomorphisms} \\Rightarrow (\\text{forget₂ } C D).\\text{ReflectsIsomorphisms}$$$

Lean4

/-- A `forget₂ C D` forgetful functor between concrete categories `C` and `D`
where `forget C` reflects isomorphisms, itself reflects isomorphisms.
-/
theorem reflectsIsomorphisms_forget₂ [HasForget₂ C D] [(forget C).ReflectsIsomorphisms] :
    (forget₂ C D).ReflectsIsomorphisms :=
  {
    reflects := fun X Y f {i} =>
      by
      haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
      haveI : IsIso ((forget C).map f) := by
        have := @HasForget₂.forget_comp C D
        rwa [← this]
      apply isIso_of_reflects_iso f (forget C) }

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