English
If a larger algebraic pushout is assumed to be a pushout, then the induced maps yield a pushout diagram as well by a compatible construction.
Русский
Если дан предикат пуш-аут, то индуцированные отображения дают пуш-аут-диаграмму.
LaTeX
$$$\text{IsPushout}(f,g,a,b) \Rightarrow \text{IsPushout}(...)$$$
Lean4
theorem isPushout_of_isPushout (R S A B : Type u) [CommRing R] [CommRing S] [CommRing A] [CommRing B] [Algebra R S]
[Algebra S B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B]
[Algebra.IsPushout R S A B] :
IsPushout (ofHom (algebraMap R S)) (ofHom (algebraMap R A)) (ofHom (algebraMap S B)) (ofHom (algebraMap A B)) :=
(isPushout_tensorProduct R S A).of_iso (Iso.refl _) (Iso.refl _) (Iso.refl _)
(Algebra.IsPushout.equiv R S A B).toCommRingCatIso (by simp) (by simp) (by ext; simp [Algebra.IsPushout.equiv_tmul])
(by ext; simp [Algebra.IsPushout.equiv_tmul])
