# Documentation

Mathlib.Algebra.Category.MonCat.Limits

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

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

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

Instances For
instance MonCat.monoidObj {J : Type v} (F : ) (j : J) :
theorem AddMonCat.sectionsAddSubmonoid.proof_2 {J : Type u_1} {j : J} {j' : J} (f : j j') :
↑(F.map f) 0 = 0
AddSubmonoid ((j : J) → ↑(F.obj j))

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

Instances For
theorem AddMonCat.sectionsAddSubmonoid.proof_1 {J : Type u_2} {a : (j : J) → ↑(F.obj j)} {b : (j : J) → ↑(F.obj j)} {j : J} {j' : J} (f : j j') :
J.map CategoryTheory.CategoryStruct.toQuiver (Type (max u_1 u_2)) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor j j' f ((((j : J) → ↑(F.obj j)) + ((j : J) → ↑(F.obj j))) ((j : J) → ↑(F.obj j)) instHAdd a b j) = (((j : J) → ↑(F.obj j)) + ((j : J) → ↑(F.obj j))) ((j : J) → ↑(F.obj j)) instHAdd a b j'
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.

Instances For

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

Instances For
∀ (x x_1 : ), ZeroHom.toFun { toFun := ().π.app j, map_zero' := (_ : J.app inst✝ TypeMax CategoryTheory.types (().obj ().pt) () ().π j 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj ().pt) () ().π j 0) } (x + x_1) = ZeroHom.toFun { toFun := ().π.app j, map_zero' := (_ : J.app inst✝ TypeMax CategoryTheory.types (().obj ().pt) () ().π j 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj ().pt) () ().π j 0) } (x + x_1)
noncomputable def MonCat.limitπMonoidHom {J : Type v} (F : ) (j : J) :

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

Instances For
theorem AddMonCat.HasLimits.limitCone.proof_1 {J : Type u_1} :
∀ (x x_1 : J) (f : x x_1), CategoryTheory.CategoryStruct.comp ((().obj (AddMonCat.of ().pt)).map f) () = CategoryTheory.CategoryStruct.comp () (F.map f)
noncomputable def AddMonCat.HasLimits.limitCone {J : Type v} :

(Internal use only; use the limits API.)

Instances For
noncomputable def MonCat.HasLimits.limitCone {J : Type v} (F : ) :

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

Instances For
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_4 {J : Type u_1} (s : ) :
().map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : s.pt), ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().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 s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : s.pt), ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } y) }) s)
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_2 {J : Type u_2} (s : ) :
{ val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_1 {J : Type u_1} (s : ) (v : (().mapCone s).pt) :
∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v
theorem AddMonCat.HasLimits.limitConeIsLimit.proof_3 {J : Type u_2} (s : ) (x : s.pt) (y : s.pt) :
ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () v = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct ((().obj (().mapCone s).pt).obj j) () () ((().mapCone s).π.app j) () 0 = J.app inst✝ TypeMax CategoryTheory.types (().obj (().mapCone s).pt) () (().mapCone s).π j' 0) } = 0) } y
noncomputable def AddMonCat.HasLimits.limitConeIsLimit {J : Type v} :

(Internal use only; use the limits API.)

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

Instances For

The category of additive monoids has all limits.

The category of monoids has all limits.

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.

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.

noncomputable instance MonCat.forgetPreservesLimits :
Type ((max u1 u2) + 1)

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

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

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

Instances For
instance CommMonCat.commMonoidObj {J : Type v} (j : J) :
theorem AddCommMonCat.forget₂CreatesLimit.proof_6 {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)
theorem AddCommMonCat.forget₂CreatesLimit.proof_2 {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 AddCommMonCat.forget₂CreatesLimit.proof_3 {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
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.

theorem AddCommMonCat.forget₂CreatesLimit.proof_5 {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 AddCommMonCat.forget₂CreatesLimit.proof_4 {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 CommMonCat.forget₂CreatesLimit {J : Type v} :

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.

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

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

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

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

Instances For
noncomputable def CommMonCat.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 monoids has all limits.

The category of commutative monoids has all limits.

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.

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.

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.

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.