Filtered colimits in the category of R-algebras

In this file we show that the forgetful functor from R-algebras to rings creates filtered colimits.

@[implicit_reducible]

noncomputable instance instCreatesColimitsOfShapeAlgCatRingCatForget₂AlgHomCarrierRingHomCarrierOfIsFiltered {R : Type u} [CommRing R] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] [CategoryTheory.IsFiltered J] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget₂ (AlgCat R) RingCat)

Equations

• One or more equations did not get rendered due to their size.

instance instHasColimitsOfShapeAlgCatOfIsFilteredOfRingCat {R : Type u} [CommRing R] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] [CategoryTheory.IsFiltered J] [CategoryTheory.Limits.HasColimitsOfShape J RingCat] : CategoryTheory.Limits.HasColimitsOfShape J (AlgCat R)

instance instPreservesFilteredColimitsAlgCatRingCatForget₂AlgHomCarrierRingHomCarrier {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ (AlgCat R) RingCat)

instance instPreservesFilteredColimitsAlgCatForgetAlgHomCarrier {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget (AlgCat R))