English
Preservation of a base-change property along pushouts: the inl-map in the pushout of a span respects the property P if the base-change property holds.
Русский
Сохранение свойства через пушаут: отображение inl в пушауте сохраняет свойство P, если базовое изменение сохраняет его.
LaTeX
$$$\text{pushout.inl} : S \to \text{pushout}(f,g)$ satisfies $P$ whenever $P(g)$ and base-change holds.$$
Lean4
theorem pushout_inl (hP : RingHom.IsStableUnderBaseChange @P) (hP' : RingHom.RespectsIso @P) {R S T : CommRingCat}
(f : R ⟶ S) (g : R ⟶ T) (H : P g.hom) : P (pushout.inl _ _ : S ⟶ pushout f g).hom :=
by
letI := f.hom.toAlgebra
letI := g.hom.toAlgebra
rw [←
show _ = pushout.inl f g from
colimit.isoColimitCocone_ι_inv ⟨_, CommRingCat.pushoutCoconeIsColimit R S T⟩ WalkingSpan.left,
CommRingCat.hom_comp, hP'.cancel_right_isIso]
dsimp only [CommRingCat.pushoutCocone_inl, PushoutCocone.ι_app_left]
apply hP R T S (S ⊗[R] T)
exact H
