English
Chevalley’s theorem: image of a locally constructible set under a morphism of finite presentation into a qcqs scheme is locally constructible.
Русский
Чева́лье: образ локально конструктивного множества под морфизмом с конечной презентацией в qcqs-множество локально конструктивен.
LaTeX
$$$\text{IsLocallyConstructible}(f.base'' s) \text{ under LocallyOfFinitePresentation and qcqs }$$$
Lean4
/-- **Chevalley's Theorem**: The image of a locally constructible set under a
morphism of finite presentation is locally constructible. -/
@[stacks 054K]
-- `nonrec` is needed for `wlog`
nonrec theorem isLocallyConstructible_image (f : X.Hom Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f]
{s : Set X} (hs : IsLocallyConstructible s) : IsLocallyConstructible (f.base '' s) :=
by
wlog hY : ∃ R, Y = Spec R
· refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_
have inst : LocallyOfFinitePresentation (Y.affineCover.pullbackHom f i) :=
MorphismProperty.pullback_snd _ _ inferInstance
have inst : QuasiCompact (Y.affineCover.pullbackHom f i) := MorphismProperty.pullback_snd _ _ inferInstance
convert
(this (Y.affineCover.pullbackHom f i)
(hs.preimage_of_isOpenEmbedding ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding)
⟨_, rfl⟩).preimage_of_isOpenEmbedding
(Y.affineCover.f i).isoOpensRange.inv.isOpenEmbedding
refine .trans ?_ ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage _)
apply Set.image_injective.mpr Subtype.val_injective
rw [Set.image_preimage_eq_inter_range, ← Set.image_comp, ← Set.image_comp, Subtype.range_coe_subtype,
Set.setOf_mem_eq]
change _ = (Y.affineCover.pullbackHom f i ≫ (Y.affineCover.f i).isoOpensRange.hom ≫ Opens.ι _).base.hom '' _
rw [Scheme.Hom.isoOpensRange_hom_ι, Cover.pullbackHom_map, Scheme.comp_base, TopCat.hom_comp,
ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range]
simp [IsOpenImmersion.range_pullback_fst_of_right, Set.image_inter_preimage]
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S
· have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
let 𝒰 := X.affineCover.finiteSubcover
rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]
refine .iUnion fun i ↦ ?_
have inst : QuasiCompact (𝒰.f i ≫ f) :=
HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
convert this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩
rw [Scheme.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp, ContinuousMap.coe_comp, Set.image_comp,
Set.image_preimage_eq_inter_range, coe_opensRange]
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)] at hf
exact (PrimeSpectrum.isConstructible_comap_image hf hs.isConstructible).isLocallyConstructible
