of_isPullback_of_descendsAlong — Mathlib

English

If f,g form a pullback square and the left leg satisfies a Q-property, while f satisfies Q and fst satisfies P, then g satisfies P. This expresses how descent along pullbacks transfers morphism properties downward along the right leg.

Русский

Если имеется квадрат-перекрестие (pullback), левая часть удовлетворяет свойству Q, f удовлетворяет Q, а fst удовлетворяет P, то g удовлетворяет P.

LaTeX

$$$ [P.DescendsAlong Q] [HasPullback f g] (hf : Q f) (hfst : Pfst) \\Rightarrow P g.$$

Lean4

theorem of_isPullback_of_descendsAlong [P.DescendsAlong Q] (h : IsPullback fst snd f g) (hf : Q f) (hfst : P fst) :
    P g :=
  DescendsAlong.of_isPullback h hf hfst

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