English
Chevalley-type result: image of a locally constructible set under a finite presentation morphism into a qcqs scheme is locally constructible.
Русский
По Чева́льли: образ локально-конструктивной множества при отображении конечной презентации в qcqs-множество — локально-конструктивен.
LaTeX
$$$\text{IsLocallyConstructible}(f.base '' s) \text{ under hypotheses }[LocallyOfFinitePresentation f]\text{ and qcqs }$$$
Lean4
instance : HasRingHomProperty (@LocallyOfFinitePresentation) RingHom.FinitePresentation
where
isLocal_ringHomProperty := RingHom.finitePresentation_isLocal
eq_affineLocally' := by
ext X Y f
rw [locallyOfFinitePresentation_iff, affineLocally_iff_affineOpens_le]
