English
For any morphism f, target is affine-locally with respect to affineAnd(Q) iff f isAffineHom and every affine open in the target pulls back to an affine open with Q on the induced map.
Русский
Для морфизма f целевая область является локально аффинальной относительно affineAnd(Q) тогда и только тогда, когда f являетсяAffineHom, а каждое аффинное открытое подмножество в цели тянется в аффинное открытое множество и на него выполняется Q.
LaTeX
$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q))\\,f \\iff \\operatorname{IsAffineHom}(f) \\land \\operatorname{affineLocally}(Q)\\,f$$$
Lean4
theorem targetAffineLocally_affineAnd_iff (hQi : RingHom.RespectsIso Q) {X Y : Scheme.{u}} (f : X ⟶ Y) :
targetAffineLocally (affineAnd Q) f ↔ ∀ U : Y.Opens, IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (f.app U).hom :=
by
simp only [targetAffineLocally, affineAnd_apply, morphismRestrict_app, CommRingCat.hom_comp, hQi.cancel_right_isIso]
refine ⟨fun hf U hU ↦ ?_, fun h U ↦ ?_⟩
· obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩
use hfU
have hf : Q (Scheme.Hom.app f (((⟨U, hU⟩ : Y.affineOpens) : Y.Opens).ι ''ᵁ ⊤)).hom := hf
rwa [Scheme.Opens.ι_image_top] at hf
· refine ⟨(h U U.2).1, ?_⟩
change Q (Scheme.Hom.app f ((U : Y.Opens).ι ''ᵁ ⊤)).hom
rw [Scheme.Opens.ι_image_top]
exact (h U U.2).2
