English
An alternative constructor for IsStableUnderBaseChange: under RespectsIso, if a certain transfer condition holds, then IsStableUnderBaseChange is granted.
Русский
Альтернативный конструктор IsStableUnderBaseChange: при условии переноса через изоморфизм и выполнения заданного условия, осуществляется устойчивость к базовому изменению.
LaTeX
$$IsStableUnderBaseChange.mk' [RespectsIso P] (hP₂ : ∀ X Y S f g [HasPullback f g] (_ : P g), P (pullback.fst f g))$$
Lean4
/-- Alternative constructor for `IsStableUnderBaseChange`. -/
theorem mk' [RespectsIso P]
(hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (_ : P g), P (pullback.fst f g)) :
IsStableUnderBaseChange P where
of_isPullback {X Y Y' S f g f' g'} sq
hg := by
haveI : HasPullback f g := sq.flip.hasPullback
let e := sq.flip.isoPullback
rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]
exact hP₂ _ _ _ f g hg
