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.

theorem RingHom.EssFiniteType.exists_comp_map_eq_of_isColimit {J : Type uJ} [CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat) (F : CategoryTheory.Functor J CommRingCat) (α : (CategoryTheory.Functor.const J).obj R ⟶ F) {S : CommRingCat} (f : R ⟶ S) (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget CommRingCat)] (hf : (CommRingCat.Hom.hom f).EssFiniteType) {i : J} (a : S ⟶ F.obj i) (ha : CategoryTheory.CategoryStruct.comp f a = α.app i) {j : J} (b : S ⟶ F.obj j) (hb : CategoryTheory.CategoryStruct.comp f b = α.app j) (hab : CategoryTheory.CategoryStruct.comp a (c.ι.app i) = CategoryTheory.CategoryStruct.comp b (c.ι.app j)) : ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), CategoryTheory.CategoryStruct.comp a (F.map hik) = CategoryTheory.CategoryStruct.comp b (F.map hjk)

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.

theorem RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit {J : Type uJ} [CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat) (F : CategoryTheory.Functor J CommRingCat) (α : (CategoryTheory.Functor.const J).obj R ⟶ F) {S : CommRingCat} (f : R ⟶ S) (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget CommRingCat)] (hf : (CommRingCat.Hom.hom f).FinitePresentation) (g : S ⟶ c.pt) (hg : ∀ (i : J), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp (α.app i) (c.ι.app i)) : ∃ (i : J) (g' : S ⟶ F.obj i), CategoryTheory.CategoryStruct.comp f g' = α.app i ∧ g = CategoryTheory.CategoryStruct.comp g' (c.ι.app i)

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.

theorem preservesColimit_coyoneda_of_finitePresentation {J : Type uJ} [CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat) (S : CategoryTheory.Under R) (hS : (CommRingCat.Hom.hom S.hom).FinitePresentation) (F : CategoryTheory.Functor J (CategoryTheory.Under R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Under.forget R)) (CategoryTheory.forget CommRingCat)] : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.coyoneda.obj (Opposite.op S))

If S is a finitely presented R-algebra, then Hom_R(S, -) preserves filtered colimits.

theorem preservesFilteredColimits_coyoneda (R : CommRingCat) (S : CategoryTheory.Under R) (hS : (CommRingCat.Hom.hom S.hom).FinitePresentation) : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.coyoneda.obj (Opposite.op S))

If S is a finitely presented R-algebra, then Hom_R(S, -) preserves filtered colimits.

theorem isFinitelyPresentable (R : CommRingCat) (S : CategoryTheory.Under R) (hS : (CommRingCat.Hom.hom S.hom).FinitePresentation) : CategoryTheory.IsFinitelyPresentable S

If S is a finitely presented R-algebra, S : Under R is finitely presentable.