forget_reflects_iso — Mathlib

English

The forgetful functor forget X reflects isomorphisms.

Русский

Функтор забывания forget X отражает изоморфизмы.

LaTeX

$$forget X reflects isomorphisms$$

Lean4

instance forget_reflects_iso : (forget X).ReflectsIsomorphisms where
  reflects {Y Z} f
    t := by
    let g : Z ⟶ Y := Under.homMk (inv ((Under.forget X).map f)) ((IsIso.comp_inv_eq _).2 (Under.w f).symm)
    dsimp [forget] at t
    refine ⟨⟨g, ⟨?_, ?_⟩⟩⟩
    repeat (ext; simp [g])

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