IsStableUnderBaseChange from RingHom to CommRingCatᵒᵖ

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe u

variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)
  (hp : RingHom.IsStableUnderBaseChange P)

theorem foo : (RingHom.toMorphismProperty P).op.IsStableUnderBaseChange := by
  sorry

[Kenny Lau]

I'm stuck on converting from the categorical "IsPushout" in CommRingCatᵒᵖ to the Algebra.IsPushout predicate.

[Kenny Lau]

What is the standard way to prove this?

[Christian Merten]

I have this in my pi1 repository. I can upstream it later today.

[Christian Merten]

#27380