English
If P is stable under cobase change and CodescendsAlong Q, then IsPushout f g inl inr with Q f implies P inl ↔ P g.
Русский
Если P устойчива к основанию-копированию и CodescendsAlong Q, то IsPushout f g inl inr и Q f дают P inl ⇔ P g.
LaTeX
$$$ [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] (h : IsPushout f g inl inr) (hg : Q f) : P inl \\leftrightarrow P g $$$
Lean4
instance [Q.IsStableUnderBaseChange] [P.HasOfPrecompProperty Q] [P.RespectsRight Q] : P.DescendsAlong Q where
of_isPullback {A X Y Z fst snd f g} h hf
hfst := by
apply P.of_precomp (W' := Q) _ _ (Q.of_isPullback h hf)
rw [← h.1.1]
exact RespectsRight.postcomp _ hf _ hfst
