Finitely presentable objects in Under R
with R : CommRingCat
#
In this file, we show that finitely presented algebras are finitely presentable in Under R
,
i.e. Hom_R(S, -)
preserves filtered colimits.
Given a filtered diagram F
of rings over R
, S
an (essentially) of finite type R
-algebra,
and two ring homs a : S ⟶ Fᵢ
and b : S ⟶ Fⱼ
over R
.
If a
and b
agree at S ⟶ colimit F
,
then there exists k
such that a
and b
are equal at S ⟶ F_k
.
In other words, the map colimᵢ Hom_R(S, Fᵢ) ⟶ Hom_R(S, colim F)
is injective.
Given a filtered diagram F
of rings over R
, S
a finitely presented R
-algebra,
and a ring hom g : S ⟶ colimit F
over R
.
then there exists i
such that g
factors through Fᵢ
.
In other words, the map colimᵢ Hom_R(S, Fᵢ) ⟶ Hom_R(S, colim F)
is surjective.
If S
is a finitely presented R
-algebra, then Hom_R(S, -)
preserves filtered colimits.
If S
is a finitely presented R
-algebra, then Hom_R(S, -)
preserves filtered colimits.
If S
is a finitely presented R
-algebra, S : Under R
is finitely presentable.