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)).toPrefunctor.obj j)

Equations

• AddGroupCat.addGroupObj F j = let_fun this := inferInstance; this

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

Equations

• GroupCat.groupObj F j = let_fun this := inferInstance; this

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

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

Equations

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

theorem AddGroupCat.sectionsAddSubgroup.proof_3 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddGroupCat) {a : (j : J) → ↑(F.toPrefunctor.obj j)} (ah : a ∈ { toAddSubsemigroup := { carrier := CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)), add_mem' := (_ : ∀ {a b : (j : J) → ↑(F.toPrefunctor.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) }, zero_mem' := (_ : ∀ {j j' : J} (f : j ⟶ j'), (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)).toPrefunctor.map f (0 j) = 0 j') }.toAddSubsemigroup.carrier) (j : J) (j' : J) (f : j ⟶ j') : (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)).toPrefunctor.map f ((-a) j) = (-a) j'

theorem AddGroupCat.sectionsAddSubgroup.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ {a b : (j : J) → ↑(F.toPrefunctor.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

theorem AddGroupCat.sectionsAddSubgroup.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddGroupCat) : ∀ {j j' : J} (f : j ⟶ j'), (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)).toPrefunctor.map f (0 j) = 0 j'

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

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

Equations

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

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

Equations

• AddGroupCat.limitAddGroup F = let_fun this := inferInstance; this

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

Equations

• GroupCat.limitGroup F = let_fun this := inferInstance; this

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 (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v

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.

Equations

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

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).toPrefunctor.map ((fun (s : CategoryTheory.Limits.Cone F) => { toZeroHom := { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }, map_add' := (_ : ∀ (x y : ↑((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s).pt), { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun (x + y) = { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun x + { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun y) }) s) = (CategoryTheory.forget₂ AddGroupCat AddMonCat).toPrefunctor.map ((fun (s : CategoryTheory.Limits.Cone F) => { toZeroHom := { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }, map_add' := (_ : ∀ (x y : ↑((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s).pt), { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun (x + y) = { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun x + { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun y) }) s)

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).toPrefunctor.obj (AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))).pt).toPrefunctor.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)).toPrefunctor.map f)

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) : { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun (x + y) = { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun x + { toFun := fun (v : ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) v = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v) }, map_zero' := (_ : { val := fun (j : J) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0) }.toFun y

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) => ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((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)).toPrefunctor.map f) 0 = ((CategoryTheory.forget AddMonCatMax).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' 0) } = 0

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.

Equations

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

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

Equations

• AddGroupCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMaxAux AddMonCat)))

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

Equations

• GroupCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMax MonCat)))

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

Equations

• AddGroupCat.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMaxAux AddMonCat)))

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

Equations

• GroupCat.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCatMax MonCat)))

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.

Equations

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

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

The category of groups has all limits.

Equations

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

instance AddGroupCat.hasLimits : CategoryTheory.Limits.HasLimits AddGroupCat

Equations

• AddGroupCat.hasLimits = AddGroupCat.hasLimitsOfSize

instance GroupCat.hasLimits : CategoryTheory.Limits.HasLimits GroupCat

Equations

• GroupCat.hasLimits = GroupCat.hasLimitsOfSize

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.

Equations

• AddGroupCat.forget₂AddMonPreservesLimits = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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.

Equations

• GroupCat.forget₂MonPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• AddGroupCat.forget₂MonPreservesLimits = AddGroupCat.forget₂AddMonPreservesLimits

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

Equations

• GroupCat.forget₂MonPreservesLimits = GroupCat.forget₂MonPreservesLimitsOfSize

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.

Equations

• AddGroupCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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.

Equations

• GroupCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• AddGroupCat.forgetPreservesLimits = AddGroupCat.forgetPreservesLimitsOfSize

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

Equations

• GroupCat.forgetPreservesLimits = GroupCat.forgetPreservesLimitsOfSize

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

Equations

• AddCommGroupCat.addCommGroupObj F j = let_fun this := inferInstance; this

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

Equations

• CommGroupCat.commGroupObj F j = let_fun this := inferInstance; this

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

Equations

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

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

Equations

• CommGroupCat.limitCommGroup F = Subgroup.toCommGroup (GroupCat.sectionsSubgroup (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommGroupCatMax GroupCatMax)))

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.

Equations

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

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

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).toPrefunctor.obj (AddMonCat.HasLimits.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).pt).toPrefunctor.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))).toPrefunctor.map f)

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)).toPrefunctor.map ((fun (s : CategoryTheory.Limits.Cone F) => (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)).toPrefunctor.map ((fun (s : CategoryTheory.Limits.Cone F) => (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 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.

Equations

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

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

Equations

• AddCommGroupCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCatMaxAux GroupCatMaxAux)))

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

Equations

• CommGroupCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommGroupCatMax GroupCatMax)))

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

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

instance AddCommGroupCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommGroupCat

Equations

• AddCommGroupCat.hasLimits = AddCommGroupCat.hasLimitsOfSize

instance CommGroupCat.hasLimits : CategoryTheory.Limits.HasLimits CommGroupCat

Equations

• CommGroupCat.hasLimits = CommGroupCat.hasLimitsOfSize

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

Equations

• AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommGroupCat.forget₂GroupPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• AddCommGroupCat.forget₂AddGroupPreservesLimits = AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize

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

Equations

• CommGroupCat.forget₂GroupPreservesLimits = CommGroupCat.forget₂GroupPreservesLimitsOfSize

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.

Equations

• AddCommGroupCat.forget₂AddCommMonPreservesLimitsAux F = AddCommMonCat.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCatMaxAux AddCommMonCat))

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.

Equations

• CommGroupCat.forget₂CommMonPreservesLimitsAux F = CommMonCat.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommGroupCatMax CommMonCat))

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

Equations

• AddCommGroupCat.forget₂AddCommMonPreservesLimits = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommGroupCat.forget₂CommMonPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

theorem AddCommGroupCat.forgetPreservesLimitsOfSize.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 AddCommGroupCat.forgetPreservesLimitsOfSize : 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.)

Equations

• AddCommGroupCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommGroupCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• AddCommGroupCat.forgetPreservesLimits = AddCommGroupCat.forgetPreservesLimitsOfSize

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

Equations

• CommGroupCat.forgetPreservesLimits = CommGroupCat.forgetPreservesLimitsOfSize

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

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

Equations

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

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

@[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

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.

Equations

• AddCommGroupCat.kernelIsoKerOver f = CategoryTheory.Over.isoMk (AddCommGroupCat.kernelIsoKer f)