English
If P is a property of morphisms of schemes induced by a ring-homomorphism property Q that is stable under composition and respects isomorphism, then P holds for f iff for every x ∈ X there exist affine opens U in Y and V in X, with x ∈ V, and a relation e between V and U such that the induced map appLE has property Q.
Русский
Если P — свойство морфизмов схем, индуцированное свойством кольцевых гомоморфизмов Q, устойчивое к композиции и сохраняющее изоморфизмы, тогда P(f) эквивалентно тому, что для каждого x ∈ X существуют афинные открытые подмножества U в Y и V в X, с x ∈ V, и соответствие e между V и U так, что соответствующий гомоморфизм appLE имеет свойство Q.
LaTeX
$$$\text{RingHom.StableUnderCompositionWithLocalizationAwaySource } Q \Rightarrow (\text{RespectsIso } Q) \Rightarrow [\text{HasRingHomProperty } P (\text{Locally } Q)] : P(f) \iff \forall x:\, X, \exists U,V,\dots, Q( f. appLE U V e).hom$$$
Lean4
/-- Any property of scheme morphisms induced by a property of ring homomorphisms is stable
under composition with open immersions. -/
theorem respects_isOpenImmersion (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource Q) :
P.Respects @IsOpenImmersion where
postcomp {X Y Z} i hi f
hf := by
wlog hZ : IsAffine Z generalizing X Y Z
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
intro U
rw [morphismRestrict_comp]
exact this _ inferInstance _ (IsZariskiLocalAtTarget.restrict hf _) U.2
let e : Y ≅ i.opensRange.toScheme := IsOpenImmersion.isoOfRangeEq i i.opensRange.ι (by simp)
rw [show f ≫ i = f ≫ e.hom ≫ i.opensRange.ι by simp [e], ← Category.assoc]
exact respects_isOpenImmersion_aux hQ _ (by rwa [P.cancel_right_of_respectsIso])
