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