iff_of_isPullback — Mathlib

English

For a pullback square, under appropriate base-change stability, the property P on the left leg is equivalent to the property P on the right leg when P descends along Q along the pullback, given an hf condition.

Русский

Для квадрата-пуллбака при условии устойчивости P к базовым изменениям и descendAlong(Q) свойство на левой стороне равно свойству на правой, при заданном hf.

LaTeX

$$$ [P.IsStableUnderBaseChange] [P.DescendsAlong Q] (\nIsPullback fst snd f g) \\Rightarrow (Q f \\Rightarrow P fst \\leftrightarrow P g).$$$

Lean4

theorem iff_of_isPullback [P.IsStableUnderBaseChange] [P.DescendsAlong Q] (h : IsPullback fst snd f g) (hf : Q f) :
    P fst ↔ P g :=
  ⟨fun hfst ↦ of_isPullback_of_descendsAlong h hf hfst, fun hf ↦ P.of_isPullback h.flip hf⟩

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