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.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) (j : J) : AddGroup ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)).obj j)

Equations

• AddGroupCat.addGroupObj F j = inferInstanceAs (AddGroup ↑(F.obj j))

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

Equations

• GroupCat.groupObj F j = inferInstanceAs (Group ↑(F.obj j))

def AddGroupCat.sectionsAddSubgroup {J : Type v} [CategoryTheory.Category.{w, v} 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.

Equations

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

theorem AddGroupCat.sectionsAddSubgroup.proof_3 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGroupCat) {a : (j : J) → ↑(F.obj j)} (ah : a ∈ { toAddSubsemigroup := { carrier := CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)), add_mem' := ⋯ }, zero_mem' := ⋯ }.carrier) (j : J) (j' : J) (f : j ⟶ j') : (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)).map f ((-a) j) = (-a) j'

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

theorem AddGroupCat.sectionsAddSubgroup.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} 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)).map f (0 j) = 0 j'

def GroupCat.sectionsSubgroup {J : Type v} [CategoryTheory.Category.{w, v} 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.

Equations

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

instance AddGroupCat.sectionsAddGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) : AddGroup ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))

Equations

• AddGroupCat.sectionsAddGroup F = AddSubgroup.toAddGroup (AddGroupCat.sectionsAddSubgroup F)

instance GroupCat.sectionsGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) : Group ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))

Equations

• GroupCat.sectionsGroup F = Subgroup.toGroup (GroupCat.sectionsSubgroup F)

noncomputable instance AddGroupCat.limitAddGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : AddGroup (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat))).pt

Equations

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

noncomputable instance GroupCat.limitGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))] : Group (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat))).pt

Equations

• GroupCat.limitGroup F = inferInstanceAs (Group (Shrink.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))))

instance AddGroupCat.instSmallElemForAllObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompMonCatInstMonCatLargeCategoryAddGroupCatInstAddGroupCatLargeCategoryForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatForgetSections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))

Equations

• ⋯ = ⋯

instance GroupCat.instSmallElemForAllObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompMonCatInstMonCatLargeCategoryGroupCatInstGroupCatLargeCategoryForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatForgetSections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))] : Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ GroupCat MonCat)) (CategoryTheory.forget MonCat)))

Equations

• ⋯ = ⋯

theorem AddGroupCat.Forget₂.createsLimit.proof_5 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u_2, max u_2 u_3} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] (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 : CategoryTheory.Limits.Cone F) => { toZeroHom := { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => (equivShrink ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))).1 { val := fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := ⋯ }, map_zero' := ⋯ }, map_add' := ⋯ }) s) = (CategoryTheory.forget₂ AddGroupCat AddMonCat).map ((fun (s : CategoryTheory.Limits.Cone F) => { toZeroHom := { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => (equivShrink ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))).1 { val := fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := ⋯ }, map_zero' := ⋯ }, map_add' := ⋯ }) s)

theorem AddGroupCat.Forget₂.createsLimit.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u_3, max u_3 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] ⦃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_3 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u_1, max u_1 u_3} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] (s : CategoryTheory.Limits.Cone F) : (equivShrink ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))).1 { val := fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j 0, property := ⋯ } = 0

theorem AddGroupCat.Forget₂.createsLimit.proof_4 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u_1, max u_1 u_3} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] (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 AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => (equivShrink ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))).1 { val := fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := ⋯ }, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => (equivShrink ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))).1 { val := fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := ⋯ }, map_zero' := ⋯ }.toFun x + { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) => (equivShrink ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)))).1 { val := fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j v, property := ⋯ }, map_zero' := ⋯ }.toFun y

noncomputable instance AddGroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddGroupCat AddMonCat)

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_2 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddGroupCat) (s : CategoryTheory.Limits.Cone F) (v : ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).pt) : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j) ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat)) (CategoryTheory.forget AddMonCat)).map f) v = ((CategoryTheory.forget AddMonCat).mapCone ((CategoryTheory.forget₂ AddGroupCat AddMonCat).mapCone s)).π.app j' v

noncomputable instance GroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ GroupCat MonCat)

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.

theorem AddGroupCat.limitCone.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u_3, max u_3 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddGroupCat AddMonCat))

noncomputable def AddGroupCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : 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₂ AddGroupCat AddMonCat)))

noncomputable def GroupCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))] : 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₂ GroupCat MonCat)))

noncomputable def AddGroupCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : 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₂ AddGroupCat AddMonCat)))

noncomputable def GroupCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))] : 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₂ GroupCat MonCat)))

instance AddGroupCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)))] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget AddGroupCat).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

instance GroupCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget GroupCat)))] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget GroupCat).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

instance AddGroupCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J AddGroupCat

If J is u-small, AddGroupCat.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance GroupCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J GroupCat

If J is u-small, GroupCat.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance AddGroupCat.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddGroupCat

The category of additive groups has all limits.

Equations

• ⋯ = ⋯

instance GroupCat.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} GroupCat

The category of groups has all limits.

Equations

• ⋯ = ⋯

instance AddGroupCat.hasLimits : CategoryTheory.Limits.HasLimits AddGroupCat

Equations

• AddGroupCat.hasLimits = ⋯

instance GroupCat.hasLimits : CategoryTheory.Limits.HasLimits GroupCat

Equations

• GroupCat.hasLimits = ⋯

theorem AddGroupCat.forget₂AddMonPreservesLimitsOfSize.proof_1 [UnivLE.{u_2, u_1} ] {J : Type u_2} : ∀ {x : CategoryTheory.Category.{u_3, u_2} J} {K : CategoryTheory.Functor J AddGroupCat}, Small.{u_1, max u_1 u_2} { x_1 : (j : J) → (CategoryTheory.Functor.comp K (CategoryTheory.forget AddGroupCat)).obj j // x_1 ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp K (CategoryTheory.forget AddGroupCat)) }

theorem AddGroupCat.forget₂AddMonPreservesLimitsOfSize.proof_2 [UnivLE.{u_2, u_3} ] {J : Type u_2} : ∀ {x : CategoryTheory.Category.{u_1, u_2} J} {K : CategoryTheory.Functor J AddGroupCat}, CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp K (CategoryTheory.forget₂ AddGroupCat AddMonCat))

noncomputable instance AddGroupCat.forget₂AddMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddGroupCat 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

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

noncomputable instance GroupCat.forget₂MonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ GroupCat 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

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

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

Equations

• AddGroupCat.forget₂MonPreservesLimits = AddGroupCat.forget₂AddMonPreservesLimitsOfSize

theorem AddGroupCat.forget₂MonPreservesLimits.proof_1 (α : Type u_1) : Small.{u_1, u_1} α

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

Equations

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

noncomputable instance AddGroupCat.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddGroupCat)

If J is u-small, the forgetful functor from AddGroupCat.{u}

preserves limits of shape J.

Equations

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

theorem AddGroupCat.forgetPreservesLimitsOfShape.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] [Small.{u_1, u_2} J] {F : CategoryTheory.Functor J AddGroupCat} : Small.{u_1, max u_1 u_2} { x : (j : J) → (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)).obj j // x ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)) }

noncomputable instance GroupCat.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget GroupCat)

If J is u-small, the forgetful functor from GroupCat.{u} preserves limits of shape J.

Equations

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

noncomputable instance AddGroupCat.forgetPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGroupCat)

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

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

noncomputable instance GroupCat.forgetPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget GroupCat)

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

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

theorem AddGroupCat.forgetPreservesLimits.proof_1 (α : Type u_1) : Small.{u_1, u_1} α

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.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) (j : J) : AddCommGroup ((CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)).obj j)

Equations

• AddCommGroupCat.addCommGroupObj F j = inferInstanceAs (AddCommGroup ↑(F.obj j))

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

Equations

• CommGroupCat.commGroupObj F j = inferInstanceAs (CommGroup ↑(F.obj j))

noncomputable instance AddCommGroupCat.limitAddCommGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat))).pt

Equations

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

noncomputable instance CommGroupCat.limitCommGroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCat)))] : CommGroup (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCat))).pt

Equations

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

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

theorem AddCommGroupCat.Forget₂.createsLimit.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u_3, max u_3 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] ⦃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)

theorem AddCommGroupCat.Forget₂.createsLimit.proof_4 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u_2, max u_2 u_3} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] (c' : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))) (t : CategoryTheory.Limits.IsLimit c') (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).map ((fun (s : CategoryTheory.Limits.Cone F) => (AddMonCat.HasLimits.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).1 ((CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).mapCone s)) s) = (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).map ((fun (s : CategoryTheory.Limits.Cone F) => (AddMonCat.HasLimits.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)))).1 ((CategoryTheory.Functor.comp (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat) (CategoryTheory.forget₂ AddGroupCat AddMonCat)).mapCone s)) s)

noncomputable instance AddCommGroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat)

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_1 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u_1, max u_1 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : Small.{u_1, max u_1 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))

noncomputable instance CommGroupCat.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCat)))] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommGroupCat GroupCat)

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.

theorem AddCommGroupCat.limitCone.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u_3, max u_3 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))

noncomputable def AddCommGroupCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget 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₂ AddCommGroupCat AddGroupCat)))

noncomputable def CommGroupCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget 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₂ CommGroupCat GroupCat)))

noncomputable def AddCommGroupCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : 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.Category.{w, v} J] (F : CategoryTheory.Functor J CommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCat)))] : CategoryTheory.Limits.IsLimit (CommGroupCat.limitCone F)

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

Equations

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

instance AddCommGroupCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget AddCommGroupCat).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

instance CommGroupCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCat)))] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget CommGroupCat).sections is u-small, F has a limit.

Equations

• ⋯ = ⋯

instance AddCommGroupCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J AddCommGroupCat

If J is u-small, AddCommGroupCat.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance CommGroupCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J CommGroupCat

If J is u-small, CommGroupCat.{u} has limits of shape J.

Equations

• ⋯ = ⋯

instance AddCommGroupCat.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddCommGroupCat

The category of additive commutative groups has all limits.

Equations

• ⋯ = ⋯

instance CommGroupCat.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommGroupCat

The category of commutative groups has all limits.

Equations

• ⋯ = ⋯

instance AddCommGroupCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommGroupCat

Equations

• AddCommGroupCat.hasLimits = ⋯

instance CommGroupCat.hasLimits : CategoryTheory.Limits.HasLimits CommGroupCat

Equations

• CommGroupCat.hasLimits = ⋯

theorem AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize.proof_2 [UnivLE.{u_2, u_3} ] {J : Type u_2} {𝒥 : CategoryTheory.Category.{u_1, u_2} J} : ∀ {K : CategoryTheory.Functor J AddCommGroupCat}, CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp K (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))

noncomputable instance AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat)

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

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

theorem AddCommGroupCat.forget₂AddGroupPreservesLimitsOfSize.proof_1 [UnivLE.{u_2, u_1} ] {J : Type u_2} {𝒥 : CategoryTheory.Category.{u_3, u_2} J} : ∀ {K : CategoryTheory.Functor J AddCommGroupCat}, Small.{u_1, max u_1 u_2} { x : (j : J) → (CategoryTheory.Functor.comp K (CategoryTheory.forget AddCommGroupCat)).obj j // x ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp K (CategoryTheory.forget AddCommGroupCat)) }

noncomputable instance CommGroupCat.forget₂GroupPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGroupCat GroupCat)

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

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

theorem AddCommGroupCat.forget₂AddGroupPreservesLimits.proof_1 (α : Type u_1) : Small.{u_1, u_1} α

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

theorem AddCommGroupCat.forget₂AddCommMonPreservesLimitsAux.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u_1, max u_1 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : Small.{u_1, max u_1 u_2} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))

noncomputable def AddCommGroupCat.forget₂AddCommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ AddCommGroupCat 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₂ AddCommGroupCat AddCommMonCat))

noncomputable def CommGroupCat.forget₂CommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGroupCat) [Small.{u, max u v} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget CommGroupCat)))] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommGroupCat 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₂ CommGroupCat CommMonCat))

noncomputable instance AddCommGroupCat.forget₂AddCommMonPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ AddCommGroupCat AddCommMonCat)

If J is u-small, the forgetful functor from AddCommGroupCat.{u} to AddCommMonCat.{u} preserves limits of shape J.

Equations

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

theorem AddCommGroupCat.forget₂AddCommMonPreservesLimitsOfShape.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] [Small.{u_1, u_2} J] {F : CategoryTheory.Functor J AddCommGroupCat} : Small.{u_1, max u_1 u_2} { x : (j : J) → (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)).obj j // x ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)) }

noncomputable instance CommGroupCat.forget₂CommMonPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ CommGroupCat CommMonCat)

If J is u-small, the forgetful functor from CommGroupCat.{u} to CommMonCat.{u} preserves limits of shape J.

Equations

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

noncomputable instance AddCommGroupCat.forget₂AddCommMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 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

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

noncomputable instance CommGroupCat.forget₂CommMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 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

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

theorem AddCommGroupCat.forgetPreservesLimitsOfShape.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] [Small.{u_1, u_2} J] {F : CategoryTheory.Functor J AddCommGroupCat} : Small.{u_1, max u_1 u_2} { x : (j : J) → (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)).obj j // x ∈ CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)) }

noncomputable instance AddCommGroupCat.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddCommGroupCat)

If J is u-small, the forgetful functor from AddCommGroupCat.{u}

preserves limits of shape J.

Equations

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

noncomputable instance CommGroupCat.forgetPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommGroupCat)

If J is u-small, the forgetful functor from CommGroupCat.{u} preserves limits of shape J.

Equations

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

noncomputable instance AddCommGroupCat.forgetPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGroupCat)

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

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

noncomputable instance CommGroupCat.forgetPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGroupCat)

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

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

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

Equations

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