English
A convenient constructor for HasAffineProperty: HasAffineProperty P (affineAnd Q) is equivalent to checking P on morphisms with IsAffineHom and Q on affines.
Русский
Удобный конструктор HasAffineProperty: HasAffineProperty P (affineAnd Q) эквивалентно проверке P на морфизмах с IsAffineHom и Q на аффинных открытых множеств.
LaTeX
$$$\\text{HasAffineProperty } P (\\text{affineAnd}(Q)) \\iff \\forall X,Y,f, P f \\iff (IsAffineHom f \\land \\forall U, IsAffineOpen U \\to Q(f.app U).hom)$$$
Lean4
/-- A convenience constructor for `HasAffineProperty P (affineAnd Q)`. The `IsAffineHom` is bundled,
since this goes well with defining morphism properties via `extends IsAffineHom`. -/
theorem affineAnd_iff (P : MorphismProperty Scheme.{u}) (hQi : RingHom.RespectsIso Q)
(hQl : RingHom.LocalizationAwayPreserves Q) (hQs : RingHom.OfLocalizationSpan Q) :
HasAffineProperty P (affineAnd Q) ↔
∀ {X Y : Scheme.{u}} (f : X ⟶ Y), P f ↔ (IsAffineHom f ∧ ∀ U : Y.Opens, IsAffineOpen U → Q (f.app U).hom) :=
by
simp_rw [isAffineHom_iff]
refine ⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩
· rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
aesop
· ext X Y f
rw [targetAffineLocally_affineAnd_iff hQi, h f]
aesop
