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 ⥤ Mon.
We then construct a monoid structure on the colimit of F ⋙ forget Mon (in Type), thereby
showing that the forgetful functor forget Mon preserves filtered colimits. Similarly for AddMon,
CommMon and AddCommMon.
The colimit of F ⋙ forget AddMon in the category of types.
In the following, we will construct an additive monoid structure on M.
The colimit of F ⋙ forget Mon in the category of types.
In the following, we will construct a monoid structure on M.
The canonical projection into the colimit, as a quotient type.
The canonical projection into the colimit, as a quotient type.
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₀⟩.
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₀⟩.
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.
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.
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 is_filtered.max)
and add them there.
Equations
- AddMon.filtered_colimits.colimit_add_aux F x y = AddMon.filtered_colimits.M.mk F ⟨category_theory.is_filtered.max x.fst y.fst, ⇑(F.map (category_theory.is_filtered.left_to_max x.fst y.fst)) x.snd + ⇑(F.map (category_theory.is_filtered.right_to_max x.fst y.fst)) y.snd⟩
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 is_filtered.max)
and multiply them there.
Equations
- Mon.filtered_colimits.colimit_mul_aux F x y = Mon.filtered_colimits.M.mk F ⟨category_theory.is_filtered.max x.fst y.fst, ⇑(F.map (category_theory.is_filtered.left_to_max x.fst y.fst)) x.snd * ⇑(F.map (category_theory.is_filtered.right_to_max x.fst y.fst)) y.snd⟩
Addition in the colimit is well-defined in the left argument.
Multiplication in the colimit is well-defined in the left argument.
Multiplication in the colimit is well-defined in the right argument.
Addition in the colimit is well-defined in the right argument.
Addition in the colimit. See also colimit_add_aux.
Equations
- AddMon.filtered_colimits.colimit_has_add F = {add := λ (x y : AddMon.filtered_colimits.M F), quot.lift₂ (AddMon.filtered_colimits.colimit_add_aux F) _ _ x y}
Multiplication in the colimit. See also colimit_mul_aux.
Equations
- Mon.filtered_colimits.colimit_has_mul F = {mul := λ (x y : Mon.filtered_colimits.M F), quot.lift₂ (Mon.filtered_colimits.colimit_mul_aux F) _ _ x y}
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.
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.
Equations
- Mon.filtered_colimits.colimit_monoid F = {mul := has_mul.mul (Mon.filtered_colimits.colimit_has_mul F), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (Mon.filtered_colimits.M F)), npow_zero' := _, npow_succ' := _}
Equations
- AddMon.filtered_colimits.colimit_add_monoid F = {add := has_add.add (AddMon.filtered_colimits.colimit_has_add F), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (AddMon.filtered_colimits.M F)), nsmul_zero' := _, nsmul_succ' := _}
The bundled monoid giving the filtered colimit of a diagram.
Equations
Instances for ↥Mon.filtered_colimits.colimit
The bundled additive monoid giving the filtered colimit of a diagram.
Equations
Instances for ↥AddMon.filtered_colimits.colimit
The additive monoid homomorphism from a given additive monoid in the diagram to the colimit additive monoid.
Equations
- AddMon.filtered_colimits.cocone_morphism F j = {to_fun := (category_theory.limits.types.colimit_cocone (F ⋙ category_theory.forget AddMon)).ι.app j, map_zero' := _, map_add' := _}
The monoid homomorphism from a given monoid in the diagram to the colimit monoid.
Equations
- Mon.filtered_colimits.cocone_morphism F j = {to_fun := (category_theory.limits.types.colimit_cocone (F ⋙ category_theory.forget Mon)).ι.app j, map_one' := _, map_mul' := _}
The cocone over the proposed colimit monoid.
Equations
- Mon.filtered_colimits.colimit_cocone F = {X := Mon.filtered_colimits.colimit F _inst_2, ι := {app := Mon.filtered_colimits.cocone_morphism F _inst_2, naturality' := _}}
The cocone over the proposed colimit additive monoid.
Equations
- AddMon.filtered_colimits.colimit_cocone F = {X := AddMon.filtered_colimits.colimit F _inst_2, ι := {app := AddMon.filtered_colimits.cocone_morphism F _inst_2, naturality' := _}}
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
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
The proposed colimit cocone is a colimit in AddMon.
Equations
- AddMon.filtered_colimits.colimit_cocone_is_colimit F = {desc := AddMon.filtered_colimits.colimit_desc F _inst_2, fac' := _, uniq' := _}
The proposed colimit cocone is a colimit in Mon.
Equations
- Mon.filtered_colimits.colimit_cocone_is_colimit F = {desc := Mon.filtered_colimits.colimit_desc F _inst_2, fac' := _, uniq' := _}
Equations
- Mon.filtered_colimits.forget_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ Mon), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (Mon.filtered_colimits.colimit_cocone_is_colimit F) (category_theory.limits.types.colimit_cocone_is_colimit (F ⋙ category_theory.forget Mon))}}
Equations
- AddMon.filtered_colimits.forget_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ AddMon), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (AddMon.filtered_colimits.colimit_cocone_is_colimit F) (category_theory.limits.types.colimit_cocone_is_colimit (F ⋙ category_theory.forget AddMon))}}
The colimit of F ⋙ forget₂ AddCommMon AddMon in the category AddMon. In the
following, we will show that this has the structure of a commutative additive monoid.
The colimit of F ⋙ forget₂ CommMon Mon in the category Mon.
In the following, we will show that this has the structure of a commutative monoid.
Equations
- AddCommMon.filtered_colimits.colimit_add_comm_monoid F = {add := add_monoid.add (AddCommMon.filtered_colimits.M F).add_monoid, add_assoc := _, zero := add_monoid.zero (AddCommMon.filtered_colimits.M F).add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (AddCommMon.filtered_colimits.M F).add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- CommMon.filtered_colimits.colimit_comm_monoid F = {mul := monoid.mul (CommMon.filtered_colimits.M F).monoid, mul_assoc := _, one := monoid.one (CommMon.filtered_colimits.M F).monoid, one_mul := _, mul_one := _, npow := monoid.npow (CommMon.filtered_colimits.M F).monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
The bundled additive commutative monoid giving the filtered colimit of a diagram.
The bundled commutative monoid giving the filtered colimit of a diagram.
Equations
The cocone over the proposed colimit additive commutative monoid.
Equations
The cocone over the proposed colimit commutative monoid.
Equations
The proposed colimit cocone is a colimit in AddCommMon.
Equations
The proposed colimit cocone is a colimit in CommMon.
Equations
- CommMon.filtered_colimits.colimit_cocone_is_colimit F = {desc := λ (t : category_theory.limits.cocone F), Mon.filtered_colimits.colimit_desc (F ⋙ category_theory.forget₂ CommMon Mon) ((category_theory.forget₂ CommMon Mon).map_cocone t), fac' := _, uniq' := _}
Equations
- AddCommMon.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ AddCommMon), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (AddCommMon.filtered_colimits.colimit_cocone_is_colimit F) (AddMon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ AddCommMon AddMon))}}
Equations
- CommMon.filtered_colimits.forget₂_Mon_preserves_filtered_colimits = {preserves_filtered_colimits := λ (J : Type u) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), {preserves_colimit := λ (F : J ⥤ CommMon), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (CommMon.filtered_colimits.colimit_cocone_is_colimit F) (Mon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ category_theory.forget₂ CommMon Mon))}}