The category of (commutative) (additive) groups has all limits

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

instance AddGroupCat.addGroupObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) (j : J) : AddGroup ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)).obj j)

instance GroupCat.groupObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMax) (j : J) : Group ((CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)).obj j)

def AddGroupCat.sectionsAddSubgroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddGroupCat) : AddSubgroup ((j : J) → ↑(F.obj j))

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

theorem AddGroupCat.sectionsAddSubgroup.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ {j j' : J} (f : j ⟶ j'), J.map CategoryTheory.CategoryStruct.toQuiver (Type (max u_2 u_1)) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)).toPrefunctor j j' f (OfNat.ofNat ((j : J) → ↑((CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)).obj j)) 0 Zero.toOfNat0 j) = OfNat.ofNat ((j : J) → ↑((CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)).obj j)) 0 Zero.toOfNat0 j'

theorem AddGroupCat.sectionsAddSubgroup.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ (AddMonCat.sectionsAddSubmonoid (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).toAddSubsemigroup.carrier → b ∈ (AddMonCat.sectionsAddSubmonoid (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).toAddSubsemigroup.carrier → a + b ∈ (AddMonCat.sectionsAddSubmonoid (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).toAddSubsemigroup.carrier

def GroupCat.sectionsSubgroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCat) : Subgroup ((j : J) → ↑(F.obj j))

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

noncomputable instance AddGroupCat.limitAddGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) : AddGroup (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat))).pt

noncomputable instance GroupCat.limitGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMax) : Group (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat))).pt

theorem AddGroupCat.Forget₂.createsLimit.proof_3 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) (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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' 0) } = 0

noncomputable instance AddGroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ GroupCatMaxAux AddMonCatMax)

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

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

theorem AddGroupCat.Forget₂.createsLimit.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) (s : CategoryTheory.Limits.Cone F) (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' v

theorem AddGroupCat.Forget₂.createsLimit.proof_4 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) (s : CategoryTheory.Limits.Cone F) (x : ↑((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s).pt) (y : ↑((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' 0) } = 0) } y

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

theorem AddGroupCat.Forget₂.createsLimit.proof_5 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) (c' : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))) (t : CategoryTheory.Limits.IsLimit c') (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : ↑((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' 0) } = 0) } y) }) s) = (CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' 0) } = 0) }, map_add' := (_ : ∀ (x y : ↑((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) v = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat 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₂ AddGroupCat AddMonCat).mapCone s)).pt).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).obj j') (((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)).map f) 0 = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCatMax)) ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π j' 0) } = 0) } y) }) s)

noncomputable instance GroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMax) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ GroupCatMax MonCatMax)

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

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

theorem AddGroupCat.limitCone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J GroupCatMaxAux) : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMaxAux AddMonCat))

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

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

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

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

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

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

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

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

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

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

The category of additive groups has all limits.

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

The category of groups has all limits.

instance AddGroupCat.hasLimits : CategoryTheory.Limits.HasLimits AddGroupCat

instance GroupCat.hasLimits : CategoryTheory.Limits.HasLimits GroupCat

noncomputable instance AddGroupCat.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₂ GroupCatMaxAux AddMonCat)

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

This means the underlying additive monoid of a limit can be computed as a limit in the category of additive monoids.

theorem AddGroupCat.forget₂AddMonPreservesLimits.proof_1 {J : Type u_1} : ∀ {x : CategoryTheory.Category.{u_1, u_1} J} {F : CategoryTheory.Functor J GroupCatMaxAux}, CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMaxAux AddMonCat))

noncomputable instance GroupCat.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₂ GroupCatMax MonCat)

The forgetful functor from groups to monoids preserves all limits.

This means the underlying monoid of a limit can be computed as a limit in the category of monoids.

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

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

theorem AddGroupCat.forgetPreservesLimitsOfSize.proof_1 {J : Type u_1} : ∀ {x : CategoryTheory.Category.{u_1, u_1} J} {F : CategoryTheory.Functor J GroupCatMaxAux}, CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMaxAux AddMonCat))

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

The forgetful functor from additive groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

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

The forgetful functor from groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

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

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

instance AddCommGroupCat.addCommGroupObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCatMaxAux) (j : J) : AddCommGroup ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCatMaxAux)).obj j)

instance CommGroupCat.commGroupObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommGroupCatMax) (j : J) : CommGroup ((CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCatMax)).obj j)

noncomputable instance AddCommGroupCat.limitAddCommGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCat) : AddCommGroup (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCatMaxAux))).pt

noncomputable instance CommGroupCat.limitCommGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommGroupCat) : CommGroup (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCatMax))).pt

theorem AddCommGroupCat.Forget₂.createsLimit.proof_2 : CategoryTheory.Faithful (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat))

theorem AddCommGroupCat.Forget₂.createsLimit.proof_3 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCatMaxAux) (c' : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat GroupCatMaxAux))) (t : CategoryTheory.Limits.IsLimit c') (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).map ((fun s => (AddMonCat.HasLimits.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).1 ((CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).mapCone s)) s) = (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).map ((fun s => (AddMonCat.HasLimits.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).1 ((CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).mapCone s)) s)

noncomputable instance AddCommGroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCatMaxAux) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommGroupCat GroupCatMaxAux)

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

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

theorem AddCommGroupCat.Forget₂.createsLimit.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCatMaxAux) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj (AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).pt).map f) ((AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).π.app Y) = CategoryTheory.CategoryStruct.comp ((AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).π.app X) ((CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat))).map f)

noncomputable instance CommGroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommGroupCatMax) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommGroupCat GroupCatMax)

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

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

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

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

theorem AddCommGroupCat.limitCone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCat) : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCatMaxAux GroupCatMaxAux))

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

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

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

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

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

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

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

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

The category of additive commutative groups has all limits.

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

The category of commutative groups has all limits.

instance AddCommGroupCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommGroupCat

instance CommGroupCat.hasLimits : CategoryTheory.Limits.HasLimits CommGroupCat

theorem AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize.proof_1 {J : Type u_1} {𝒥 : CategoryTheory.Category.{u_1, u_1} J} {F : CategoryTheory.Functor J AddCommGroupCatMaxAux} : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCatMaxAux GroupCatMaxAux))

noncomputable instance AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ AddCommGroupCatMaxAux GroupCatMaxAux)

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

noncomputable instance CommGroupCat.forget₂GroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ CommGroupCatMax GroupCatMax)

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

noncomputable instance AddCommGroupCat.forget₂AddGroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat)

noncomputable instance CommGroupCat.forget₂GroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommGroupCat GroupCat)

noncomputable def AddCommGroupCat.forget₂AddCommMonPreservesLimitsAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddCommGroupCatMaxAux) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ AddCommGroupCatMaxAux AddCommMonCat).mapCone (AddCommGroupCat.limitCone F))

An auxiliary declaration to speed up typechecking.

noncomputable def CommGroupCat.forget₂CommMonPreservesLimitsAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommGroupCatMax) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommGroupCatMax CommMonCat).mapCone (CommGroupCat.limitCone F))

An auxiliary declaration to speed up typechecking.

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

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

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

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

noncomputable instance AddCommGroupCat.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget AddCommGroupCatMaxAux)

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

theorem AddCommGroupCat.forgetPreservesLimits.proof_1 {J : Type u_1} : ∀ {x : CategoryTheory.Category.{u_1, u_1} J} {F : CategoryTheory.Functor J AddCommGroupCatMaxAux}, CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddGroupCat))

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

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

def AddCommGroupCat.kernelIsoKer {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Limits.kernel f ≅ AddCommGroupCat.of { x // x ∈ AddMonoidHom.ker f }

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

@[simp]

theorem AddCommGroupCat.kernelIsoKer_hom_comp_subtype {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.kernelIsoKer f).hom (AddSubgroup.subtype (AddMonoidHom.ker f)) = CategoryTheory.Limits.kernel.ι f

@[simp]

theorem AddCommGroupCat.kernelIsoKer_inv_comp_ι {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGroupCat.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = AddSubgroup.subtype (AddMonoidHom.ker f)

@[simp]

theorem AddCommGroupCat.kernelIsoKerOver_hom_left_apply_coe {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) (g : ↑(CategoryTheory.Limits.kernel f)) : ↑(↑(AddCommGroupCat.kernelIsoKerOver f).hom.left g) = ↑(CategoryTheory.Limits.kernel.ι f) g

@[simp]

theorem AddCommGroupCat.kernelIsoKerOver_inv_left_apply {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : ∀ (a : ↑(CategoryTheory.Limits.KernelFork.ofι (AddSubgroup.subtype (AddMonoidHom.ker f)) (_ : CategoryTheory.CategoryStruct.comp (AddSubgroup.subtype (AddMonoidHom.ker f)) f = 0)).pt), ↑(AddCommGroupCat.kernelIsoKerOver f).inv.left a = ↑(CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair f 0) (CategoryTheory.Limits.KernelFork.ofι (AddSubgroup.subtype (AddMonoidHom.ker f)) (_ : CategoryTheory.CategoryStruct.comp (AddSubgroup.subtype (AddMonoidHom.ker f)) f = 0))) a

def AddCommGroupCat.kernelIsoKerOver {G : AddCommGroupCat} {H : AddCommGroupCat} (f : G ⟶ H) : CategoryTheory.Over.mk (CategoryTheory.Limits.kernel.ι f) ≅ CategoryTheory.Over.mk (AddSubgroup.subtype (AddMonoidHom.ker f))

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