Smallness results on the category of CommRing

theorem CommRingCat.essentiallySmall_of_finiteType {P Q : CategoryTheory.ObjectProperty CommRingCat} [CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} Q] (hPQ : ∀ (S : CommRingCat), P S → ∃ (R : CommRingCat), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType) : CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} P

theorem CommRingCat.essentiallySmall_of_localizationAway {P Q : CategoryTheory.ObjectProperty CommRingCat} [CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} Q] (hPQ : ∀ (S : CommRingCat), P S → ∃ (s : Set ↑S), Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q ↧(Localization.Away f)) : CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} P