Documentation

Mathlib.Algebra.Category.Ring.FinitePresentation

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, S : Under R is finitely presentable.