# Documentation

Mathlib.Algebra.Category.GroupCat.Limits

# 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 GroupCat.groupObj {J : Type v} (j : J) :
AddSubgroup ((j : J) → ↑(F.obj j))

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

Instances For
∀ {j j' : J} (f : j j'), J.map CategoryTheory.CategoryStruct.toQuiver (Type (max u_2 u_1)) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor j j' f (OfNat.ofNat ((j : J) → ↑()) 0 Zero.toOfNat0 j) = OfNat.ofNat ((j : J) → ↑()) 0 Zero.toOfNat0 j'
def GroupCat.sectionsSubgroup {J : Type v} (F : ) :
Subgroup ((j : J) → ↑(F.obj j))

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

Instances For
noncomputable instance GroupCat.limitGroup {J : Type v} :
theorem AddGroupCat.Forget₂.createsLimit.proof_3 {J : Type u_2} (s : ) :
{ val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) () (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) () (().mapCone (().mapCone s)).π j' 0) } = 0
noncomputable instance AddGroupCat.Forget₂.createsLimit {J : Type v} :

We show that the forgetful functor AddGroupCat ⥤ 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.

theorem AddGroupCat.Forget₂.createsLimit.proof_2 {J : Type u_1} (s : ) (v : (().mapCone (().mapCone s)).pt) :
∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) (().obj j) (().obj j') ((().mapCone (().mapCone s)).π.app j) (().map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) () (().mapCone (().mapCone s)).π j' v
theorem AddGroupCat.Forget₂.createsLimit.proof_4 {J : Type u_2} (s : ) (x : (().mapCone s).pt) (y : (().mapCone s).pt) :
ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) () (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) () (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) () (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } y
theorem AddGroupCat.Forget₂.createsLimit.proof_1 {J : Type u_1} ⦃X : J ⦃Y : J (f : X Y) :
CategoryTheory.CategoryStruct.comp ((().obj ().pt).map f) (().π.app Y) = CategoryTheory.CategoryStruct.comp (().π.app X) ()
theorem AddGroupCat.Forget₂.createsLimit.proof_5 {J : Type u_1} (t : ) (s : ) :
().map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : (().mapCone s).pt), ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } y) }) s) = ().map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : (().mapCone s).pt), ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone (().mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp () ()).obj j) ((CategoryTheory.Functor.comp () ()).obj j') ((().mapCone (().mapCone s)).π.app j) ((CategoryTheory.Functor.comp () ()).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone (().mapCone s)).pt) (CategoryTheory.Functor.comp () ()) (().mapCone (().mapCone s)).π j' 0) } = 0) } y) }) s)
noncomputable instance GroupCat.Forget₂.createsLimit {J : Type v} :

We show that the forgetful functor GroupCat ⥤ 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.

noncomputable def AddGroupCat.limitCone {J : Type v} :

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

Instances For
noncomputable def GroupCat.limitCone {J : Type v} :

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

Instances For
noncomputable def AddGroupCat.limitConeIsLimit {J : Type v} :

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

Instances For
noncomputable def GroupCat.limitConeIsLimit {J : Type v} :

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

Instances For

The category of additive groups has all limits.

The category of groups has all limits.

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.

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.

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.

noncomputable instance GroupCat.forgetPreservesLimitsOfSize :

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.

noncomputable instance GroupCat.forgetPreservesLimits :
instance CommGroupCat.commGroupObj {J : Type v} (j : J) :
noncomputable instance CommGroupCat.limitCommGroup {J : Type v} :
theorem AddCommGroupCat.Forget₂.createsLimit.proof_3 {J : Type u_1} (t : ) (s : ) :
().map ((fun s => (AddMonCat.HasLimits.limitConeIsLimit ()).1 (().mapCone s)) s) = ().map ((fun s => (AddMonCat.HasLimits.limitConeIsLimit ()).1 (().mapCone s)) s)
noncomputable instance AddCommGroupCat.Forget₂.createsLimit {J : Type v} :

We show that the forgetful functor AddCommGroupCat ⥤ AddGroupCat creates limits.

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

noncomputable instance CommGroupCat.Forget₂.createsLimit {J : Type v} :

We show that the forgetful functor CommGroupCat ⥤ GroupCat creates limits.

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

noncomputable def AddCommGroupCat.limitCone {J : Type v} :

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

Instances For
noncomputable def CommGroupCat.limitCone {J : Type v} :

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

Instances For
noncomputable def AddCommGroupCat.limitConeIsLimit {J : Type v} :

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

Instances For
noncomputable def CommGroupCat.limitConeIsLimit {J : Type v} :

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

Instances For

The category of additive commutative groups has all limits.

The category of commutative groups has all limits.

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

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

An auxiliary declaration to speed up typechecking.

Instances For

An auxiliary declaration to speed up typechecking.

Instances For

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

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

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

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

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

Instances For
@[simp]
↑(().hom.left g) =
@[simp]
∀ (a : ().pt), ().inv.left a = ↑(CategoryTheory.Limits.limit.lift () ()) a

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

Instances For