forget₂_full — Mathlib

English

The forgetful functor from Semigrp to Type reflects isomorphisms: if forget f is an isomorphism, then f is an isomorphism in Semigrp.

Русский

Функтор забывания из Semigrp в Type отражает изоморфизмы: если forget f — изоморфизм, то f — изоморфизм в Semigrp.

LaTeX

$$$(\\text{forget Semigrp}).ReflectsIsomorphisms$$$

Lean4

/-- Ensure that `forget₂ CommMonCat MonCat` automatically reflects isomorphisms.
We could have used `CategoryTheory.HasForget.ReflectsIso` alternatively.
-/
@[to_additive]
instance forget₂_full : (forget₂ Semigrp MagmaCat).Full where map_surjective f := ⟨ofHom f.hom, rfl⟩

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