MonCat.FilteredColimits.colimit_mul_mk_eq
theorem MonCat.FilteredColimits.colimit_mul_mk_eq :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] (x 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⟩
This theorem states that within the context of a filtered category, the multiplication operation in the colimit is independent of the chosen "maximum" object in the category. More specifically, it demonstrates that one can "unfold" the multiplication operation between two objects `x` and `y`, using a custom object `k` and morphisms `f : x.fst ⟶ k` and `g : y.fst ⟶ k`. The theorem asserts that the multiplication of `x` and `y` in the colimit, where `x` and `y` are objects mapped into the Monoidal Category (`MonCatMax`) by a functor `F`, is equal to the projection into the colimit of `k` and the product of the images of `x` and `y` under `F` mapped by morphisms `f` and `g`, respectively.
More concisely: In a filtered category, the multiplication of objects in the colimit of a functor to a monoidal category is equal to the projection into the colimit of their common image and the product of their images under the functor.
|
MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left
theorem MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] {x x' y : (j : J) × ↑(F.obj j)},
CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) x x' →
MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x' y
The theorem `MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left` states that in the category of monoids (`MonCat`), if we have a filtered colimit of some functor `F`, and two elements `x` and `x'` from the same object `j` in the index category `J` that are related under the type of relations that define the colimit, then the result of the colimit multiplication operation on `x` and any other element `y` is the same as the result of the colimit multiplication operation on `x'` and `y`. Here, multiplication in the colimit is deemed well-defined in the left argument.
More concisely: In the category of monoids, if `x` and `x'` are related elements from the same object in an index category for a filtered colimit, then the result of the colimit multiplication of `x` with any element is equal to the result of the colimit multiplication of `x'` with that same element.
|
AddMonCat.FilteredColimits.colimit_zero_eq
theorem AddMonCat.FilteredColimits.colimit_zero_eq :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] (j : J), 0 = AddMonCat.FilteredColimits.M.mk F ⟨j, 0⟩
This theorem states that the definition of the "zero" element in the colimit of a functor `F` from a small category `J` to `AddMonCatMax` is independent of the chosen object of `J`. In other words, for any object `j` in `J`, the "zero" element in the colimit is equal to the canonical projection into the colimit at the tuple consisting of `j` and the "zero" element in the monoid of `F.obj j`. This theorem is significant because it allows us to "unfold" the definition of `colimit_zero` at a custom chosen object `j`. The small category `J` is assumed to be filtered.
More concisely: The zero element in the colimit of a functor from a filtered small category to AddMonCatMax is equal to the canonical projection of the zero element in the monoid of any object into the colimit.
|
MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right
theorem MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] {x y y' : (j : J) × ↑(F.obj j)},
CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) y y' →
MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x y'
The theorem `MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right` asserts that for a given small category `J`, a functor `F` from `J` to `MonCatMax` (the category of monoids and monoid morphisms), and filtered colimit condition on `J`, if two objects `y` and `y'` from `J` are related by the `FilteredColimit.Rel` relation of the functor `F` composed with the forgetful functor, then the result of the auxiliary multiplication function `colimitMulAux` applied to `x` and `y` is equal to the result of the same function applied to `x` and `y'`. This implies that the multiplication operation is well-defined in the right argument in the colimit of the category `MonCat`.
More concisely: For any small category J, functor F from J to MonCatMax preserving filtered colimits, and related objects y and y' in J via the FilteredColimits.Rel relation of F, the auxiliary multiplication function colimitMulAux(F x y) equals colimitMulAux(F x y').
|
AddMonCat.FilteredColimits.colimit_add_mk_eq
theorem AddMonCat.FilteredColimits.colimit_add_mk_eq :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] (x 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⟩
This theorem, `AddMonCat.FilteredColimits.colimit_add_mk_eq`, states that in the context of a small category `J` and a functor `F` mapping `J` to `AddMonCatMax`, addition in the colimit is independent of the chosen "maximum" in the filtered category. In other words, for any objects `x` and `y` in the category `J`, and a custom object `k` in `J` along with morphisms `f` from `x` to `k` and `g` from `y` to `k`, the sum of the images of `x` and `y` under the canonical projection into the colimit is equal to the image under the same projection of the object in `J` obtained by mapping the sum of `x` and `y` through the morphisms `f` and `g` to `k`. It's an important property of the category of additive monoids, which ensures that the addition operation is well-defined in the filtered colimit.
More concisely: In the category of AddMonCatMax, the sum of images of objects under canonical projections into a filtered colimit is equal to the image of their sum through given morphisms.
|
AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_left
theorem AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_left :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] {x x' y : (j : J) × ↑(F.obj j)},
CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) x x' →
AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x' y
This theorem, titled "Addition in the colimit is well-defined in the left argument", states that for any small category `J`, if `F` is a functor from `J` to the category of additive monoids with maximum type, and `J` has the property of being filtered, then for any three objects `x`, `x'`, and `y` in the category `J` lifted to the objects of `F`, if there exists a relationship in the filtered colimit of `F` after applying the forgetful functor to the category of additive monoids between `x` and `x'`, then the sum of `x` and `y` in the colimit of `F` equals the sum of `x'` and `y` in the colimit of `F`. In other words, the operation of addition in the colimit of a functor to the category of additive monoids is well-defined on the left argument, under the condition of a certain relationship in the filtered colimit.
More concisely: For any small filtered category `J`, functor `F` from `J` to the category of additive monoids preserving sums, and objects `x`, `x'`, and `y` in `J`, if the sum of `x` and `y` equals the sum of `x'` and `y` in the filtered colimit of `F`, then the sums are interchangeable in the colimit of `F`.
|
MonCat.FilteredColimits.colimit_one_eq
theorem MonCat.FilteredColimits.colimit_one_eq :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] (j : J), 1 = MonCat.FilteredColimits.M.mk F ⟨j, 1⟩
The theorem `MonCat.FilteredColimits.colimit_one_eq` states that within the context of a Small Category `J` and a functor `F` from `J` to `MonCatMax`, the definition of the "one" in the colimit is independent of the chosen object of `J`. In other words, for any object `j` from `J`, the "one" element is equal to the "one" element at the object `j` when it is projected into the colimit. This theorem allows us to "unfold" or expand the definition of `colimit_one` at a custom chosen object `j` in the Category `J`.
More concisely: For any Small Category `J`, functor `F` from `J` to `MonCatMax`, and objects `j` in `J`, the "one" element in the colimit of `F` is equal to the "one" element at object `j` when projected into the colimit.
|
AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right
theorem AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right :
∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax)
[inst_1 : CategoryTheory.IsFiltered J] {x y y' : (j : J) × ↑(F.obj j)},
CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) y y' →
AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x y'
The theorem `AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right` asserts that for any small category `J` and any functor `F` from `J` to the category of additive monoids, if `y` and `y'` are related in the filtered colimit of `F` composed with the forgetful functor from `AddMonCat` to `Type`, then the addition at the colimit of `F` for any element `x` and the elements `y` and `y'` are equal. This guarantees that the addition operation in the colimit of an additive monoid is well-defined for the right argument, which is a crucial requirement for the colimit to be an additive monoid itself.
More concisely: Given a small category `J`, a functor `F` from `J` to additive monoids, and related elements `y` and `y'` in the filtered colimit of `F` in `AddMonCat`, the addition at the colimit of `F` of any element `x` with `y` is equal to the addition at the colimit of `F` of `x` with `y'`.
|