mkIso' — Mathlib

English

In the category of commutative group objects, there exists an initial object (the trivial one).

Русский

В категории коммутативных групп существует начальный объект (тривиальный).

LaTeX

$$$\\text{HasInitial }(\\text{CommGrp}_C)$$$

Lean4

/-- Construct an isomorphism of commutative group objects by giving a monoid isomorphism between the
underlying objects. -/
@[simps!]
def mkIso' {G H : C} (e : G ≅ H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] :
    mk G ≅ mk H :=
  (fullyFaithfulForget₂Grp_ C).preimageIso (Grp_.mkIso' e)

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