# The category of (commutative) (additive) monoids 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.

Type ((max u1 u2) + 1)

An alias for AddMonCat.{max u v}, to deal around unification issues.

Equations
Instances For
@[inline, reducible]
abbrev MonCatMax :
Type ((max u1 u2) + 1)

An alias for MonCat.{max u v}, to deal around unification issues.

Equations
Instances For
instance AddMonCat.addMonoidObj {J : Type v} (F : ) (j : J) :
Equations
instance MonCat.monoidObj {J : Type v} (F : ) (j : J) :
Equations
theorem AddMonCat.sectionsAddSubmonoid.proof_1 {J : Type u_3} [] (F : ) {a : (j : J) → (F.obj j)} {b : (j : J) → (F.obj j)} {j : J} {j' : J} (f : j j') :
f ((a + b) j) = (a + b) j'
AddSubmonoid ((j : J) → (F.obj j))

The flat sections of a functor into AddMonCat form an additive submonoid of all sections.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonCat.sectionsAddSubmonoid.proof_2 {J : Type u_2} [] (F : ) {j : J} {j' : J} (f : j j') :
(F.map f) 0 = 0
def MonCat.sectionsSubmonoid {J : Type v} (F : ) :
Submonoid ((j : J) → (F.obj j))

The flat sections of a functor into MonCat form a submonoid of all sections.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
instance MonCat.sectionsMonoid {J : Type v} (F : ) :
Equations
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance MonCat.limitMonoid {J : Type v} (F : ) :
Equations
noncomputable def AddMonCat.limitπAddMonoidHom {J : Type v} (F : ) (j : J) :

limit.π (F ⋙ forget AddMonCat) j as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonCat.limitπAddMonoidHom.proof_1 {J : Type u_3} [] (F : ) [] (j : J) :
= 0
theorem AddMonCat.limitπAddMonoidHom.proof_2 {J : Type u_3} [] (F : ) [] (j : J) :
∀ (x x_1 : ), { toFun := ().app j, map_zero' := }.toFun (x + x_1) = { toFun := ().app j, map_zero' := }.toFun x + { toFun := ().app j, map_zero' := }.toFun x_1
noncomputable def MonCat.limitπMonoidHom {J : Type v} (F : ) (j : J) :

limit.π (F ⋙ forget MonCat) j as a MonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def AddMonCat.HasLimits.limitCone {J : Type v} (F : ) :

(Internal use only; use the limits API.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonCat.HasLimits.limitCone.proof_1 {J : Type u_2} [] (F : ) [] :
∀ (x x_1 : J) (f : x x_1), CategoryTheory.CategoryStruct.comp ((.obj (AddMonCat.of ().pt)).map f) () =
noncomputable def MonCat.HasLimits.limitCone {J : Type v} (F : ) :

Construction of a limit cone in MonCat. (Internal use only; use the limits API.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_3 {J : Type u_3} [] (F : ) [] (s : ) (x : s.pt) (y : s.pt) :
{ toFun := fun (v : (.mapCone s).pt) => ().1 { val := fun (j : J) => (.mapCone s).app j v, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (v : (.mapCone s).pt) => (equivShrink ()).1 { val := fun (j : J) => (.mapCone s).app j v, property := }, map_zero' := }.toFun x + { toFun := fun (v : (.mapCone s).pt) => (equivShrink ()).1 { val := fun (j : J) => (.mapCone s).app j v, property := }, map_zero' := }.toFun y
noncomputable def AddMonCat.HasLimits.limitConeIsLimit {J : Type v} (F : ) :

(Internal use only; use the limits API.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_1 {J : Type u_2} [] (F : ) (s : ) (v : (.mapCone s).pt) :
∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp ((.mapCone s).app j) () v = (.mapCone s).app j' v
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_2 {J : Type u_3} [] (F : ) [] (s : ) :
{ val := fun (j : J) => (.mapCone s).app j 0, property := } = 0
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_4 {J : Type u_3} [] (F : ) [] (s : ) :
((fun (s : ) => { toZeroHom := { toFun := fun (v : (.mapCone s).pt) => (equivShrink ()).1 { val := fun (j : J) => (.mapCone s).app j v, property := }, map_zero' := }, map_add' := }) s) = ((fun (s : ) => { toZeroHom := { toFun := fun (v : (.mapCone s).pt) => (equivShrink ()).1 { val := fun (j : J) => (.mapCone s).app j v, property := }, map_zero' := }, map_add' := }) s)
noncomputable def MonCat.HasLimits.limitConeIsLimit {J : Type v} (F : ) :

Witness that the limit cone in MonCat is a limit cone. (Internal use only; use the limits API.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance AddMonCat.HasLimits.hasLimit {J : Type v} (F : ) :

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

Equations
• =
instance MonCat.HasLimits.hasLimit {J : Type v} (F : ) :

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

Equations
• =

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

Equations
• =

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

Equations
• =

The category of additive monoids has all limits.

Equations
• =

The category of monoids has all limits.

Equations
• =
Equations
Equations
noncomputable instance AddMonCat.forgetPreservesLimitsOfShape {J : Type v} [] :

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

preserves limits of shape J.

Equations
• One or more equations did not get rendered due to their size.
theorem AddMonCat.forgetPreservesLimitsOfShape.proof_1 {J : Type u_2} [] [] {F : } :
Small.{u_1, max u_1 u_2} { x : (j : J) → // }
noncomputable instance MonCat.forgetPreservesLimitsOfShape {J : Type v} [] :

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

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

The forgetful functor from additive monoids 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
• One or more equations did not get rendered due to their size.
noncomputable instance MonCat.forgetPreservesLimitsOfSize :

The forgetful functor from monoids 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
• One or more equations did not get rendered due to their size.
Equations
noncomputable instance MonCat.forgetPreservesLimits :
Equations
Type ((max u1 u2) + 1)

An alias for AddCommMonCat.{max u v}, to deal around unification issues.

Equations
Instances For
@[inline, reducible]
abbrev CommMonCatMax :
Type ((max u1 u2) + 1)

An alias for CommMonCat.{max u v}, to deal around unification issues.

Equations
Instances For
Equations
instance CommMonCat.commMonoidObj {J : Type v} (F : ) (j : J) :
Equations
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance CommMonCat.limitCommMonoid {J : Type v} (F : ) :
Equations
• One or more equations did not get rendered due to their size.
theorem AddCommMonCat.forget₂CreatesLimit.proof_6 {J : Type u_3} [] [] (t : ) (s : ) :
((fun (s : ) => { toZeroHom := { toFun := fun (v : (.mapCone (.mapCone s)).pt) => (equivShrink (CategoryTheory.Functor.sections ())).1 { val := fun (j : J) => (.mapCone (.mapCone s)).app j v, property := }, map_zero' := }, map_add' := }) s) = ((fun (s : ) => { toZeroHom := { toFun := fun (v : (.mapCone (.mapCone s)).pt) => (equivShrink (CategoryTheory.Functor.sections ())).1 { val := fun (j : J) => (.mapCone (.mapCone s)).app j v, property := }, map_zero' := }, map_add' := }) s)
noncomputable instance AddCommMonCat.forget₂CreatesLimit {J : Type v} :

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

All we need to do is notice that the limit point has an AddCommMonoid instance available,

and then reuse the existing limit.

Equations
• One or more equations did not get rendered due to their size.
theorem AddCommMonCat.forget₂CreatesLimit.proof_3 {J : Type u_2} [] (s : ) (v : (.mapCone (.mapCone s)).pt) :
∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp ((.mapCone (.mapCone s)).app j) (.map f) v = (.mapCone (.mapCone s)).app j' v
theorem AddCommMonCat.forget₂CreatesLimit.proof_5 {J : Type u_3} [] [] (s : ) (x : (.mapCone s).pt) (y : (.mapCone s).pt) :
{ toFun := fun (v : (.mapCone (.mapCone s)).pt) => (equivShrink (CategoryTheory.Functor.sections ())).1 { val := fun (j : J) => (.mapCone (.mapCone s)).app j v, property := }, map_zero' := }.toFun (x + y) = { toFun := fun (v : (.mapCone (.mapCone s)).pt) => (equivShrink (CategoryTheory.Functor.sections ())).1 { val := fun (j : J) => (.mapCone (.mapCone s)).app j v, property := }, map_zero' := }.toFun x + { toFun := fun (v : (.mapCone (.mapCone s)).pt) => (equivShrink (CategoryTheory.Functor.sections ())).1 { val := fun (j : J) => (.mapCone (.mapCone s)).app j v, property := }, map_zero' := }.toFun y
theorem AddCommMonCat.forget₂CreatesLimit.proof_4 {J : Type u_3} [] [] (s : ) :
(equivShrink (CategoryTheory.Functor.sections ())).1 { val := fun (j : J) => (.mapCone (.mapCone s)).app j 0, property := } = 0
theorem AddCommMonCat.forget₂CreatesLimit.proof_2 {J : Type u_2} [] [] ⦃X : J ⦃Y : J (f : X Y) :
CategoryTheory.CategoryStruct.comp ((.obj ().pt).map f) (.app Y) = CategoryTheory.CategoryStruct.comp (.app X)
noncomputable instance CommMonCat.forget₂CreatesLimit {J : Type v} (F : ) :

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

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

Equations
• One or more equations did not get rendered due to their size.
noncomputable def AddCommMonCat.limitCone {J : Type v} :

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

Equations
Instances For
noncomputable def CommMonCat.limitCone {J : Type v} (F : ) :

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

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

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

Equations
Instances For
noncomputable def CommMonCat.limitConeIsLimit {J : Type v} (F : ) :

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

Equations
Instances For
instance AddCommMonCat.hasLimit {J : Type v} :

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

Equations
• =
instance CommMonCat.hasLimit {J : Type v} (F : ) :

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

Equations
• =
instance AddCommMonCat.hasLimitsOfShape {J : Type v} [] :

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

Equations
• =
instance CommMonCat.hasLimitsOfShape {J : Type v} [] :

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

Equations
• =

The category of additive commutative monoids has all limits.

Equations
• =

The category of commutative monoids has all limits.

Equations
• =
Equations
∀ {K : }, Small.{u_1, max u_1 u_2} { x : (j : J) → // }

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

This means the underlying type 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.

The forgetful functor from commutative monoids to monoids preserves all limits.

This means the underlying type 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.
Equations
Equations
noncomputable instance AddCommMonCat.forgetPreservesLimitsOfShape {J : Type v} [] :

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

preserves limits of shape J.

Equations
• One or more equations did not get rendered due to their size.
noncomputable instance CommMonCat.forgetPreservesLimitsOfShape {J : Type v} [] :

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

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

The forgetful functor from additive commutative monoids 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
• One or more equations did not get rendered due to their size.

The forgetful functor from commutative monoids 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
• One or more equations did not get rendered due to their size.