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.

abbrev AddMonCatMax : Type ((max u1 u2) + 1)

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

@[inline, reducible]

abbrev MonCatMax : Type ((max u1 u2) + 1)

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

instance AddMonCat.addMonoidObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (j : J) : AddMonoid ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)).obj j)

instance MonCat.monoidObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) (j : J) : Monoid ((CategoryTheory.Functor.comp F (CategoryTheory.forget MonCat)).obj j)

theorem AddMonCat.sectionsAddSubmonoid.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) {j : J} {j' : J} (f : j ⟶ j') : ↑(F.map f) 0 = 0

def AddMonCat.sectionsAddSubmonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : AddSubmonoid ((j : J) → ↑(F.obj j))

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

theorem AddMonCat.sectionsAddSubmonoid.proof_1 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) {a : (j : J) → ↑(F.obj j)} {b : (j : J) → ↑(F.obj j)} (ah : a ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))) (bh : b ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))) {j : J} {j' : J} (f : j ⟶ j') : J.map CategoryTheory.CategoryStruct.toQuiver (Type (max u_1 u_2)) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)).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} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) : Submonoid ((j : J) → ↑(F.obj j))

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

instance AddMonCat.limitAddMonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : AddMonoid (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt

instance MonCat.limitMonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) : Monoid (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget MonCatMax))).pt

theorem AddMonCat.limitπAddMonoidHom.proof_1 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (j : J) : J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π j 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π j 0

noncomputable def AddMonCat.limitπAddMonoidHom {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (j : J) : (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt →+ (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)).obj j

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

theorem AddMonCat.limitπAddMonoidHom.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (j : J) : ∀ (x x_1 : (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt), ZeroHom.toFun { toFun := (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π.app j, map_zero' := (_ : J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π j 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π j 0) } (x + x_1) = ZeroHom.toFun { toFun := (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π.app j, map_zero' := (_ : J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π j 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).π j 0) } (x + x_1)

noncomputable def MonCat.limitπMonoidHom {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) (j : J) : (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget MonCatMax))).pt →* (CategoryTheory.Functor.comp F (CategoryTheory.forget MonCat)).obj j

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

theorem AddMonCat.HasLimits.limitCone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : ∀ (x x_1 : J) (f : x ⟶ x_1), CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj (AddMonCat.of (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax))).pt)).map f) (AddMonCat.limitπAddMonoidHom F x_1) = CategoryTheory.CategoryStruct.comp (AddMonCat.limitπAddMonoidHom F x) (F.map f)

noncomputable def AddMonCat.HasLimits.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : CategoryTheory.Limits.Cone F

(Internal use only; use the limits API.)

noncomputable def MonCat.HasLimits.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) : CategoryTheory.Limits.Cone F

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

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_4 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.forget AddMonCatMax).map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).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 ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } y) }) s) = (CategoryTheory.forget AddMonCatMax).map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).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 ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } y) }) s)

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_2 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (s : CategoryTheory.Limits.Cone F) : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (s : CategoryTheory.Limits.Cone F) (v : ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_3 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (s : CategoryTheory.Limits.Cone F) (x : ↑s.pt) (y : ↑s.pt) : ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone s).π.app j) ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone s).pt) (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone s).π j' 0) } = 0) } y

noncomputable def AddMonCat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : CategoryTheory.Limits.IsLimit (AddMonCat.HasLimits.limitCone F)

(Internal use only; use the limits API.)

noncomputable def MonCat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) : CategoryTheory.Limits.IsLimit (MonCat.HasLimits.limitCone F)

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

instance AddMonCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} AddMonCatMax

The category of additive monoids has all limits.

theorem AddMonCat.hasLimitsOfSize.proof_1 : CategoryTheory.Limits.HasLimitsOfSize.{u_1, u_1, max u_2 u_1, max (u_2 + 1) (u_1 + 1)} AddMonCatMax

instance MonCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} MonCatMax

The category of monoids has all limits.

instance AddMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddMonCat

instance MonCat.hasLimits : CategoryTheory.Limits.HasLimits MonCat

noncomputable instance AddMonCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget AddMonCatMax)

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

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

noncomputable instance MonCat.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget MonCat)

abbrev AddCommMonCatMax : Type ((max u1 u2) + 1)

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

@[inline, reducible]

abbrev CommMonCatMax : Type ((max u1 u2) + 1)

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

instance AddCommMonCat.addCommMonoidObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) (j : J) : AddCommMonoid ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommMonCatMax)).obj j)

instance CommMonCat.commMonoidObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommMonCatMax) (j : J) : CommMonoid ((CategoryTheory.Functor.comp F (CategoryTheory.forget CommMonCatMax)).obj j)

instance AddCommMonCat.limitAddCommMonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) : AddCommMonoid (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommMonCatMax))).pt

instance CommMonCat.limitCommMonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommMonCatMax) : CommMonoid (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget CommMonCatMax))).pt

theorem AddCommMonCat.forget₂CreatesLimit.proof_6 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) (c' : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCatMax))) (t : CategoryTheory.Limits.IsLimit c') (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s).pt), ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } y) }) s) = (CategoryTheory.forget₂ AddCommMonCat AddMonCat).map ((fun s => { toZeroHom := { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s).pt), ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } y) }) s)

theorem AddCommMonCat.forget₂CreatesLimit.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj (AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).pt).map f) ((AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).π.app Y) = CategoryTheory.CategoryStruct.comp ((AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).π.app X) ((CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).map f)

theorem AddCommMonCat.forget₂CreatesLimit.proof_3 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) (s : CategoryTheory.Limits.Cone F) (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v

noncomputable instance AddCommMonCat.forget₂CreatesLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommMonCat AddMonCatMax)

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} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) (s : CategoryTheory.Limits.Cone F) (x : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s).pt) (y : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s).pt) : ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } (x + y) = ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } x + ZeroHom.toFun { toFun := fun v => { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' v) }, map_zero' := (_ : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0) } y

theorem AddCommMonCat.forget₂CreatesLimit.proof_1 : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget₂ AddCommMonCat AddMonCatMax)

theorem AddCommMonCat.forget₂CreatesLimit.proof_4 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) (s : CategoryTheory.Limits.Cone F) : { val := fun j => J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp TypeMax CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone s)).π j' 0) } = 0

noncomputable instance CommMonCat.forget₂CreatesLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommMonCatMax) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommMonCat MonCatMax)

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.

theorem AddCommMonCat.limitCone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCatMax AddMonCatMax))

noncomputable def AddCommMonCat.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) : CategoryTheory.Limits.Cone F

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

noncomputable def CommMonCat.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommMonCatMax) : CategoryTheory.Limits.Cone F

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

noncomputable def AddCommMonCat.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommMonCatMax) : CategoryTheory.Limits.IsLimit (AddCommMonCat.limitCone F)

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

noncomputable def CommMonCat.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommMonCatMax) : CategoryTheory.Limits.IsLimit (CommMonCat.limitCone F)

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

theorem AddCommMonCat.hasLimitsOfSize.proof_1 : CategoryTheory.Limits.HasLimitsOfSize.{u_1, u_1, max u_2 u_1, max (u_2 + 1) (u_1 + 1)} AddCommMonCatMax

instance AddCommMonCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} AddCommMonCatMax

The category of additive commutative monoids has all limits.

instance CommMonCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} CommMonCatMax

The category of commutative monoids has all limits.

instance AddCommMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommMonCat

instance CommMonCat.hasLimits : CategoryTheory.Limits.HasLimits CommMonCat

theorem AddCommMonCat.forget₂AddMonPreservesLimits.proof_1 {J : Type u_1} (𝒥 : CategoryTheory.Category.{u_1, u_1} J) {F : CategoryTheory.Functor J AddCommMonCatMax} : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCatMax AddMonCatMax))

noncomputable instance AddCommMonCat.forget₂AddMonPreservesLimits : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ AddCommMonCatMax AddMonCatMax)

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.

noncomputable instance CommMonCat.forget₂MonPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ CommMonCatMax MonCatMax)

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.

noncomputable instance AddCommMonCat.forget₂MonPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

noncomputable instance CommMonCat.forget₂MonPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommMonCat MonCat)

theorem AddCommMonCat.forgetPreservesLimitsOfSize.proof_1 : ∀ {x : Type u_1} (x_1 : CategoryTheory.Category.{u_1, u_1} x) {F : CategoryTheory.Functor x AddCommMonCatMax}, CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCatMax AddMonCatMax))

noncomputable instance AddCommMonCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget AddCommMonCatMax)

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.

noncomputable instance CommMonCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget CommMonCatMax)

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.

noncomputable instance AddCommMonCat.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommMonCat)

noncomputable instance CommMonCat.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommMonCat)