CommGrp (Type u) ≌ CommGrpCat.{u}

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

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

@[implicit_reducible]

instance CommGrpTypeEquivalenceCommGrp.commGrpCommGroup (A : Type u) [CategoryTheory.GrpObj A] [CategoryTheory.IsCommMonObj A] : CommGroup A

Equations

• CommGrpTypeEquivalenceCommGrp.commGrpCommGroup A = { toGroup := GrpTypeEquivalenceGrp.grpGroup A, mul_comm := ⋯ }

noncomputable def CommGrpTypeEquivalenceCommGrp.functor : CategoryTheory.Functor (CategoryTheory.CommGrp (Type u)) CommGrpCat

Converting a commutative group object in Type u into a group.

Equations

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

noncomputable def CommGrpTypeEquivalenceCommGrp.inverse : CategoryTheory.Functor CommGrpCat (CategoryTheory.CommGrp (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.

@[simp]

theorem CommGrpTypeEquivalenceCommGrp.inverse_obj_X {A : CommGrpCat} : (inverse.obj A).X = ↑A

@[simp]

theorem CommGrpTypeEquivalenceCommGrp.inverse_obj_one {A : CommGrpCat} {x : (fun (X : Type u) => X) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type u))} : (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.one) x = 1

@[simp]

theorem CommGrpTypeEquivalenceCommGrp.inverse_obj_mul {A : CommGrpCat} {p : (fun (X : Type u) => X) (CategoryTheory.MonoidalCategoryStruct.tensorObj (inverse.obj A).X (inverse.obj A).X)} : (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.mul) p = p.1 * p.2

@[simp]

theorem CommGrpTypeEquivalenceCommGrp.inverse_obj_inv {A : CommGrpCat} {x : (fun (X : Type u) => X) (inverse.obj A).X} : (CategoryTheory.ConcreteCategory.hom CategoryTheory.GrpObj.inv) x = x⁻¹

noncomputable def commGrpTypeEquivalenceCommGrp : CategoryTheory.CommGrp (Type u) ≌ CommGrpCat

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

Equations

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

noncomputable def commGrpTypeEquivalenceCommGrpForgetGrp : CommGrpTypeEquivalenceCommGrp.functor.comp (CategoryTheory.forget₂ CommGrpCat GrpCat) ≅ (CategoryTheory.CommGrp.forget₂Grp (Type u)).comp GrpTypeEquivalenceGrp.functor

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).

Equations

• commGrpTypeEquivalenceCommGrpForgetGrp = CategoryTheory.Iso.refl (CommGrpTypeEquivalenceCommGrp.functor.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))

noncomputable def commGrpTypeEquivalenceCommGrpForgetCommMon : CommGrpTypeEquivalenceCommGrp.functor.comp (CategoryTheory.forget₂ CommGrpCat CommMonCat) ≅ (CategoryTheory.CommGrp.forget₂CommMon (Type u)).comp CommMonTypeEquivalenceCommMon.functor

The equivalences CommMon (Type u) ≌ CommMonCat.{u} and CommGrp (Type u) ≌ CommGrpCat.{u} are naturally compatible with the forgetful functors to GrpCat and Grp (Type u).

Equations

• commGrpTypeEquivalenceCommGrpForgetCommMon = CategoryTheory.Iso.refl (CommGrpTypeEquivalenceCommGrp.functor.comp (CategoryTheory.forget₂ CommGrpCat CommMonCat))