mk' — Mathlib

English

If f,g form a pushout, and Q f holds, then P inl implies P inr (via CodescendsAlong).

Русский

Если f,g образуют пушаут, и Q f, то P inl приводит к P inr через CodescendsAlong.

LaTeX

$$$ [P.CodescendsAlong Q] (IsPushout f g inl inr) \\Rightarrow Q f \\Rightarrow P inl \\Rightarrow P inr$$$

Lean4

/-- Alternative constructor for `CodescendsAlong` using `HasPullback`. -/
theorem mk' [P.RespectsIso]
    (H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g], Q f → P (pullback.fst f g) → P g) : P.DescendsAlong Q
    where
  of_isPullback {A X Y Z fst snd f g} h hf
    hfst := by
    have : HasPullback f g := h.hasPullback
    apply H hf
    rwa [← P.cancel_left_of_respectsIso h.isoPullback.hom, h.isoPullback_hom_fst]

Похожие утверждения