The category of (commutative) (additive) groups has all limits

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

instance Grp.groupObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) (j : J) : Group ((F.comp (CategoryTheory.forget Grp)).obj j)

Equations

• Grp.groupObj F j = inferInstanceAs (Group ↑(F.obj j))

instance AddGrp.addGroupObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) (j : J) : AddGroup ((F.comp (CategoryTheory.forget AddGrp)).obj j)

Equations

• AddGrp.addGroupObj F j = inferInstanceAs (AddGroup ↑(F.obj j))

def Grp.sectionsSubgroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) : Subgroup ((j : J) → ↑(F.obj j))

The flat sections of a functor into Grp form a subgroup of all sections.

Equations

• Grp.sectionsSubgroup F = { carrier := (F.comp (CategoryTheory.forget Grp)).sections, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddGrp.sectionsAddSubgroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) : AddSubgroup ((j : J) → ↑(F.obj j))

The flat sections of a functor into AddGrp form an additive subgroup of all sections.

Equations

• AddGrp.sectionsAddSubgroup F = { carrier := (F.comp (CategoryTheory.forget AddGrp)).sections, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

instance Grp.sectionsGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) : Group ↑(F.comp (CategoryTheory.forget Grp)).sections

Equations

• Grp.sectionsGroup F = (Grp.sectionsSubgroup F).toGroup

instance AddGrp.sectionsAddGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) : AddGroup ↑(F.comp (CategoryTheory.forget AddGrp)).sections

Equations

• AddGrp.sectionsAddGroup F = (AddGrp.sectionsAddSubgroup F).toAddGroup

def Grp.sectionsπMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) (j : J) : ↑(F.comp (CategoryTheory.forget Grp)).sections →* ↑(F.obj j)

The projection from Functor.sections to a factor as a MonoidHom.

Equations

• Grp.sectionsπMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget Grp)).sections) => ↑x j, map_one' := ⋯, map_mul' := ⋯ }

def AddGrp.sectionsπAddMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) (j : J) : ↑(F.comp (CategoryTheory.forget AddGrp)).sections →+ ↑(F.obj j)

The projection from Functor.sections to a factor as an AddMonoidHom.

Equations

• AddGrp.sectionsπAddMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j, map_zero' := ⋯, map_add' := ⋯ }

noncomputable instance Grp.limitGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : Group (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget Grp))).pt

Equations

• Grp.limitGroup F = inferInstanceAs (Group (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget Grp)).sections))

noncomputable instance AddGrp.limitAddGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : AddGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddGrp))).pt

Equations

• AddGrp.limitAddGroup F = inferInstanceAs (AddGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddGrp)).sections))

instance Grp.instSmallElemForallObjCompMonCatForget₂ForgetSections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ Grp MonCat)).comp (CategoryTheory.forget MonCat)).sections

Equations

• ⋯ = ⋯

instance AddGrp.instSmallElemForallObjCompMonCatForget₂ForgetSections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ AddGrp AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections

Equations

• ⋯ = ⋯

noncomputable instance Grp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ Grp MonCat)

We show that the forgetful functor Grp ⥤ MonCat creates limits.

All we need to do is notice that the limit point has a Group instance available, and then reuse the existing limit.

Equations

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

noncomputable instance AddGrp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddGrp AddMonCat)

We show that the forgetful functor AddGrp ⥤ AddMonCat creates limits.

All we need to do is notice that the limit point has an AddGroup instance available, and then reuse the existing limit.

Equations

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

noncomputable def Grp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into Grp. (Generally, you'll just want to use limit F.)

Equations

• Grp.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ Grp MonCat)))

noncomputable def AddGrp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into Grp. (Generally, you'll just want to use limit F.)

Equations

• AddGrp.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddGrp AddMonCat)))

noncomputable def Grp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : CategoryTheory.Limits.IsLimit (Grp.limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

• Grp.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ Grp MonCat)))

noncomputable def AddGrp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : CategoryTheory.Limits.IsLimit (AddGrp.limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

• AddGrp.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddGrp AddMonCat)))

instance Grp.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget Grp).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

instance AddGrp.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget AddGrp).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

theorem Grp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections

A functor F : J ⥤ Grp.{u} has a limit iff (F ⋙ forget Grp).sections is u-small.

theorem AddGrp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections

A functor F : J ⥤ AddGrp.{u} has a limit iff (F ⋙ forget AddGrp).sections is u-small.

instance Grp.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J Grp

If J is u-small, Grp.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance AddGrp.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J AddGrp

If J is u-small, AddGrp.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance Grp.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} Grp

The category of groups has all limits.

Equations

• ⋯ = ⋯

instance AddGrp.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddGrp

The category of additive groups has all limits.

Equations

• ⋯ = ⋯

instance Grp.hasLimits : CategoryTheory.Limits.HasLimits Grp

Equations

• Grp.hasLimits = ⋯

instance AddGrp.hasLimits : CategoryTheory.Limits.HasLimits AddGrp

Equations

• AddGrp.hasLimits = ⋯

noncomputable instance Grp.forget₂MonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ Grp MonCat)

The forgetful functor from groups to monoids preserves all limits.

This means the underlying monoid of a limit can be computed as a limit in the category of monoids.

Equations

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

noncomputable instance AddGrp.forget₂AddMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddGrp AddMonCat)

The forgetful functor from additive groups to additive monoids preserves all limits.

This means the underlying additive monoid of a limit can be computed as a limit in the category of additive monoids.

Equations

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

noncomputable instance Grp.forget₂MonPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ Grp MonCat)

Equations

• Grp.forget₂MonPreservesLimits = Grp.forget₂MonPreservesLimitsOfSize

noncomputable instance AddGrp.forget₂MonPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddGrp AddMonCat)

Equations

• AddGrp.forget₂MonPreservesLimits = AddGrp.forget₂AddMonPreservesLimitsOfSize

noncomputable instance Grp.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget Grp)

If J is u-small, the forgetful functor from Grp.{u} preserves limits of shape J.

Equations

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

noncomputable instance AddGrp.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddGrp)

If J is u-small, the forgetful functor from AddGrp.{u}

preserves limits of shape J.

Equations

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

noncomputable instance Grp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget Grp)

The forgetful functor from groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

Equations

• Grp.forgetPreservesLimitsOfSize = inferInstance

noncomputable instance AddGrp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGrp)

The forgetful functor from additive groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

Equations

• AddGrp.forgetPreservesLimitsOfSize = inferInstance

noncomputable instance Grp.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Grp)

Equations

• Grp.forgetPreservesLimits = Grp.forgetPreservesLimitsOfSize

noncomputable instance AddGrp.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddGrp)

Equations

• AddGrp.forgetPreservesLimits = AddGrp.forgetPreservesLimitsOfSize

instance CommGrp.commGroupObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) (j : J) : CommGroup ((F.comp (CategoryTheory.forget CommGrp)).obj j)

Equations

• CommGrp.commGroupObj F j = inferInstanceAs (CommGroup ↑(F.obj j))

instance AddCommGrp.addCommGroupObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) (j : J) : AddCommGroup ((F.comp (CategoryTheory.forget AddCommGrp)).obj j)

Equations

• AddCommGrp.addCommGroupObj F j = inferInstanceAs (AddCommGroup ↑(F.obj j))

noncomputable instance CommGrp.limitCommGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommGrp))).pt

Equations

• CommGrp.limitCommGroup F = inferInstanceAs (CommGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget CommGrp)).sections))

noncomputable instance AddCommGrp.limitAddCommGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommGrp))).pt

Equations

• AddCommGrp.limitAddCommGroup F = inferInstanceAs (AddCommGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections))

instance CommGrp.instReflectsIsomorphismsGrpForget₂ : (CategoryTheory.forget₂ CommGrp Grp).ReflectsIsomorphisms

Equations

• CommGrp.instReflectsIsomorphismsGrpForget₂ = ⋯

instance AddCommGrp.instReflectsIsomorphismsAddGrpForget₂ : (CategoryTheory.forget₂ AddCommGrp AddGrp).ReflectsIsomorphisms

Equations

• AddCommGrp.instReflectsIsomorphismsAddGrpForget₂ = ⋯

noncomputable instance CommGrp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommGrp Grp)

We show that the forgetful functor CommGrp ⥤ Grp creates limits.

All we need to do is notice that the limit point has a CommGroup instance available, and then reuse the existing limit.

Equations

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

noncomputable instance AddCommGrp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommGrp AddGrp)

We show that the forgetful functor AddCommGrp ⥤ AddGrp creates limits.

All we need to do is notice that the limit point has an AddCommGroup instance available, and then reuse the existing limit.

Equations

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

noncomputable def CommGrp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into CommGrp. (Generally, you'll just want to use limit F.)

Equations

• CommGrp.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrp Grp)))

noncomputable def AddCommGrp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into AddCommGrp. (Generally, you'll just want to use limit F.)

Equations

• AddCommGrp.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)))

noncomputable def CommGrp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.IsLimit (CommGrp.limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

• CommGrp.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrp Grp)))

noncomputable def AddCommGrp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.IsLimit (AddCommGrp.limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

• AddCommGrp.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)))

instance CommGrp.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget CommGrp).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

instance AddCommGrp.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget AddCommGrp).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

theorem CommGrp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections

A functor F : J ⥤ CommGrp.{u} has a limit iff (F ⋙ forget CommGrp).sections is u-small.

theorem AddCommGrp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections

A functor F : J ⥤ AddCommGrp.{u} has a limit iff (F ⋙ forget AddCommGrp).sections is u-small.

instance CommGrp.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J CommGrp

If J is u-small, CommGrp.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance AddCommGrp.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J AddCommGrp

If J is u-small, AddCommGrp.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance CommGrp.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommGrp

The category of commutative groups has all limits.

Equations

• ⋯ = ⋯

instance AddCommGrp.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddCommGrp

The category of additive commutative groups has all limits.

Equations

• ⋯ = ⋯

instance CommGrp.hasLimits : CategoryTheory.Limits.HasLimits CommGrp

Equations

• CommGrp.hasLimits = ⋯

instance AddCommGrp.hasLimits : CategoryTheory.Limits.HasLimits AddCommGrp

Equations

• AddCommGrp.hasLimits = ⋯

noncomputable instance CommGrp.forget₂GroupPreservesLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ CommGrp Grp)

Equations

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

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ AddCommGrp AddGrp)

Equations

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

noncomputable instance CommGrp.forget₂GroupPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ CommGrp Grp)

Equations

• CommGrp.forget₂GroupPreservesLimitsOfShape = { preservesLimit := fun {K : CategoryTheory.Functor J CommGrp} => inferInstance }

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ AddCommGrp AddGrp)

Equations

• AddCommGrp.forget₂AddGroupPreservesLimitsOfShape = { preservesLimit := fun {K : CategoryTheory.Functor J AddCommGrp} => inferInstance }

noncomputable instance CommGrp.forget₂GroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrp Grp)

The forgetful functor from commutative groups to groups preserves all limits. (That is, the underlying group could have been computed instead as limits in the category of groups.)

Equations

• CommGrp.forget₂GroupPreservesLimitsOfSize = { preservesLimitsOfShape := fun {J : Type ?u.10} [CategoryTheory.Category.{?u.8, ?u.10} J] => inferInstance }

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGrp AddGrp)

The forgetful functor from additive commutative groups to additive groups preserves all limits. (That is, the underlying group could have been computed instead as limits in the category of additive groups.)

Equations

• AddCommGrp.forget₂AddGroupPreservesLimitsOfSize = { preservesLimitsOfShape := fun {J : Type ?u.10} [CategoryTheory.Category.{?u.8, ?u.10} J] => inferInstance }

noncomputable instance CommGrp.forget₂GroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommGrp Grp)

Equations

• CommGrp.forget₂GroupPreservesLimits = CommGrp.forget₂GroupPreservesLimitsOfSize

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommGrp AddGrp)

Equations

• AddCommGrp.forget₂AddGroupPreservesLimits = AddCommGrp.forget₂AddGroupPreservesLimitsOfSize

noncomputable def CommGrp.forget₂CommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommGrp CommMonCat).mapCone (CommGrp.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• CommGrp.forget₂CommMonPreservesLimitsAux F = CommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommGrp CommMonCat))

noncomputable def AddCommGrp.forget₂AddCommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ AddCommGrp AddCommMonCat).mapCone (AddCommGrp.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• AddCommGrp.forget₂AddCommMonPreservesLimitsAux F = AddCommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddCommMonCat))

noncomputable instance CommGrp.forget₂CommMonPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ CommGrp CommMonCat)

If J is u-small, the forgetful functor from CommGrp.{u} to CommMonCat.{u} preserves limits of shape J.

Equations

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

noncomputable instance AddCommGrp.forget₂AddCommMonPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ AddCommGrp AddCommMonCat)

If J is u-small, the forgetful functor from AddCommGrp.{u} to AddCommMonCat.{u} preserves limits of shape J.

Equations

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

noncomputable instance CommGrp.forget₂CommMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrp CommMonCat)

The forgetful functor from commutative groups to commutative monoids preserves all limits. (That is, the underlying commutative monoids could have been computed instead as limits in the category of commutative monoids.)

Equations

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

noncomputable instance AddCommGrp.forget₂AddCommMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGrp AddCommMonCat)

The forgetful functor from additive commutative groups to additive commutative monoids preserves all limits. (That is, the underlying additive commutative monoids could have been computed instead as limits in the category of additive commutative monoids.)

Equations

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

noncomputable instance CommGrp.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommGrp)

If J is u-small, the forgetful functor from CommGrp.{u} preserves limits of shape J.

Equations

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

noncomputable instance AddCommGrp.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddCommGrp)

If J is u-small, the forgetful functor from AddCommGrp.{u}

preserves limits of shape J.

Equations

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

noncomputable instance CommGrp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGrp)

The forgetful functor from commutative groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

• CommGrp.forgetPreservesLimitsOfSize = inferInstance

noncomputable instance AddCommGrp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGrp)

The forgetful functor from additive commutative groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

• AddCommGrp.forgetPreservesLimitsOfSize = inferInstance

noncomputable instance AddCommGrp.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommGrp)

Equations

• AddCommGrp.forgetPreservesLimits = AddCommGrp.forgetPreservesLimitsOfSize

noncomputable instance CommGrp.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommGrp)

Equations

• CommGrp.forgetPreservesLimits = CommGrp.forgetPreservesLimitsOfSize

def AddCommGrp.kernelIsoKer {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Limits.kernel f ≅ AddCommGrp.of ↥(AddMonoidHom.ker f)

The categorical kernel of a morphism in AddCommGrp agrees with the usual group-theoretical kernel.

Equations

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

@[simp]

theorem AddCommGrp.kernelIsoKer_hom_comp_subtype {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGrp.kernelIsoKer f).hom (AddMonoidHom.ker f).subtype = CategoryTheory.Limits.kernel.ι f

@[simp]

theorem AddCommGrp.kernelIsoKer_inv_comp_ι {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGrp.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = (AddMonoidHom.ker f).subtype

def AddCommGrp.kernelIsoKerOver {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.Over.mk (CategoryTheory.Limits.kernel.ι f) ≅ CategoryTheory.Over.mk (AddMonoidHom.ker f).subtype

The categorical kernel inclusion for f : G ⟶ H, as an object over G, agrees with the AddSubgroup.subtype map.

Equations

• AddCommGrp.kernelIsoKerOver f = CategoryTheory.Over.isoMk (AddCommGrp.kernelIsoKer f) ⋯

@[simp]

theorem AddCommGrp.kernelIsoKerOver_inv_left_apply {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) : ∀ (a : ↑(CategoryTheory.Limits.KernelFork.ofι (AddMonoidHom.ker f).subtype ⋯).pt), (AddCommGrp.kernelIsoKerOver f).inv.left a = (CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair f 0) (CategoryTheory.Limits.KernelFork.ofι (AddMonoidHom.ker f).subtype ⋯)) a

@[simp]

theorem AddCommGrp.kernelIsoKerOver_hom_left_apply_coe {G : AddCommGrp} {H : AddCommGrp} (f : G ⟶ H) (g : ↑(CategoryTheory.Limits.kernel f)) : ↑((AddCommGrp.kernelIsoKerOver f).hom.left g) = (CategoryTheory.Limits.kernel.ι f) g