English
The property P is local on the target in the Zariski topology whenever HasAffineProperty P Q holds.
Русский
Свойство P локально по цели в Zariski-опоре при условии HasAffineProperty P Q.
LaTeX
$$$IsZariskiLocalAtTarget P$$$
Lean4
instance (priority := 900) : IsZariskiLocalAtTarget P :=
by
letI := isLocal_affineProperty P
apply IsZariskiLocalAtTarget.mk'
· rw [eq_targetAffineLocally P]
intro X Y f U H V
rw [Q.arrow_mk_iso_iff (morphismRestrictRestrict f _ _)]
exact H ⟨_, V.2.image_of_isOpenImmersion (Y.ofRestrict _)⟩
· rintro X Y f ι U hU H
let 𝒰 := Y.openCoverOfIsOpenCover U hU
apply of_openCover 𝒰.affineRefinement.openCover
rintro ⟨i, j⟩
have : P (𝒰.pullbackHom f i) :=
by
refine (P.arrow_mk_iso_iff (morphismRestrictEq _ ?_ ≪≫ morphismRestrictOpensRange f (𝒰.f i))).mp (H i)
exact (Scheme.Opens.opensRange_ι _).symm
rw [← Q.cancel_left_of_respectsIso (𝒰.pullbackCoverAffineRefinementObjIso f _).inv,
𝒰.pullbackCoverAffineRefinementObjIso_inv_pullbackHom]
exact of_isPullback (.of_hasPullback _ _) this
