of_targetAffineLocally_of_isPullback

English

If f is target affine-locally locally P and iY is a pullback square with iX, then the pulled-back morphism f' has P.

Русский

Если f локально по цели вдоль аффинной части и дан квадрат тягосоглашения, то отражающийся морфизм f' имеет свойство P.

LaTeX

$$$IsPullback iX f' f iY \Rightarrow (targetAffineLocally P f) \Rightarrow P f'.$$$

Lean4

theorem of_targetAffineLocally_of_isPullback {P : AffineTargetMorphismProperty} [P.IsLocal] {X Y UX UY : Scheme.{u}}
    [IsAffine UY] {f : X ⟶ Y} {iY : UY ⟶ Y} [IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY}
    (h : IsPullback iX f' f iY) (hf : targetAffineLocally P f) : P f' :=
  by
  rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
  exact (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp (hf ⟨_, isAffineOpen_opensRange iY⟩)

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