forget_reflects_isos — Mathlib

English

The forgetful functor forgets enough structure to detect isomorphisms: if a morphism in AlgCat becomes an isomorphism after forgetting, then it was already an isomorphism in AlgCat.

Русский

Забывающий функтор детектирует изоморфизмы: если отображение в AlgCat становится изоморфизмом после забывания, то изоморфизм уже существовал в AlgCat.

LaTeX

$$$(\\text{forget} (\\mathrm{AlgCat} R)).\\text{ReflectsIsomorphisms}$$$

Lean4

instance forget_reflects_isos : (forget (AlgCat.{u} R)).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget (AlgCat.{u} R)).map f)
    let e : X ≃ₐ[R] Y := { f.hom, i.toEquiv with }
    exact e.toAlgebraIso.isIso_hom

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