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.

abbrev AddMonCatMax :
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
      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

      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} [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'

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

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

          (Internal use only; use the limits API.)

          Instances For

            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} [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_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

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

              Instances For

                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.

                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.

                abbrev AddCommMonCatMax :
                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
                    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_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) :

                    We show that the forgetful functor AddCommMonCatAddMonCat 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_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

                    We show that the forgetful functor CommMonCatMonCat creates limits.

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

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

                    Instances For

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

                      Instances For

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

                        Instances For

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

                          Instances For

                            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.

                            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.