Results on the category of rings requiring linear algebra #
Results #
CommRingCat.nontrivial_of_isPushout_of_isField: the pushout of non-trivial rings over a field is non-trivial.
theorem CommRingCat.nontrivial_of_isPushout_of_isField {A B C D : CommRingCat} (hA : IsField ↑A) {f : A ⟶ B} {g : A ⟶ C} {inl : B ⟶ D} {inr : C ⟶ D} [Nontrivial ↑B] [Nontrivial ↑C] (h : CategoryTheory.IsPushout f g inl inr) :
Nontrivial ↑D