English
An alternate constructor for CodescendsAlong Q given a universal pushout descent rule H.
Русский
Альтернативное построение CodescendsAlong Q через универсальное правило спуска, представленное H.
LaTeX
$$$\forall {C} [\mathsf{Category} C] {P Q : \mathsf{MorphismProperty} C} [P.RespectsIso], (H : \forall {X Y Z : C} {f : Z \rightarrow X} {g : Z \rightarrow Y} [\mathsf{HasPushout} f g], Q f \rightarrow P(\mathrm{pushout.inl} f g) \rightarrow P g) \Rightarrow P.CodescendsAlong Q.$$$
Lean4
/-- Alternative constructor for `CodescendsAlong` using `HasPushout`. -/
theorem mk' [P.RespectsIso]
(H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [HasPushout f g], Q f → P (pushout.inl f g) → P g) : P.CodescendsAlong Q
where
of_isPushout {A X Y Z f g inl inr} h hf
hfst := by
have : HasPushout f g := h.hasPushout
apply H hf
rwa [← P.cancel_right_of_respectsIso _ h.isoPushout.inv, h.inl_isoPushout_inv]
