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.
abbrev
AddMonCat.FilteredColimits.M
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
:
The colimit of F ⋙ forget AddMon in the category of types.
In the following, we will construct an additive monoid structure on M.
Instances For
@[inline, reducible]
abbrev
MonCat.FilteredColimits.M
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
:
The colimit of F ⋙ forget MonCat in the category of types.
In the following, we will construct a monoid structure on M.
Instances For
abbrev
AddMonCat.FilteredColimits.M.mk
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
:
(j : J) × ↑(F.obj j) → AddMonCat.FilteredColimits.M F
The canonical projection into the colimit, as a quotient type.
Instances For
@[inline, reducible]
abbrev
MonCat.FilteredColimits.M.mk
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
:
(j : J) × ↑(F.obj j) → MonCat.FilteredColimits.M F
The canonical projection into the colimit, as a quotient type.
Instances For
theorem
AddMonCat.FilteredColimits.M.mk_eq
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
(x : (j : J) × ↑(F.obj j))
(y : (j : J) × ↑(F.obj j))
(h : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd)
:
theorem
MonCat.FilteredColimits.M.mk_eq
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
(x : (j : J) × ↑(F.obj j))
(y : (j : J) × ↑(F.obj j))
(h : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd)
:
noncomputable instance
AddMonCat.FilteredColimits.colimitZero
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered 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₀⟩.
noncomputable instance
MonCat.FilteredColimits.colimitOne
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
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₀⟩.
theorem
AddMonCat.FilteredColimits.colimit_zero_eq
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(j : J)
:
0 = AddMonCat.FilteredColimits.M.mk F { fst := j, snd := 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 MonCat)
[CategoryTheory.IsFiltered J]
(j : J)
:
1 = MonCat.FilteredColimits.M.mk F { fst := j, snd := 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 AddMonCat)
[CategoryTheory.IsFiltered J]
(x : (j : J) × ↑(F.obj j))
(y : (j : J) × ↑(F.obj 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.
Instances For
noncomputable def
MonCat.FilteredColimits.colimitMulAux
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
(x : (j : J) × ↑(F.obj j))
(y : (j : J) × ↑(F.obj j))
:
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.
Instances For
theorem
AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_left
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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 (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)) x x')
:
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 MonCat)
[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 (CategoryTheory.Functor.comp F (CategoryTheory.forget MonCat)) x x')
:
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 AddMonCat)
[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 (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)) y 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 MonCat)
[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 (CategoryTheory.Functor.comp F (CategoryTheory.forget MonCat)) y y')
:
Multiplication in the colimit is well-defined in the right argument.
noncomputable instance
AddMonCat.FilteredColimits.colimitAdd
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
Addition in the colimit. See also colimitAddAux.
theorem
AddMonCat.FilteredColimits.colimitAdd.proof_2
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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 (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)) x x')
:
theorem
AddMonCat.FilteredColimits.colimitAdd.proof_1
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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 (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)) y y')
:
noncomputable instance
MonCat.FilteredColimits.colimitMul
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
Multiplication in the colimit. See also colimitMulAux.
theorem
AddMonCat.FilteredColimits.colimit_add_mk_eq
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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 { fst := k, snd := ↑(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 MonCat)
[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 { fst := k, snd := ↑(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 AddMonCat)
[CategoryTheory.IsFiltered J]
(x : AddMonCat.FilteredColimits.M F)
:
noncomputable instance
AddMonCat.FilteredColimits.colimitAddZeroClass
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
theorem
AddMonCat.FilteredColimits.colimitAddZeroClass.proof_2
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(x : AddMonCat.FilteredColimits.M F)
:
noncomputable instance
MonCat.FilteredColimits.colimitMulOneClass
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
theorem
AddMonCat.FilteredColimits.colimitAddMonoid.proof_2
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(a : AddMonCat.FilteredColimits.M F)
:
theorem
AddMonCat.FilteredColimits.colimitAddMonoid.proof_4
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
∀ (x : AddMonCat.FilteredColimits.M F), nsmulRec 0 x = nsmulRec 0 x
theorem
AddMonCat.FilteredColimits.colimitAddMonoid.proof_3
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(a : AddMonCat.FilteredColimits.M F)
:
noncomputable instance
AddMonCat.FilteredColimits.colimitAddMonoid
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
theorem
AddMonCat.FilteredColimits.colimitAddMonoid.proof_1
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(x : AddMonCat.FilteredColimits.M F)
(y : AddMonCat.FilteredColimits.M F)
(z : AddMonCat.FilteredColimits.M F)
:
theorem
AddMonCat.FilteredColimits.colimitAddMonoid.proof_5
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
∀ (n : ℕ) (x : AddMonCat.FilteredColimits.M F), nsmulRec (n + 1) x = nsmulRec (n + 1) x
noncomputable instance
MonCat.FilteredColimits.colimitMonoid
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
noncomputable def
AddMonCat.FilteredColimits.colimit
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
The bundled additive monoid giving the filtered colimit of a diagram.
Instances For
noncomputable def
MonCat.FilteredColimits.colimit
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
The bundled monoid giving the filtered colimit of a diagram.
Instances For
theorem
AddMonCat.FilteredColimits.coconeMorphism.proof_1
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(j : J)
:
AddMonCat.FilteredColimits.M.mk F { fst := j, snd := 0 } = 0
def
AddMonCat.FilteredColimits.coconeMorphism
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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.
Instances For
theorem
AddMonCat.FilteredColimits.coconeMorphism.proof_2
{J : Type u_2}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(j : J)
(x : ↑(F.obj j))
(y : ↑(F.obj j))
:
ZeroHom.toFun
{
toFun :=
(CategoryTheory.Limits.Types.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))).ι.app
j,
map_zero' := (_ : AddMonCat.FilteredColimits.M.mk F { fst := j, snd := 0 } = 0) }
(x + y) = ZeroHom.toFun
{
toFun :=
(CategoryTheory.Limits.Types.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))).ι.app
j,
map_zero' := (_ : AddMonCat.FilteredColimits.M.mk F { fst := j, snd := 0 } = 0) }
x + ZeroHom.toFun
{
toFun :=
(CategoryTheory.Limits.Types.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))).ι.app
j,
map_zero' := (_ : AddMonCat.FilteredColimits.M.mk F { fst := j, snd := 0 } = 0) }
y
def
MonCat.FilteredColimits.coconeMorphism
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[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.
Instances For
@[simp]
theorem
AddMonCat.FilteredColimits.cocone_naturality
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
{j : J}
{j' : J}
(f : j ⟶ j')
:
@[simp]
theorem
MonCat.FilteredColimits.cocone_naturality
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
{j : J}
{j' : J}
(f : j ⟶ j')
:
theorem
AddMonCat.FilteredColimits.colimitCocone.proof_1
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
⦃X : J⦄
⦃Y : J⦄
(f : X ⟶ Y)
:
noncomputable def
AddMonCat.FilteredColimits.colimitCocone
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
The cocone over the proposed colimit additive monoid.
Instances For
noncomputable def
MonCat.FilteredColimits.colimitCocone
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
The cocone over the proposed colimit monoid.
Instances For
def
AddMonCat.FilteredColimits.colimitDesc
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(t : CategoryTheory.Limits.Cocone F)
:
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.
Instances For
theorem
AddMonCat.FilteredColimits.colimitDesc.proof_1
{J : Type u_2}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(t : CategoryTheory.Limits.Cocone F)
:
CategoryTheory.Limits.IsColimit.desc J inst✝ TypeMax CategoryTheory.types
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))
(CategoryTheory.Limits.Types.colimitCocone (CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t) 0 = 0
theorem
AddMonCat.FilteredColimits.colimitDesc.proof_2
{J : Type u_2}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
(t : CategoryTheory.Limits.Cocone F)
(x : ↑(AddMonCat.FilteredColimits.colimit F))
(y : ↑(AddMonCat.FilteredColimits.colimit F))
:
ZeroHom.toFun
{
toFun :=
CategoryTheory.Limits.IsColimit.desc
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t),
map_zero' :=
(_ :
CategoryTheory.Limits.IsColimit.desc J inst✝ TypeMax CategoryTheory.types
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))
(CategoryTheory.Limits.Types.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t) 0 = 0) }
(x + y) = ZeroHom.toFun
{
toFun :=
CategoryTheory.Limits.IsColimit.desc
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t),
map_zero' :=
(_ :
CategoryTheory.Limits.IsColimit.desc J inst✝ TypeMax CategoryTheory.types
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))
(CategoryTheory.Limits.Types.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t) 0 = 0) }
x + ZeroHom.toFun
{
toFun :=
CategoryTheory.Limits.IsColimit.desc
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t),
map_zero' :=
(_ :
CategoryTheory.Limits.IsColimit.desc J inst✝ TypeMax CategoryTheory.types
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat))
(CategoryTheory.Limits.Types.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
(CategoryTheory.Limits.Types.colimitCoconeIsColimit
(CategoryTheory.Functor.comp F (CategoryTheory.forget AddMonCat)))
((CategoryTheory.forget AddMonCat).mapCocone t) 0 = 0) }
y
def
MonCat.FilteredColimits.colimitDesc
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[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.
Instances For
theorem
AddMonCat.FilteredColimits.colimitCoconeIsColimit.proof_1
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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
theorem
AddMonCat.FilteredColimits.colimitCoconeIsColimit.proof_2
{J : Type u_1}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[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)
:
def
AddMonCat.FilteredColimits.colimitCoconeIsColimit
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J AddMonCat)
[CategoryTheory.IsFiltered J]
:
The proposed colimit cocone is a colimit in AddMon.
Instances For
def
MonCat.FilteredColimits.colimitCoconeIsColimit
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J MonCat)
[CategoryTheory.IsFiltered J]
:
The proposed colimit cocone is a colimit in MonCat.
Instances For
noncomputable abbrev
AddCommMonCat.FilteredColimits.M
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J AddCommMonCat)
:
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.
Instances For
@[inline, reducible]
noncomputable abbrev
CommMonCat.FilteredColimits.M
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J CommMonCat)
:
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.
Instances For
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))
:
noncomputable instance
AddCommMonCat.FilteredColimits.colimitAddCommMonoid
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J AddCommMonCat)
:
noncomputable instance
CommMonCat.FilteredColimits.colimitCommMonoid
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J CommMonCat)
:
noncomputable def
AddCommMonCat.FilteredColimits.colimit
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J AddCommMonCat)
:
The bundled additive commutative monoid giving the filtered colimit of a diagram.
Instances For
noncomputable def
CommMonCat.FilteredColimits.colimit
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J CommMonCat)
:
The bundled commutative monoid giving the filtered colimit of a diagram.
Instances For
noncomputable def
AddCommMonCat.FilteredColimits.colimitCocone
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J AddCommMonCat)
:
The cocone over the proposed colimit additive commutative monoid.
Instances For
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
((CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).map f)
((AddMonCat.FilteredColimits.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).ι.app
Y) = CategoryTheory.CategoryStruct.comp
((AddMonCat.FilteredColimits.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).ι.app
X)
(((CategoryTheory.Functor.const J).obj
(AddMonCat.FilteredColimits.colimitCocone
(CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).pt).map
f)
noncomputable def
CommMonCat.FilteredColimits.colimitCocone
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J CommMonCat)
:
The cocone over the proposed colimit commutative monoid.
Instances For
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 =>
AddMonCat.FilteredColimits.colimitDesc
(CategoryTheory.Functor.comp F (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 =>
AddMonCat.FilteredColimits.colimitDesc
(CategoryTheory.Functor.comp F (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)
:
The proposed colimit cocone is a colimit in AddCommMon.
Instances For
def
CommMonCat.FilteredColimits.colimitCoconeIsColimit
{J : Type v}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
(F : CategoryTheory.Functor J CommMonCat)
:
The proposed colimit cocone is a colimit in CommMonCat.