The forgetful functor from (commutative) (additive) monoids preserves filtered colimits.

Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.

In this file, we start with a small filtered category J and a functor F : J ⥤ MonCat. We then construct a monoid structure on the colimit of F ⋙ forget MonCat (in Type), thereby showing that the forgetful functor forget MonCat preserves filtered colimits. Similarly for AddMonCat, CommMonCat and AddCommMonCat.

@[reducible, inline]

abbrev AddMonCat.FilteredColimits.M {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : Type (max u v)

The colimit of F ⋙ forget AddMon in the category of types. In the following, we will construct an additive monoid structure on M.

Equations

• AddMonCat.FilteredColimits.M F = CategoryTheory.Limits.Types.Quot (F.comp (CategoryTheory.forget AddMonCat))

@[reducible, inline]

abbrev MonCat.FilteredColimits.M {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) : Type (max u v)

The colimit of F ⋙ forget MonCat in the category of types. In the following, we will construct a monoid structure on M.

Equations

• MonCat.FilteredColimits.M F = CategoryTheory.Limits.Types.Quot (F.comp (CategoryTheory.forget MonCat))

@[reducible, inline]

noncomputable abbrev AddMonCat.FilteredColimits.M.mk {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) : (j : J) × ↑(F.obj j) → AddMonCat.FilteredColimits.M F

The canonical projection into the colimit, as a quotient type.

Equations

• AddMonCat.FilteredColimits.M.mk F = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.forget AddMonCat)))

@[reducible, inline]

noncomputable abbrev MonCat.FilteredColimits.M.mk {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) : (j : J) × ↑(F.obj j) → MonCat.FilteredColimits.M F

The canonical projection into the colimit, as a quotient type.

Equations

• MonCat.FilteredColimits.M.mk F = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.forget MonCat)))

theorem AddMonCat.FilteredColimits.M.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : ∃ (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k), (F.map f) x.snd = (F.map g) y.snd) : AddMonCat.FilteredColimits.M.mk F x = AddMonCat.FilteredColimits.M.mk F y

theorem MonCat.FilteredColimits.M.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : ∃ (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k), (F.map f) x.snd = (F.map g) y.snd) : MonCat.FilteredColimits.M.mk F x = MonCat.FilteredColimits.M.mk F y

noncomputable instance AddMonCat.FilteredColimits.colimitZero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : Zero (AddMonCat.FilteredColimits.M F)

As J is nonempty, we can pick an arbitrary object j₀ : J. We use this object to define the "zero" in the colimit as the equivalence class of ⟨j₀, 0 : F.obj j₀⟩.

Equations

• AddMonCat.FilteredColimits.colimitZero F = { zero := AddMonCat.FilteredColimits.M.mk F ⟨⋯.some, 0⟩ }

noncomputable instance MonCat.FilteredColimits.colimitOne {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : One (MonCat.FilteredColimits.M F)

As J is nonempty, we can pick an arbitrary object j₀ : J. We use this object to define the "one" in the colimit as the equivalence class of ⟨j₀, 1 : F.obj j₀⟩.

Equations

• MonCat.FilteredColimits.colimitOne F = { one := MonCat.FilteredColimits.M.mk F ⟨⋯.some, 1⟩ }

theorem AddMonCat.FilteredColimits.colimit_zero_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (j : J) : 0 = AddMonCat.FilteredColimits.M.mk F ⟨j, 0⟩

The definition of the "zero" in the colimit is independent of the chosen object of J. In particular, this lemma allows us to "unfold" the definition of colimit_zero at a custom chosen object j.

theorem MonCat.FilteredColimits.colimit_one_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (j : J) : 1 = MonCat.FilteredColimits.M.mk F ⟨j, 1⟩

The definition of the "one" in the colimit is independent of the chosen object of J. In particular, this lemma allows us to "unfold" the definition of colimit_one at a custom chosen object j.

noncomputable def AddMonCat.FilteredColimits.colimitAddAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) : AddMonCat.FilteredColimits.M F

The "unlifted" version of addition in the colimit. To add two dependent pairs ⟨j₁, x⟩ and ⟨j₂, y⟩, we pass to a common successor of j₁ and j₂ (given by IsFiltered.max) and add them there.

Equations

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

noncomputable def MonCat.FilteredColimits.colimitMulAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) : MonCat.FilteredColimits.M F

The "unlifted" version of multiplication in the colimit. To multiply two dependent pairs ⟨j₁, x⟩ and ⟨j₂, y⟩, we pass to a common successor of j₁ and j₂ (given by IsFiltered.max) and multiply them there.

Equations

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

theorem AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_left {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] {x : (j : J) × ↑(F.obj j)} {x' : (j : J) × ↑(F.obj j)} {y : (j : J) × ↑(F.obj j)} (hxx' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) x x') : AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x' y

Addition in the colimit is well-defined in the left argument.

theorem MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] {x : (j : J) × ↑(F.obj j)} {x' : (j : J) × ↑(F.obj j)} {y : (j : J) × ↑(F.obj j)} (hxx' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) x x') : MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x' y

Multiplication in the colimit is well-defined in the left argument.

theorem AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] {x : (j : J) × ↑(F.obj j)} {y : (j : J) × ↑(F.obj j)} {y' : (j : J) × ↑(F.obj j)} (hyy' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) y y') : AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x y'

Addition in the colimit is well-defined in the right argument.

theorem MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] {x : (j : J) × ↑(F.obj j)} {y : (j : J) × ↑(F.obj j)} {y' : (j : J) × ↑(F.obj j)} (hyy' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) y y') : MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x y'

Multiplication in the colimit is well-defined in the right argument.

theorem AddMonCat.FilteredColimits.colimitAdd.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (y' : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.forget AddMonCat)) y y') : AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x y'

noncomputable instance AddMonCat.FilteredColimits.colimitAdd {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : Add (AddMonCat.FilteredColimits.M F)

Addition in the colimit. See also colimitAddAux.

Equations

• AddMonCat.FilteredColimits.colimitAdd F = { add := fun (x y : AddMonCat.FilteredColimits.M F) => Quot.lift₂ (AddMonCat.FilteredColimits.colimitAddAux F) ⋯ ⋯ x y }

theorem AddMonCat.FilteredColimits.colimitAdd.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × ↑(F.obj j)) (x' : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.forget AddMonCat)) x x') : AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x' y

noncomputable instance MonCat.FilteredColimits.colimitMul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : Mul (MonCat.FilteredColimits.M F)

Multiplication in the colimit. See also colimitMulAux.

Equations

• MonCat.FilteredColimits.colimitMul F = { mul := fun (x y : MonCat.FilteredColimits.M F) => Quot.lift₂ (MonCat.FilteredColimits.colimitMulAux F) ⋯ ⋯ x y }

theorem AddMonCat.FilteredColimits.colimit_add_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k) : AddMonCat.FilteredColimits.M.mk F x + AddMonCat.FilteredColimits.M.mk F y = AddMonCat.FilteredColimits.M.mk F ⟨k, (F.map f) x.snd + (F.map g) y.snd⟩

Addition in the colimit is independent of the chosen "maximum" in the filtered category. In particular, this lemma allows us to "unfold" the definition of the addition of x and y, using a custom object k and morphisms f : x.1 ⟶ k and g : y.1 ⟶ k.

theorem MonCat.FilteredColimits.colimit_mul_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k) : MonCat.FilteredColimits.M.mk F x * MonCat.FilteredColimits.M.mk F y = MonCat.FilteredColimits.M.mk F ⟨k, (F.map f) x.snd * (F.map g) y.snd⟩

Multiplication in the colimit is independent of the chosen "maximum" in the filtered category. In particular, this lemma allows us to "unfold" the definition of the multiplication of x and y, using a custom object k and morphisms f : x.1 ⟶ k and g : y.1 ⟶ k.

theorem AddMonCat.FilteredColimits.colimitAddZeroClass.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : AddMonCat.FilteredColimits.M F) : 0 + x = x

noncomputable instance AddMonCat.FilteredColimits.colimitAddZeroClass {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : AddZeroClass (AddMonCat.FilteredColimits.M F)

Equations

• AddMonCat.FilteredColimits.colimitAddZeroClass F = AddZeroClass.mk ⋯ ⋯

theorem AddMonCat.FilteredColimits.colimitAddZeroClass.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : AddMonCat.FilteredColimits.M F) : x + 0 = x

noncomputable instance MonCat.FilteredColimits.colimitMulOneClass {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : MulOneClass (MonCat.FilteredColimits.M F)

Equations

• MonCat.FilteredColimits.colimitMulOneClass F = MulOneClass.mk ⋯ ⋯

theorem AddMonCat.FilteredColimits.colimitAddMonoid.proof_4 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : ∀ (x : AddMonCat.FilteredColimits.M F), nsmulRec 0 x = nsmulRec 0 x

theorem AddMonCat.FilteredColimits.colimitAddMonoid.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (a : AddMonCat.FilteredColimits.M F) : 0 + a = a

noncomputable instance AddMonCat.FilteredColimits.colimitAddMonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : AddMonoid (AddMonCat.FilteredColimits.M F)

Equations

• AddMonCat.FilteredColimits.colimitAddMonoid F = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

theorem AddMonCat.FilteredColimits.colimitAddMonoid.proof_5 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : ∀ (n : ℕ) (x : AddMonCat.FilteredColimits.M F), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem AddMonCat.FilteredColimits.colimitAddMonoid.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : AddMonCat.FilteredColimits.M F) (y : AddMonCat.FilteredColimits.M F) (z : AddMonCat.FilteredColimits.M F) : x + y + z = x + (y + z)

theorem AddMonCat.FilteredColimits.colimitAddMonoid.proof_3 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (a : AddMonCat.FilteredColimits.M F) : a + 0 = a

noncomputable instance MonCat.FilteredColimits.colimitMonoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : Monoid (MonCat.FilteredColimits.M F)

Equations

• MonCat.FilteredColimits.colimitMonoid F = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

noncomputable def AddMonCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : AddMonCat

The bundled additive monoid giving the filtered colimit of a diagram.

Equations

• AddMonCat.FilteredColimits.colimit F = AddMonCat.of (AddMonCat.FilteredColimits.M F)

noncomputable def MonCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : MonCat

The bundled monoid giving the filtered colimit of a diagram.

Equations

• MonCat.FilteredColimits.colimit F = MonCat.of (MonCat.FilteredColimits.M F)

theorem AddMonCat.FilteredColimits.coconeMorphism.proof_2 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (j : J) (x : ↑(F.obj j)) (y : ↑(F.obj j)) : { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).ι.app j, map_zero' := ⋯ }.toFun (x + y) = { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).ι.app j, map_zero' := ⋯ }.toFun x + { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).ι.app j, map_zero' := ⋯ }.toFun y

def AddMonCat.FilteredColimits.coconeMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (j : J) : F.obj j ⟶ AddMonCat.FilteredColimits.colimit F

The additive monoid homomorphism from a given additive monoid in the diagram to the colimit additive monoid.

Equations

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

theorem AddMonCat.FilteredColimits.coconeMorphism.proof_1 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (j : J) : AddMonCat.FilteredColimits.M.mk F ⟨j, 0⟩ = 0

def MonCat.FilteredColimits.coconeMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (j : J) : F.obj j ⟶ MonCat.FilteredColimits.colimit F

The monoid homomorphism from a given monoid in the diagram to the colimit monoid.

Equations

• MonCat.FilteredColimits.coconeMorphism F j = { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget MonCat))).ι.app j, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddMonCat.FilteredColimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] {j : J} {j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (F.map f) (AddMonCat.FilteredColimits.coconeMorphism F j') = AddMonCat.FilteredColimits.coconeMorphism F j

@[simp]

theorem MonCat.FilteredColimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] {j : J} {j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (F.map f) (MonCat.FilteredColimits.coconeMorphism F j') = MonCat.FilteredColimits.coconeMorphism F j

theorem AddMonCat.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map f) (AddMonCat.FilteredColimits.coconeMorphism F Y) = CategoryTheory.CategoryStruct.comp (AddMonCat.FilteredColimits.coconeMorphism F X) (CategoryTheory.CategoryStruct.id (AddMonCat.FilteredColimits.colimit F))

noncomputable def AddMonCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit additive monoid.

Equations

• AddMonCat.FilteredColimits.colimitCocone F = { pt := AddMonCat.FilteredColimits.colimit F, ι := { app := AddMonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }

noncomputable def MonCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit monoid.

Equations

• MonCat.FilteredColimits.colimitCocone F = { pt := MonCat.FilteredColimits.colimit F, ι := { app := MonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }

theorem AddMonCat.FilteredColimits.colimitDesc.proof_2 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) (x : ↑(AddMonCat.FilteredColimits.colimit F)) (y : ↑(AddMonCat.FilteredColimits.colimit F)) : { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit (F.comp (CategoryTheory.forget AddMonCat))).desc ((CategoryTheory.forget AddMonCat).mapCocone t), map_zero' := ⋯ }.toFun (x + y) = { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit (F.comp (CategoryTheory.forget AddMonCat))).desc ((CategoryTheory.forget AddMonCat).mapCocone t), map_zero' := ⋯ }.toFun x + { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit (F.comp (CategoryTheory.forget AddMonCat))).desc ((CategoryTheory.forget AddMonCat).mapCocone t), map_zero' := ⋯ }.toFun y

def AddMonCat.FilteredColimits.colimitDesc {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) : AddMonCat.FilteredColimits.colimit F ⟶ t.pt

Given a cocone t of F, the induced additive monoid homomorphism from the colimit to the cocone point. As a function, this is simply given by the induced map of the corresponding cocone in Type. The only thing left to see is that it is an additive monoid homomorphism.

Equations

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

theorem AddMonCat.FilteredColimits.colimitDesc.proof_1 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit (F.comp (CategoryTheory.forget AddMonCat))).desc ((CategoryTheory.forget AddMonCat).mapCocone t) 0 = 0

def MonCat.FilteredColimits.colimitDesc {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) : MonCat.FilteredColimits.colimit F ⟶ t.pt

Given a cocone t of F, the induced monoid homomorphism from the colimit to the cocone point. As a function, this is simply given by the induced map of the corresponding cocone in Type. The only thing left to see is that it is a monoid homomorphism.

Equations

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

theorem AddMonCat.FilteredColimits.colimitCoconeIsColimit.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) (m : (AddMonCat.FilteredColimits.colimitCocone F).pt ⟶ t.pt) (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp ((AddMonCat.FilteredColimits.colimitCocone F).ι.app j) m = t.ι.app j) : m = AddMonCat.FilteredColimits.colimitDesc F t

theorem AddMonCat.FilteredColimits.colimitCoconeIsColimit.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) (j : J) : CategoryTheory.CategoryStruct.comp ((AddMonCat.FilteredColimits.colimitCocone F).ι.app j) (AddMonCat.FilteredColimits.colimitDesc F t) = t.ι.app j

def AddMonCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.IsColimit (AddMonCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in AddMonCat.

Equations

• AddMonCat.FilteredColimits.colimitCoconeIsColimit F = { desc := AddMonCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }

def MonCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.IsColimit (MonCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in MonCat.

Equations

• MonCat.FilteredColimits.colimitCoconeIsColimit F = { desc := MonCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }

noncomputable instance AddMonCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddMonCat)

Equations

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

noncomputable instance MonCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget MonCat)

Equations

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

@[reducible, inline]

noncomputable abbrev AddCommMonCat.FilteredColimits.M {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) : AddMonCat

The colimit of F ⋙ forget₂ AddCommMonCat AddMonCat in the category AddMonCat. In the following, we will show that this has the structure of a commutative additive monoid.

Equations

• AddCommMonCat.FilteredColimits.M F = AddMonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))

@[reducible, inline]

noncomputable abbrev CommMonCat.FilteredColimits.M {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommMonCat) : MonCat

The colimit of F ⋙ forget₂ CommMonCat MonCat in the category MonCat. In the following, we will show that this has the structure of a commutative monoid.

Equations

• CommMonCat.FilteredColimits.M F = MonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))

noncomputable instance AddCommMonCat.FilteredColimits.colimitAddCommMonoid {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M F)

Equations

• AddCommMonCat.FilteredColimits.colimitAddCommMonoid F = AddCommMonoid.mk ⋯

theorem AddCommMonCat.FilteredColimits.colimitAddCommMonoid.proof_1 {J : Type u_2} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) (x : ↑(AddCommMonCat.FilteredColimits.M F)) (y : ↑(AddCommMonCat.FilteredColimits.M F)) : x + y = y + x

noncomputable instance CommMonCat.FilteredColimits.colimitCommMonoid {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommMonCat) : CommMonoid ↑(CommMonCat.FilteredColimits.M F)

Equations

• CommMonCat.FilteredColimits.colimitCommMonoid F = CommMonoid.mk ⋯

noncomputable def AddCommMonCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) : AddCommMonCat

The bundled additive commutative monoid giving the filtered colimit of a diagram.

Equations

• AddCommMonCat.FilteredColimits.colimit F = AddCommMonCat.of ↑(AddCommMonCat.FilteredColimits.M F)

noncomputable def CommMonCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommMonCat) : CommMonCat

The bundled commutative monoid giving the filtered colimit of a diagram.

Equations

• CommMonCat.FilteredColimits.colimit F = CommMonCat.of ↑(CommMonCat.FilteredColimits.M F)

theorem AddCommMonCat.FilteredColimits.colimitCocone.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) ⦃X : J⦄ ⦃Y : J⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).map f) ((AddMonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).ι.app Y) = CategoryTheory.CategoryStruct.comp ((AddMonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).ι.app X) (((CategoryTheory.Functor.const J).obj (AddMonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).pt).map f)

noncomputable def AddCommMonCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit additive commutative monoid.

Equations

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

noncomputable def CommMonCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommMonCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit commutative monoid.

Equations

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

theorem AddCommMonCat.FilteredColimits.colimitCoconeIsColimit.proof_1 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) (t : CategoryTheory.Limits.Cocone F) (j : J) : CategoryTheory.CategoryStruct.comp ((AddCommMonCat.FilteredColimits.colimitCocone F).ι.app j) ((fun (t : CategoryTheory.Limits.Cocone F) => AddMonCat.FilteredColimits.colimitDesc (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCocone t)) t) = t.ι.app j

theorem AddCommMonCat.FilteredColimits.colimitCoconeIsColimit.proof_2 {J : Type u_1} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) (t : CategoryTheory.Limits.Cocone F) (m : (AddCommMonCat.FilteredColimits.colimitCocone F).pt ⟶ t.pt) (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp ((AddCommMonCat.FilteredColimits.colimitCocone F).ι.app j) m = t.ι.app j) : m = (fun (t : CategoryTheory.Limits.Cocone F) => AddMonCat.FilteredColimits.colimitDesc (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCocone t)) t

def AddCommMonCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddCommMonCat) : CategoryTheory.Limits.IsColimit (AddCommMonCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in AddCommMonCat.

Equations

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

def CommMonCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommMonCat) : CategoryTheory.Limits.IsColimit (CommMonCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in CommMonCat.

Equations

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

noncomputable instance AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddCommMonCat AddMonCat)

Equations

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

noncomputable instance CommMonCat.FilteredColimits.forget₂MonPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommMonCat MonCat)

Equations

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

noncomputable instance AddCommMonCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddCommMonCat)

Equations

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

noncomputable instance CommMonCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommMonCat)

Equations

• CommMonCat.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ CommMonCat MonCat) (CategoryTheory.forget MonCat)