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

Equations

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

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

Equations

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

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

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

def AddGrp.sectionsAddSubgroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) : AddSubgroup ((j : J) → ↑(F.obj j))

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

Equations

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

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

def Grp.sectionsSubgroup {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) : Subgroup ((j : J) → ↑(F.obj j))

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

Equations

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

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

Equations

• AddGrp.sectionsAddGroup F = (AddGrp.sectionsAddSubgroup F).toAddGroup

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

Equations

• Grp.sectionsGroup F = (Grp.sectionsSubgroup F).toGroup

def AddGrp.sectionsπAddMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) (j : J) : ↑(F.comp (CategoryTheory.forget AddGrp)).sections →+ ↑(F.obj j)

The projection from Functor.sections to a factor as an AddMonoidHom.

Equations

• AddGrp.sectionsπAddMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j, map_zero' := ⋯, map_add' := ⋯ }

theorem AddGrp.sectionsπAddMonoidHom.proof_1 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGrp) (j : J) : (fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j) 0 = (fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j) 0

theorem AddGrp.sectionsπAddMonoidHom.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J AddGrp) (j : J) : ∀ (x x_1 : ↑(F.comp (CategoryTheory.forget AddGrp)).sections), { toFun := fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j, map_zero' := ⋯ }.toFun (x + x_1)

def Grp.sectionsπMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) (j : J) : ↑(F.comp (CategoryTheory.forget Grp)).sections →* ↑(F.obj j)

The projection from Functor.sections to a factor as a MonoidHom.

Equations

• Grp.sectionsπMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget Grp)).sections) => ↑x j, map_one' := ⋯, map_mul' := ⋯ }

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

Equations

• AddGrp.limitAddGroup F = inferInstanceAs (AddGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddGrp)).sections))

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

Equations

• Grp.limitGroup F = inferInstanceAs (Group (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget Grp)).sections))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

We show that the forgetful functor AddGrp ⥤ 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 AddGrp.Forget₂.createsLimit.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u_3, max u_3 u_2} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj (AddMonCat.HasLimits.limitCone (F.comp (CategoryTheory.forget₂ AddGrp AddMonCat))).pt).map f) ((AddMonCat.HasLimits.limitCone (F.comp (CategoryTheory.forget₂ AddGrp AddMonCat))).π.app Y) = CategoryTheory.CategoryStruct.comp ((AddMonCat.HasLimits.limitCone (F.comp (CategoryTheory.forget₂ AddGrp AddMonCat))).π.app X) ((F.comp (CategoryTheory.forget₂ AddGrp AddMonCat)).map f)

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

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

We show that the forgetful functor Grp ⥤ 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 AddGrp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : CategoryTheory.Limits.Cone F

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

Equations

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

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

noncomputable def Grp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : CategoryTheory.Limits.Cone F

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

Equations

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

noncomputable def AddGrp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections] : CategoryTheory.Limits.IsLimit (AddGrp.limitCone F)

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

Equations

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

noncomputable def Grp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections] : CategoryTheory.Limits.IsLimit (Grp.limitCone F)

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

Equations

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

theorem AddGrp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrp)).sections

A functor F : J ⥤ AddGrp.{u} has a limit iff (F ⋙ forget AddGrp).sections is u-small.

theorem Grp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget Grp)).sections

A functor F : J ⥤ Grp.{u} has a limit iff (F ⋙ forget Grp).sections is u-small.

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

The category of additive groups has all limits.

Equations

• ⋯ = ⋯

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

The category of groups has all limits.

Equations

• ⋯ = ⋯

instance AddGrp.hasLimits : CategoryTheory.Limits.HasLimits AddGrp

Equations

• AddGrp.hasLimits = ⋯

instance Grp.hasLimits : CategoryTheory.Limits.HasLimits Grp

Equations

• Grp.hasLimits = ⋯

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

theorem AddGrp.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 AddGrp}, CategoryTheory.Limits.HasLimit (K.comp (CategoryTheory.forget₂ AddGrp AddMonCat))

theorem AddGrp.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 AddGrp}, Small.{u_1, max u_1 u_2} { x_1 : (j : J) → (K.comp (CategoryTheory.forget AddGrp)).obj j // x_1 ∈ (K.comp (CategoryTheory.forget AddGrp)).sections }

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

Equations

• AddGrp.forget₂MonPreservesLimits = AddGrp.forget₂AddMonPreservesLimitsOfSize

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

Equations

• Grp.forget₂MonPreservesLimits = Grp.forget₂MonPreservesLimitsOfSize

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

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

preserves limits of shape J.

Equations

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

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

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

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

Equations

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

noncomputable instance AddGrp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGrp)

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

• AddGrp.forgetPreservesLimitsOfSize = inferInstance

noncomputable instance Grp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget Grp)

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

• Grp.forgetPreservesLimitsOfSize = inferInstance

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

Equations

• AddGrp.forgetPreservesLimits = AddGrp.forgetPreservesLimitsOfSize

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

Equations

• Grp.forgetPreservesLimits = Grp.forgetPreservesLimitsOfSize

instance AddCommGrp.addCommGroupObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) (j : J) : AddCommGroup ((F.comp (CategoryTheory.forget AddCommGrp)).obj j)

Equations

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

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

Equations

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

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

Equations

• AddCommGrp.limitAddCommGroup F = inferInstanceAs (AddCommGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections))

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

Equations

• CommGrp.limitCommGroup F = inferInstanceAs (CommGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget CommGrp)).sections))

instance AddCommGrp.instReflectsIsomorphismsAddGrpForget₂ : (CategoryTheory.forget₂ AddCommGrp AddGrp).ReflectsIsomorphisms

Equations

• AddCommGrp.instReflectsIsomorphismsAddGrpForget₂ = ⋯

instance CommGrp.instReflectsIsomorphismsGrpForget₂ : (CategoryTheory.forget₂ CommGrp Grp).ReflectsIsomorphisms

Equations

• CommGrp.instReflectsIsomorphismsGrpForget₂ = ⋯

theorem AddCommGrp.Forget₂.createsLimit.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))

theorem AddCommGrp.Forget₂.createsLimit.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J AddCommGrp) (this : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))) : Small.{u_1, max u_1 u_2} ↑((F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)).comp (CategoryTheory.forget AddGrp)).sections

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

theorem AddCommGrp.Forget₂.createsLimit.proof_3 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddCommGrp) (this : Small.{u_3, max u_3 u_2} ↑((F.comp ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat))).comp (CategoryTheory.forget AddMonCat)).sections) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj (AddMonCat.HasLimits.limitCone (F.comp ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat)))).pt).map f) ((AddMonCat.HasLimits.limitCone (F.comp ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat)))).π.app Y) = CategoryTheory.CategoryStruct.comp ((AddMonCat.HasLimits.limitCone (F.comp ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat)))).π.app X) ((F.comp ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat))).map f)

theorem AddCommGrp.Forget₂.createsLimit.proof_4 : ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat)).Faithful

noncomputable instance AddCommGrp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommGrp AddGrp)

We show that the forgetful functor AddCommGrp ⥤ AddGrp 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.

noncomputable instance CommGrp.Forget₂.createsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommGrp Grp)

We show that the forgetful functor CommGrp ⥤ Grp 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 AddCommGrp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.Cone F

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

Equations

• AddCommGrp.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)))

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

noncomputable def CommGrp.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.Cone F

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

Equations

• CommGrp.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrp Grp)))

noncomputable def AddCommGrp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.IsLimit (AddCommGrp.limitCone F)

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

Equations

• AddCommGrp.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)))

noncomputable def CommGrp.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.IsLimit (CommGrp.limitCone F)

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

Equations

• CommGrp.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrp Grp)))

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

theorem AddCommGrp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections

A functor F : J ⥤ AddCommGrp.{u} has a limit iff (F ⋙ forget AddCommGrp).sections is u-small.

theorem CommGrp.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections

A functor F : J ⥤ CommGrp.{u} has a limit iff (F ⋙ forget CommGrp).sections is u-small.

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

The category of additive commutative groups has all limits.

Equations

• ⋯ = ⋯

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

The category of commutative groups has all limits.

Equations

• ⋯ = ⋯

instance AddCommGrp.hasLimits : CategoryTheory.Limits.HasLimits AddCommGrp

Equations

• AddCommGrp.hasLimits = ⋯

instance CommGrp.hasLimits : CategoryTheory.Limits.HasLimits CommGrp

Equations

• CommGrp.hasLimits = ⋯

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ AddCommGrp AddGrp)

Equations

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

theorem AddCommGrp.forget₂AddGroupPreservesLimit.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddCommGrp) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))

noncomputable instance CommGrp.forget₂GroupPreservesLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ CommGrp Grp)

Equations

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

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ AddCommGrp AddGrp)

Equations

• AddCommGrp.forget₂AddGroupPreservesLimitsOfShape = { preservesLimit := fun {K : CategoryTheory.Functor J AddCommGrp} => inferInstance }

noncomputable instance CommGrp.forget₂GroupPreservesLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ CommGrp Grp)

Equations

• CommGrp.forget₂GroupPreservesLimitsOfShape = { preservesLimit := fun {K : CategoryTheory.Functor J CommGrp} => inferInstance }

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGrp AddGrp)

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

Equations

• AddCommGrp.forget₂AddGroupPreservesLimitsOfSize = { preservesLimitsOfShape := fun {J : Type ?u.10} [CategoryTheory.Category.{?u.8, ?u.10} J] => inferInstance }

noncomputable instance CommGrp.forget₂GroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrp Grp)

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

• CommGrp.forget₂GroupPreservesLimitsOfSize = { preservesLimitsOfShape := fun {J : Type ?u.10} [CategoryTheory.Category.{?u.8, ?u.10} J] => inferInstance }

noncomputable instance AddCommGrp.forget₂AddGroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddCommGrp AddGrp)

Equations

• AddCommGrp.forget₂AddGroupPreservesLimits = AddCommGrp.forget₂AddGroupPreservesLimitsOfSize

noncomputable instance CommGrp.forget₂GroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommGrp Grp)

Equations

• CommGrp.forget₂GroupPreservesLimits = CommGrp.forget₂GroupPreservesLimitsOfSize

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

noncomputable def AddCommGrp.forget₂AddCommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ AddCommGrp AddCommMonCat).mapCone (AddCommGrp.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• AddCommGrp.forget₂AddCommMonPreservesLimitsAux F = AddCommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommGrp AddCommMonCat))

noncomputable def CommGrp.forget₂CommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrp) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrp)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommGrp CommMonCat).mapCone (CommGrp.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• CommGrp.forget₂CommMonPreservesLimitsAux F = CommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommGrp CommMonCat))

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

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

Equations

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

theorem AddCommGrp.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 AddCommGrp} : Small.{u_1, max u_1 u_2} { x : (j : J) → (F.comp (CategoryTheory.forget AddCommGrp)).obj j // x ∈ (F.comp (CategoryTheory.forget AddCommGrp)).sections }

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

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

Equations

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

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

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

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

preserves limits of shape J.

Equations

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

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

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

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

Equations

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

noncomputable instance AddCommGrp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGrp)

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

• AddCommGrp.forgetPreservesLimitsOfSize = inferInstance

noncomputable instance CommGrp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGrp)

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

• CommGrp.forgetPreservesLimitsOfSize = inferInstance

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

Equations

• AddCommGrp.forgetPreservesLimits = AddCommGrp.forgetPreservesLimitsOfSize

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

Equations

• CommGrp.forgetPreservesLimits = CommGrp.forgetPreservesLimitsOfSize

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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