instReflectsIsomorphismsGrpCatForget₂

English

The composite forgetful functor from CommGrpCat to GrpCat to Type reflects isomorphisms: if the underlying map is an isomorphism, then the original morphism is an isomorphism in CommGrpCat.

Русский

Сложный забывающий функтор CommGrpCat ⥤ GrpCat ⥤ Type сохраняет отражение изоморфизмов: если отображение является изоморфизмом на уровне Type, то исходный морфизм в CommGrpCat также является изоморфизмом.

LaTeX

$$$ (\mathrm{forget} \;2) \; \text{ reflectsIsomorphisms } $$$

Lean4

@[to_additive]
instance : (forget₂ CommGrpCat.{u} GrpCat.{u}).ReflectsIsomorphisms :=
  reflectsIsomorphisms_forget₂ _ _

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