English
If P is preserved under pushouts and respects iso, and for every pushout square the right leg inherits P from the left leg, then P is stable under cobase change.
Русский
Если P сохраняется при пуш-ауте и учитывает изоморфии, и для каждого квадрата пуш-аут правая нога наследует P от левой, то P устойчива к cobase change.
LaTeX
$$([RespectsIso P], ∀ A B A' (f:A→A') (g:A→B) [HasPushout f g], (P f) → P(pushout.inr f g)) → IsStableUnderCobaseChange P$$
Lean4
/-- An alternative constructor for `IsStableUnderCobaseChange`. -/
theorem mk' [RespectsIso P]
(hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (_ : P f), P (pushout.inr f g)) :
IsStableUnderCobaseChange P where
of_isPushout {A A' B B' f g f' g'} sq
hf := by
haveI : HasPushout f g := sq.flip.hasPushout
let e := sq.flip.isoPushout
rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]
exact hP₂ _ _ _ f g hf
