English
If f : R → S is a ring homomorphism of finite presentation and s ⊆ Spec(S) is constructible, then comap f '' s is constructible in Spec(R).
Русский
Пусть f : R → S — гомоморфизм колец конечной презентации, и s ⊆ Spec(S) конструктивно. Тогда comap f '' sConstructible в Spec(R).
LaTeX
$$$f: R \\to S$ рационально порожденный, \\ f.FinitePresentation \\Rightarrow \\operatorname{IsConstructible}(s) \\Rightarrow \\operatorname{IsConstructible}(\\operatorname{comap} f '' s)$$$
Lean4
/-- **Chevalley's theorem**: If `f` is of finite presentation,
then the image of a constructible set under `Spec(f)` is constructible. -/
theorem isConstructible_comap_image {f : R →+* S} (hf : f.FinitePresentation) {s : Set (PrimeSpectrum S)}
(hs : IsConstructible s) : IsConstructible (comap f '' s) :=
by
refine
hf.polynomial_induction (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
(fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s)) (fun _ _ _ ↦ isConstructible_comap_C) ?_
?_ f s hs
· intro R _ S _ f hf hf' s hs
refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_
rw [range_comap_of_surjective _ f hf]
exact isRetrocompact_zeroLocus_compl_of_fg hf'
· intro R _ S _ T _ f g H₁ H₂ s hs
simp only [comap_comp, ContinuousMap.coe_comp, Set.image_comp]
exact H₁ _ (H₂ _ hs)
