instReflectsIsomorphismsForget — Mathlib

English

The forgetful functor reflects isomorphisms: if the image of a morphism is an isomorphism in the base category, then the morphism is an isomorphism in the comonoid category.

Русский

Функтор забывания отражает изоморфизмы: если образ морфизма является изоморфизмом в базовой категории, то сам морфизм — изоморфизм в категории комоноидов.

LaTeX

$$$\text{forget}(C)\;\text{reflects isomorphisms}$$$

Lean4

/-- The forgetful functor from comonoid objects to the ambient category reflects isomorphisms. -/
instance : (forget C).ReflectsIsomorphisms where reflects f e := ⟨⟨{ hom := inv f.hom }, by cat_disch⟩⟩

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