English
If S is finitely presented over R (i.e., S over R is of finite presentation), then the functor Hom_R(S, -) preserves filtered colimits. Equivalently, the corresponding coyoneda functor preserves filtered colimits.
Русский
Если S над R является конечнопредставимой (S над R имеет конечную презентацию), то ковариантный гомоморфизм Hom_R(S,-) сохраняет фильтрованные колимиты (то есть соответствующий кофонилонный функтор сохраняет фильтрованные пределы).
LaTeX
$$$\mathrm{PreservesFilteredColimits}\big(\mathrm{Hom}_R(S, -)\big)$$$
Lean4
/-- If `S` is a finitely presented `R`-algebra, then `Hom_R(S, -)` preserves filtered colimits. -/
theorem preservesFilteredColimits_coyoneda (S : Under R) (hS : S.hom.hom.FinitePresentation) :
PreservesFilteredColimits (coyoneda.obj (.op S)) :=
⟨fun _ _ _ ↦ ⟨preservesColimit_coyoneda_of_finitePresentation R S hS _⟩⟩
