English
If Q is stable under base change, then P is stable under base change.
Русский
Если Q стабильно по основанию, то и P стабильно по основанию.
LaTeX
$$$Q.IsStableUnderBaseChange \Rightarrow P.IsStableUnderBaseChange$$$
Lean4
theorem isStableUnderBaseChange (hP' : Q.IsStableUnderBaseChange) : P.IsStableUnderBaseChange :=
MorphismProperty.IsStableUnderBaseChange.mk'
(fun X Y S f g _ H => by
rw [P.iff_of_zeroHypercover_target (S.affineCover.pullback₁ f)]
intro i
let e : pullback (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) ≅ _ :=
by
refine
pullbackSymmetry _ _ ≪≫
pullbackRightPullbackFstIso f g _ ≪≫
?_ ≪≫ (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
exact asIso (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using pullback.condition) (by simp))
have : e.hom ≫ pullback.fst _ _ = pullback.snd (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) := by simp [e]
rw [← this, P.cancel_left_of_respectsIso]
apply HasAffineProperty.pullback_fst_of_right hP'
letI := isLocal_affineProperty P
rw [← pullbackSymmetry_hom_comp_snd, Q.cancel_left_of_respectsIso]
apply of_isPullback (.of_hasPullback _ _) H)
