reflectsIsomorphisms_forget — Mathlib

English

The forgetful functor from CommAlgCat R to CommRingCat reflects isomorphisms: if a map becomes an isomorphism after forgetting, it was already an isomorphism in CommAlgCat.

Русский

Функтор забывания из CommAlgCat R в CommRingCat отражает изоморфизмы: если карта после забывания становится изоморфизмом, то она таковым была и в CommAlgCat.

LaTeX

$$$\mathrm{forget} : \mathrm{CommAlgCat} R \to \mathrm{CommRingCat} R$ reflects isomorphisms$$

Lean4

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

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