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

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

abbrev AddMonCatMax : Type ((max u1 u2) + 1)

An alias for AddMonCat.{max u v}, to deal around unification issues.

Equations

• AddMonCatMax = AddMonCat

@[reducible, inline]

abbrev MonCatMax : Type ((max u1 u2) + 1)

An alias for MonCat.{max u v}, to deal around unification issues.

Equations

• MonCatMax = MonCat

instance AddMonCat.addMonoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) (j : J) : AddMonoid ((F.comp (CategoryTheory.forget AddMonCat)).obj j)

Equations

• AddMonCat.addMonoidObj F j = inferInstanceAs (AddMonoid ↑(F.obj j))

instance MonCat.monoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) (j : J) : Monoid ((F.comp (CategoryTheory.forget MonCat)).obj j)

Equations

• MonCat.monoidObj F j = inferInstanceAs (Monoid ↑(F.obj j))

theorem AddMonCat.sectionsAddSubmonoid.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddMonCat) {j : J} {j' : J} (f : j ⟶ j') : (F.map f) 0 = 0

def AddMonCat.sectionsAddSubmonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) : AddSubmonoid ((j : J) → ↑(F.obj j))

The flat sections of a functor into AddMonCat form an additive submonoid of all sections.

Equations

• AddMonCat.sectionsAddSubmonoid F = { carrier := (F.comp (CategoryTheory.forget AddMonCat)).sections, add_mem' := ⋯, zero_mem' := ⋯ }

theorem AddMonCat.sectionsAddSubmonoid.proof_1 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddMonCat) {a : (j : J) → ↑(F.obj j)} {b : (j : J) → ↑(F.obj j)} (ah : a ∈ (F.comp (CategoryTheory.forget AddMonCat)).sections) (bh : b ∈ (F.comp (CategoryTheory.forget AddMonCat)).sections) {j : J} {j' : J} (f : j ⟶ j') : (F.comp (CategoryTheory.forget AddMonCat)).map f ((a + b) j) = (a + b) j'

def MonCat.sectionsSubmonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) : Submonoid ((j : J) → ↑(F.obj j))

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

Equations

• MonCat.sectionsSubmonoid F = { carrier := (F.comp (CategoryTheory.forget MonCat)).sections, mul_mem' := ⋯, one_mem' := ⋯ }

instance AddMonCat.sectionsAddMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) : AddMonoid ↑(F.comp (CategoryTheory.forget AddMonCat)).sections

Equations

• AddMonCat.sectionsAddMonoid F = (AddMonCat.sectionsAddSubmonoid F).toAddMonoid

instance MonCat.sectionsMonoid {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) : Monoid ↑(F.comp (CategoryTheory.forget MonCat)).sections

Equations

• MonCat.sectionsMonoid F = (MonCat.sectionsSubmonoid F).toMonoid

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

Equations

• AddMonCat.limitAddMonoid F = inferInstanceAs (AddMonoid (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections))

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

Equations

• MonCat.limitMonoid F = inferInstanceAs (Monoid (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget MonCat)).sections))

theorem AddMonCat.limitπAddMonoidHom.proof_2 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_2, max u_2 u_3} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J) : ∀ (x x_1 : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt), { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j, map_zero' := ⋯ }.toFun x + { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j, map_zero' := ⋯ }.toFun x_1

theorem AddMonCat.limitπAddMonoidHom.proof_1 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_1, max u_1 u_3} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j 0 = 0

noncomputable def AddMonCat.limitπAddMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt →+ (F.comp (CategoryTheory.forget AddMonCat)).obj j

limit.π (F ⋙ forget AddMonCat) j as an AddMonoidHom.

Equations

• AddMonCat.limitπAddMonoidHom F j = { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def MonCat.limitπMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt →* (F.comp (CategoryTheory.forget MonCat)).obj j

limit.π (F ⋙ forget MonCat) j as a MonoidHom.

Equations

• MonCat.limitπMonoidHom F j = { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).π.app j, map_one' := ⋯, map_mul' := ⋯ }

theorem AddMonCat.HasLimits.limitCone.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_3, max u_3 u_2} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : ∀ (x x_1 : J) (f : x ⟶ x_1), CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj (AddMonCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt)).map f) (AddMonCat.limitπAddMonoidHom F x_1) = CategoryTheory.CategoryStruct.comp (AddMonCat.limitπAddMonoidHom F x) (F.map f)

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

(Internal use only; use the limits API.)

Equations

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

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

Construction of a limit cone in MonCat. (Internal use only; use the limits API.)

Equations

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

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_2 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_1, max u_1 u_3} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (s : CategoryTheory.Limits.Cone F) : (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).1 ⟨fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).π.app j 0, ⋯⟩ = 0

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_4 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_2, max u_2 u_3} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.forget AddMonCat).map ((fun (s : CategoryTheory.Limits.Cone F) => { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).1 ⟨fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).π.app j v, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }) s) = (CategoryTheory.forget AddMonCat).map ((fun (s : CategoryTheory.Limits.Cone F) => { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).1 ⟨fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).π.app j v, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }) s)

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_3 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_1, max u_1 u_3} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (s : CategoryTheory.Limits.Cone F) (x : ↑s.pt) (y : ↑s.pt) : { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).1 ⟨fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).π.app j v, ⋯⟩, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).1 ⟨fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).π.app j v, ⋯⟩, map_zero' := ⋯ }.toFun x + { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).1 ⟨fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).π.app j v, ⋯⟩, map_zero' := ⋯ }.toFun y

theorem AddMonCat.HasLimits.limitConeIsLimit.proof_1 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddMonCat) (s : CategoryTheory.Limits.Cone F) (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (((CategoryTheory.forget AddMonCat).mapCone s).π.app j) ((F.comp (CategoryTheory.forget AddMonCat)).map f) v = ((CategoryTheory.forget AddMonCat).mapCone s).π.app j' v

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

(Internal use only; use the limits API.)

Equations

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

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

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

Equations

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

The category of additive monoids has all limits.

Equations

• ⋯ = ⋯

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

The category of monoids has all limits.

Equations

• ⋯ = ⋯

instance AddMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddMonCat

Equations

• AddMonCat.hasLimits = ⋯

instance MonCat.hasLimits : CategoryTheory.Limits.HasLimits MonCat

Equations

• MonCat.hasLimits = ⋯

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

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

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

preserves limits of shape J.

Equations

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

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

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

Equations

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

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

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

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

Equations

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

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

The forgetful functor from monoids to types preserves all limits.

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

Equations

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

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

Equations

• AddMonCat.forgetPreservesLimits = AddMonCat.forgetPreservesLimitsOfSize

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

Equations

• MonCat.forgetPreservesLimits = MonCat.forgetPreservesLimitsOfSize

abbrev AddCommMonCatMax : Type ((max u1 u2) + 1)

An alias for AddCommMonCat.{max u v}, to deal around unification issues.

Equations

• AddCommMonCatMax = AddCommMonCat

@[reducible, inline]

abbrev CommMonCatMax : Type ((max u1 u2) + 1)

An alias for CommMonCat.{max u v}, to deal around unification issues.

Equations

• CommMonCatMax = CommMonCat

instance AddCommMonCat.addCommMonoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) (j : J) : AddCommMonoid ((F.comp (CategoryTheory.forget AddCommMonCat)).obj j)

Equations

• AddCommMonCat.addCommMonoidObj F j = inferInstanceAs (AddCommMonoid ↑(F.obj j))

instance CommMonCat.commMonoidObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) (j : J) : CommMonoid ((F.comp (CategoryTheory.forget CommMonCat)).obj j)

Equations

• CommMonCat.commMonoidObj F j = inferInstanceAs (CommMonoid ↑(F.obj j))

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

Equations

• AddCommMonCat.limitAddCommMonoid F = inferInstanceAs (AddCommMonoid (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections))

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

Equations

• CommMonCat.limitCommMonoid F = inferInstanceAs (CommMonoid (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

All we need to do is notice that the limit point has an AddCommMonoid instance available,

and then reuse the existing limit.

Equations

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

theorem AddCommMonCat.forget₂CreatesLimit.proof_1 : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).ReflectsIsomorphisms

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

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

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

The category of additive commutative monoids has all limits.

Equations

• ⋯ = ⋯

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

The category of commutative monoids has all limits.

Equations

• ⋯ = ⋯

instance AddCommMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommMonCat

Equations

• AddCommMonCat.hasLimits = ⋯

instance CommMonCat.hasLimits : CategoryTheory.Limits.HasLimits CommMonCat

Equations

• CommMonCat.hasLimits = ⋯

noncomputable instance AddCommMonCat.forget₂AddMonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

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

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

monoids.

Equations

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

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

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

noncomputable instance CommMonCat.forget₂MonPreservesLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommMonCat MonCat)

The forgetful functor from commutative monoids to monoids preserves all limits.

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

Equations

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

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

Equations

• AddCommMonCat.forget₂MonPreservesLimits = AddCommMonCat.forget₂AddMonPreservesLimitsOfSize

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

Equations

• CommMonCat.forget₂MonPreservesLimits = CommMonCat.forget₂MonPreservesLimitsOfSize

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

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

preserves limits of shape J.

Equations

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

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

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

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

Equations

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

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

The forgetful functor from additive commutative monoids to types preserves all

limits.

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

Equations

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

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

The forgetful functor from commutative monoids to types preserves all limits.

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

Equations

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

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

Equations

• AddCommMonCat.forgetPreservesLimits = AddCommMonCat.forgetPreservesLimitsOfSize

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

Equations

• CommMonCat.forgetPreservesLimits = CommMonCat.forgetPreservesLimitsOfSize