isStableUnderBaseChange — Mathlib

English

If Q is stable under base change (localization away from the source), then P is stable under base change: pullbacks of morphisms with P again have P.

Русский

Если Q устойчиво к базовым изменениям (локализация вдоль источника), то P устойчиво к базовым изменениям: базовые изменения сохраняют свойство P.

LaTeX

$$$(\text{RingHom.IsStableUnderBaseChange } Q) \Rightarrow P.\text{IsStableUnderBaseChange}$$$

Lean4

theorem isStableUnderBaseChange (hP : RingHom.IsStableUnderBaseChange Q) : P.IsStableUnderBaseChange :=
  by
  apply HasAffineProperty.isStableUnderBaseChange
  letI := HasAffineProperty.isLocal_affineProperty P
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g H
  rw [← HasAffineProperty.iff_of_isAffine (P := P)] at H ⊢
  wlog hX : IsAffine Y generalizing Y
  · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
    intro i
    simp only [Scheme.Pullback.openCoverOfRight_X, Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_pt,
      PullbackCone.mk_π_app, Category.comp_id]
    apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance
  rw [iff_of_isAffine (P := P)] at H ⊢
  exact hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H

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