English
If Q contains identities and respects isomorphisms and P is affine locally defined by affineAnd(Q), then P equals IsAffineHom ⊓ P'.
Русский
Если Q содержит тождества и сохраняет изоморфизмы, а P локально определяется affineAnd(Q), тогда P = IsAffineHom ⊓ P'.
LaTeX
$$$P = (\\operatorname{IsAffineHom} \\cap P')$$$
Lean4
/-- `P` is local at the target if
1. `P` respects isomorphisms.
2. If `P` holds for `f : X ⟶ Y`, then `P` holds for `f ∣_ U` for any `U`.
3. If `P` holds for `f ∣_ U` for an open cover `U` of `Y`, then `P` holds for `f`.
-/
protected theorem mk' {P : MorphismProperty Scheme} [P.RespectsIso]
(restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U))
(of_sSup_eq_top :
∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ i, P (f ∣_ U i)) → P f) :
IsZariskiLocalAtTarget P
where
pullbackSnd 𝒰 i hf := (P.arrow_mk_iso_iff (morphismRestrictOpensRange _ _)).mp (restrict _ _ hf)
of_zeroHypercover {X Y f} 𝒰
h := by
refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) ?_
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h i)
