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

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

noncomputable instance Grp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) : 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) : 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.

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.

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.

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.

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

The category of groups has all limits.

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

The category of additive groups has all limits.

instance Grp.hasLimits : CategoryTheory.Limits.HasLimits Grp

instance AddGrp.hasLimits : CategoryTheory.Limits.HasLimits AddGrp

instance Grp.forget₂Mon_preservesLimitsOfSize [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.

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.

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

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

instance Grp.forget_preservesLimitsOfShape {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.

instance AddGrp.forget_preservesLimitsOfShape {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.

instance Grp.forget_preservesLimitsOfSize : 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.

instance AddGrp.forget_preservesLimitsOfSize : 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.

instance Grp.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Grp)

instance AddGrp.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddGrp)

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

Equations

• Grp.forget_createsLimit F = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ Grp MonCat).comp (CategoryTheory.forget MonCat)))

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

Equations

• AddGrp.forget_createsLimit F = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ AddGrp AddMonCat).comp (CategoryTheory.forget AddMonCat)))

noncomputable instance Grp.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget Grp)

Equations

• Grp.forget_createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J Grp} => inferInstance }

noncomputable instance AddGrp.forget_createsLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddGrp)

Equations

• AddGrp.forget_createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J AddGrp} => inferInstance }

noncomputable instance Grp.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget Grp)

The forgetful functor from groups to types creates all limits.

Equations

• Grp.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }

noncomputable instance AddGrp.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGrp)

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

Equations

• AddGrp.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }

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

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

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.

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.

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.

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.

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

The category of commutative groups has all limits.

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

The category of additive commutative groups has all limits.

instance CommGrp.hasLimits : CategoryTheory.Limits.HasLimits CommGrp

instance AddCommGrp.hasLimits : CategoryTheory.Limits.HasLimits AddCommGrp

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

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

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

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

instance CommGrp.forget₂Group_preservesLimitsOfSize : 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.)

instance AddCommGrp.forget₂AddGroup_preservesLimitsOfSize : 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.)

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

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

noncomputable def CommGrp.forget₂CommMon_preservesLimitsAux {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₂CommMon_preservesLimitsAux F = CommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommGrp CommMonCat))

noncomputable def AddCommGrp.forget₂AddCommMon_preservesLimitsAux {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₂AddCommMon_preservesLimitsAux F = AddCommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddCommMonCat))

instance CommGrp.forget₂CommMon_preservesLimitsOfShape {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.

instance AddCommGrp.forget₂AddCommMon_preservesLimitsOfShape {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.

instance CommGrp.forget₂CommMon_preservesLimitsOfSize [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.)

instance AddCommGrp.forget₂AddCommMon_preservesLimitsOfSize [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.)

instance CommGrp.forget_preservesLimitsOfShape {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.

instance AddCommGrp.forget_preservesLimitsOfShape {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.

instance CommGrp.forget_preservesLimitsOfSize : 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.)

instance AddCommGrp.forget_preservesLimitsOfSize : 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.)

instance AddCommGrp.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommGrp)

instance CommGrp.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommGrp)

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

Equations

• CommGrp.forget_createsLimit F = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ CommGrp Grp).comp (CategoryTheory.forget Grp)))

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

Equations

• AddCommGrp.forget_createsLimit F = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget AddGrp)))

noncomputable instance CommGrp.forget_createsLimitsOfShape (J : Type v) [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget CommGrp)

Equations

• CommGrp.forget_createsLimitsOfShape J = { CreatesLimit := fun {K : CategoryTheory.Functor J CommGrp} => inferInstance }

noncomputable instance AddCommGrp.forget_createsLimitsOfShape (J : Type v) [CategoryTheory.Category.{w, v} J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddCommGrp)

Equations

• AddCommGrp.forget_createsLimitsOfShape J = { CreatesLimit := fun {K : CategoryTheory.Functor J AddCommGrp} => inferInstance }

noncomputable instance CommGrp.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGrp)

The forgetful functor from commutative groups to types creates all limits.

Equations

• CommGrp.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }

noncomputable instance AddCommGrp.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGrp)

The forgetful functor from additive commutative groups to types creates all limits.

Equations

• AddCommGrp.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }

def AddCommGrp.kernelIsoKer {G 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 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 H : AddCommGrp} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGrp.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = (AddMonoidHom.ker f).subtype

def AddCommGrp.kernelIsoKerOver {G 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) ⋯