commGrpTypeEquivalenceCommGrpForgetGrp

English

Compatibility of forgetful equivalences between commutative monoids and monoids with forgetful functors to GrpCat.

Русский

Совместимость эквивалентностей забывания между коммутативными моноидами и моноидами через забывающие функторы к GrpCat.

LaTeX

$$$ commMonTypeEquivalenceCommMonForgetGrp $$$

Lean4

/-- The equivalences `Grp_ (Type u) ≌ GrpCat.{u}` and `CommGrp_ (Type u) ≌ CommGrpCat.{u}`
are naturally compatible with the forgetful functors to `GrpCat` and `Grp_ (Type u)`.
-/
noncomputable def commGrpTypeEquivalenceCommGrpForgetGrp :
    CommGrpTypeEquivalenceCommGrp.functor ⋙ forget₂ CommGrpCat GrpCat ≅
      CommGrp_.forget₂Grp_ (Type u) ⋙ GrpTypeEquivalenceGrp.functor :=
  Iso.refl _

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