Morphisms to a colimit in a Grothendieck abelian category #
Let C : Type u be an abelian category [Category.{v} C] which
satisfies IsGrothendieckAbelian.{w} C. We may expect
that all the objects X : C are κ-presentable for some regular
cardinal κ. However, we only prove a weaker result (which
is enough in order to obtain the existence of enough
injectives (TODO)): let κ be a big enough regular
cardinal κ such that if Y : J ⥤ C is a functor from
a κ-filtered category, and c : Cocone Y is a colimit cocone,
then the map from the colimit of the types X ⟶ Y j to
X ⟶ c.pt is injective, and it is bijective under the
additional assumption that for any map f : j ⟶ j' in J,
Y.map f is a monomorphism, see
IsGrothendieckAbelian.preservesColimit_coyoneda_obj_of_mono.
Given y : X ⟶ Y.obj j₀, we introduce a natural
transformation g : X ⟶ Y.obj t.right for t : Under j₀.
We consider the kernel of this morphism: we have a natural exact sequence
kernel (g y) ⟶ X ⟶ Y.obj t.right for all t : Under j₀. Under the
assumption that the composition y ≫ c.ι.app j₀ : X ⟶ c.pt is zero,
we get that after passing to the colimit, the right map X ⟶ c.pt is
zero, which implies that the left map f : colimit (kernel (g y)) ⟶ X
is an epimorphism (see epi_f). If κ is a regular cardinal that is
bigger than the cardinality of Subobject X and J is κ-filtered,
it follows that for some φ : j₀ ⟶ j in Under j₀,
the inclusion (kernel.ι (g y)).app j is an isomorphism,
which implies that that y ≫ Y.map φ = 0 (see the lemma injectivity₀).
The natural transformation X ⟶ Y.obj t.right for t : Under j₀
that is induced by y : X ⟶ Y.obj j₀.
Equations
- CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y = { app := fun (t : CategoryTheory.Under j₀) => CategoryTheory.CategoryStruct.comp y (Y.map t.hom), naturality := ⋯ }
Instances For
The obvious morphism colimit (kernel (g y)) ⟶ X (which is an epimorphism
if J is filtered, see epi_f.).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel of g y gives a family of subobjects of X indexed by Under j0, and we consider it as a functor Under j₀ ⥤ MonoOver X`.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let z : X ⟶ c.pt (where c is a colimit cocone for Y : J ⥤ C).
We consider the pullback of c.ι and of the constant
map (Functor.const J).map z. If we assume that c.ι is a monomorphism,
then this pullback evaluated at j : J can be identified to a subobject of X
(this is the inverse image by z of Y.obj j considered as a subobject of c.pt).
This corresponds to a functor F z : J ⥤ MonoOver X, and when taking the colimit
(computed in C), we obtain an epimorphism
f z : colimit (pullback c.ι ((Functor.const J).map z)) ⟶ X
when J is filtered (see epi_f). If κ is a regular cardinal that is
bigger than the cardinality of Subobject X and J is κ-filtered,
we deduce that z factors as X ⟶ Y.obj j ⟶ c.pt for some j
(see the lemma surjectivity).
The functor J ⥤ MonoOver X which sends j : J to the inverse image by z : X ⟶ c.pt
of the subobject Y.obj j of c.pt; it is defined here as the object in MonoOver X
corresponding to the monomorphism
(pullback.snd c.ι ((Functor.const _).map z)).app j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical map colimit (pullback c.ι ((Functor.const J).map z)) ⟶ X,
which is an isomorphism when J is filtered, see isIso_f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If X is an object in a Grothendieck abelian category, then
the functor coyoneda.obj (op X) commutes with colimits corresponding
to diagrams of monomorphisms indexed by κ-filtered categories
for a big enough regular cardinal κ.