English
The affineAnd(Q) local condition is equivalent to IsAffineHom and the affineLocally condition for Q.
Русский
Локальное условие affineAnd(Q) эквивалентно IsAffineHom и локальному условию affineLocally для Q.
LaTeX
$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q)) f \\iff \\operatorname{IsAffineHom}(f) \\land \\operatorname{affineLocally}(Q) f$$$
Lean4
theorem targetAffineLocally_affineAnd_iff_affineLocally (hQ : RingHom.PropertyIsLocal Q) {X Y : Scheme.{u}}
(f : X ⟶ Y) : targetAffineLocally (affineAnd Q) f ↔ IsAffineHom f ∧ affineLocally Q f :=
by
haveI : HasRingHomProperty (affineLocally Q) Q := ⟨hQ, rfl⟩
rw [targetAffineLocally_affineAnd_iff' hQ.respectsIso]
simp only [and_congr_right_iff]
intro hf
constructor
· wlog hY : IsAffine Y
· intro h
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := affineLocally Q) _ (iSup_affineOpens_eq_top _)]
intro U
have : IsAffine (f ⁻¹ᵁ U) := hf.isAffine_preimage U U.2
rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q), morphismRestrict_appTop, CommRingCat.hom_comp,
hQ.respectsIso.cancel_right_isIso]
apply h
rw [Scheme.Opens.ι_image_top]
exact U.2
intro h
have : IsAffine X := isAffine_of_isAffineHom f
rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q)]
exact h ⊤ (isAffineOpen_top Y)
· intro h U hU
rw [affineLocally_iff_affineOpens_le] at h
rw [f.app_eq_appLE]
exact h ⟨U, hU⟩ ⟨f ⁻¹ᵁ U, hf.isAffine_preimage U hU⟩ (by simp)
