English
For any property P, the universally defined property P.universally is Zariski-local at the source.
Русский
Для любого свойства P локальность относительно источника сохраняется в свойстве P.universally по Zariski.
LaTeX
$$IsZariskiLocalAtSource(P.universally)$$
Lean4
theorem universally_isZariskiLocalAtSource (P : MorphismProperty Scheme) [IsZariskiLocalAtSource P] :
IsZariskiLocalAtSource P.universally := by
refine .mk_of_iff ?_
intro X Y f 𝒰
refine ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
· apply MorphismProperty.universally_mk'
intro T g _
rw [← P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso g f _).hom, pullbackLeftPullbackSndIso_hom_fst]
exact IsZariskiLocalAtSource.comp (hf _ _ _ (IsPullback.of_hasPullback ..)) _
· apply MorphismProperty.universally_mk'
intro T g _
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (𝒰.pullback₁ <| pullback.snd g f)]
intro i
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
PreZeroHypercover.pullback₁_f]
rw [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso]
exact hf i _ _ _ (IsPullback.of_hasPullback ..)
