English
A bundled version of the previous equivalence: targetAffineLocally(affineAnd(Q)) holds exactly when IsAffineHom f holds and Q holds on all restrictions to affine opens.
Русский
Упакованная версия предыдущего эквивалентности: targetAffineLocally(affineAnd(Q)) верно тогда и только тогда IsAffineHom(f) и Q выполняются на ограничениях к аффинным открытым множествам.
LaTeX
$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q))\\,f \\iff \\bigl(\\operatorname{IsAffineHom}(f) \\land \\forall U\\,(\\operatorname{IsAffineOpen}(U) \to Q(f.app U).hom)\\bigr)$$$
Lean4
/-- Variant of `targetAffineLocally_affineAnd_iff` where `IsAffineHom` is bundled. -/
theorem targetAffineLocally_affineAnd_iff' (hQi : RingHom.RespectsIso Q) {X Y : Scheme.{u}} (f : X ⟶ Y) :
targetAffineLocally (affineAnd Q) f ↔ IsAffineHom f ∧ ∀ U : Y.Opens, IsAffineOpen U → Q (f.app U).hom :=
by
rw [targetAffineLocally_affineAnd_iff hQi, isAffineHom_iff]
aesop
