Grp (Type u) ≌ GrpCat.{u}

The category of internal group objects in Type is equivalent to the category of "native" bundled groups.

Moreover, this equivalence is compatible with the forgetful functors to Type.

@[implicit_reducible]

instance GrpTypeEquivalenceGrp.grpGroup (A : Type u) [CategoryTheory.GrpObj A] : Group A

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GrpTypeEquivalenceGrp.functor : CategoryTheory.Functor (CategoryTheory.Grp (Type u)) GrpCat

Converting a group object in Type u into a group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GrpTypeEquivalenceGrp.inverse : CategoryTheory.Functor GrpCat (CategoryTheory.Grp (Type u))

Converting a group into a group object in Type u.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def grpTypeEquivalenceGrp : CategoryTheory.Grp (Type u) ≌ GrpCat

The category of group objects in Type u is equivalent to the category of groups.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def grpTypeEquivalenceGrpForget : GrpTypeEquivalenceGrp.functor.comp (CategoryTheory.forget₂ GrpCat MonCat) ≅ (CategoryTheory.Grp.forget₂Mon (Type u)).comp MonTypeEquivalenceMon.functor

The equivalences Mon (Type u) ≌ MonCat.{u} and Grp (Type u) ≌ GrpCat.{u} are naturally compatible with the forgetful functors to MonCat and Mon (Type u).

Equations

• grpTypeEquivalenceGrpForget = CategoryTheory.Iso.refl (GrpTypeEquivalenceGrp.functor.comp (CategoryTheory.forget₂ GrpCat MonCat))