forget_reflects_iso — Mathlib

English

The forgetful functor forget X reflects isomorphisms: if forget X sends a morphism to an isomorphism, then the morphism was already an isomorphism.

Русский

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

LaTeX

$$$\\operatorname{IsIso}(f) \\Rightarrow \\operatorname{IsIso}(\\mathrm{forget}(f))$$$

Lean4

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

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