forget_reflects_isos — Mathlib

English

The forgetful functor from CoalgCat R to ModuleCat R reflects isomorphisms; hence a morphism in CoalgCat is an isomorphism whenever its image under forget is an isomorphism.

Русский

Забывающий функтор из CoalgCat R в ModuleCat R отражает изоморфизмы; следовательно, морфизм в CoalgCat является изоморфизмом тогда и только тогда, когда его образ под забыванием является изоморфизмом.

LaTeX

$$$$ \text{forget} (CoalgCat R) \text{ReflectsIsomorphisms}. $$$$

Lean4

instance forget_reflects_isos : (forget (CoalgCat.{v} R)).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget (CoalgCat.{v} R)).map f)
    let e : X ≃ₗc[R] Y := { f.toCoalgHom, i.toEquiv with }
    exact ⟨e.toCoalgIso.isIso_hom.1⟩

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