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 GrpCat.groupObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) (j : J) : Group ((F.comp (CategoryTheory.forget GrpCat)).obj j)

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

We show that the forgetful functor GrpCat ⥤ 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 AddGrpCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddGrpCat AddMonCat)

We show that the forgetful functor AddGrpCat ⥤ 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 GrpCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] : CategoryTheory.Limits.Cone F

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

The category of groups has all limits.

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

The category of additive groups has all limits.

instance GrpCat.hasLimits : CategoryTheory.Limits.HasLimits GrpCat

instance AddGrpCat.hasLimits : CategoryTheory.Limits.HasLimits AddGrpCat

instance GrpCat.forget₂Mon_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ GrpCat 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 AddGrpCat.forget₂AddMonPreservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddGrpCat 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 GrpCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ GrpCat MonCat)

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

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

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

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

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

instance GrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget GrpCat)

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 AddGrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGrpCat)

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 GrpCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget GrpCat)

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

The forgetful functor from groups to types creates all limits.

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance CommGrpCat.instReflectsIsomorphismsGrpCatForget₂ : (CategoryTheory.forget₂ CommGrpCat GrpCat).ReflectsIsomorphisms

instance AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForget₂ : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).ReflectsIsomorphisms

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

We show that the forgetful functor CommGrpCat ⥤ GrpCat 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 AddCommGrpCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)

We show that the forgetful functor AddCommGrpCat ⥤ AddGrpCat 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 CommGrpCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] : CategoryTheory.Limits.Cone F

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

Equations

• CommGrpCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)))

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

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

Equations

• AddCommGrpCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)))

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

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

Equations

• CommGrpCat.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)))

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

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

Equations

• AddCommGrpCat.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)))

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

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

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

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

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

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

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

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

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

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

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

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

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

The category of commutative groups has all limits.

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

The category of additive commutative groups has all limits.

instance CommGrpCat.hasLimits : CategoryTheory.Limits.HasLimits CommGrpCat

instance AddCommGrpCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommGrpCat

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

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

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

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

instance CommGrpCat.forget₂Group_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrpCat GrpCat)

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 AddCommGrpCat.forget₂AddGroup_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)

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 CommGrpCat.forget₂Group_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommGrpCat GrpCat)

instance AddCommGrpCat.forget₂AddGroup_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)

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

An auxiliary declaration to speed up typechecking.

Equations

• CommGrpCat.forget₂CommMon_preservesLimitsAux F = CommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommGrpCat CommMonCat))

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

An auxiliary declaration to speed up typechecking.

Equations

• AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux F = AddCommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat))

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

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

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

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

instance CommGrpCat.forget₂CommMon_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrpCat 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 AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGrpCat 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 CommGrpCat.forget_preservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommGrpCat)

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

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

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

instance CommGrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGrpCat)

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 AddCommGrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGrpCat)

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 AddCommGrpCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommGrpCat)

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

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

Equations

• CommGrpCat.forget_createsLimit F = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp (CategoryTheory.forget GrpCat)))

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

Equations

• AddCommGrpCat.forget_createsLimit F = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp (CategoryTheory.forget AddGrpCat)))

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def AddCommGrpCat.kernelIsoKer {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Limits.kernel f ≅ of ↥(Hom.hom f).ker

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

Equations

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

@[simp]

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

@[simp]

theorem AddCommGrpCat.kernelIsoKer_inv_comp_ι {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = ofHom (Hom.hom f).ker.subtype

def AddCommGrpCat.kernelIsoKerOver {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Over.mk (CategoryTheory.Limits.kernel.ι f) ≅ CategoryTheory.Over.mk (ofHom (Hom.hom f).ker.subtype)

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

Equations

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