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
.
The colimit of F ⋙ forget AddMon
in the category of types.
In the following, we will construct an additive monoid structure on M
.
Equations
Instances For
The colimit of F ⋙ forget MonCat
in the category of types.
In the following, we will construct a monoid structure on M
.
Equations
Instances For
The canonical projection into the colimit, as a quotient type.
Equations
Instances For
The canonical projection into the colimit, as a quotient type.
Equations
Instances For
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⟩ }
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⟩ }
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 IsFiltered.max
) and add them there.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Addition in the colimit is well-defined in the left argument.
Multiplication in the colimit is well-defined in the left argument.
Addition in the colimit is well-defined in the right argument.
Multiplication in the colimit is well-defined in the right argument.
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 }
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 }
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
Equations
Equations
- AddMonCat.FilteredColimits.colimitAddMonoid F = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯
Equations
- MonCat.FilteredColimits.colimitMonoid F = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯
The bundled additive monoid giving the filtered colimit of a diagram.
Instances For
The bundled monoid giving the filtered colimit of a diagram.
Equations
Instances For
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.
Instances For
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' := ⋯ }
Instances For
The cocone over the proposed colimit additive monoid.
Equations
- AddMonCat.FilteredColimits.colimitCocone F = { pt := AddMonCat.FilteredColimits.colimit F, ι := { app := AddMonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }
Instances For
The cocone over the proposed colimit monoid.
Equations
- MonCat.FilteredColimits.colimitCocone F = { pt := MonCat.FilteredColimits.colimit F, ι := { app := MonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }
Instances For
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.
Instances For
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.
Instances For
The proposed colimit cocone is a colimit in AddMonCat
.
Equations
- AddMonCat.FilteredColimits.colimitCoconeIsColimit F = { desc := AddMonCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }
Instances For
The proposed colimit cocone is a colimit in MonCat
.
Equations
- MonCat.FilteredColimits.colimitCoconeIsColimit F = { desc := MonCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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
Instances For
Equations
The bundled additive commutative monoid giving the filtered colimit of a diagram.
Equations
Instances For
The bundled commutative monoid giving the filtered colimit of a diagram.
Instances For
The cocone over the proposed colimit additive commutative monoid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone over the proposed colimit commutative monoid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in AddCommMonCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in CommMonCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.