English
For an ideal data I on Y and a morphism f: X → Y, the inverse comapIso interacts with the subscheme embedding to realize the pullback of I along f as a subscheme on X.
Русский
Для данных идеала I на Y и морфизма f: X → Y обратная совместная композиция comapIso с subschemeι реализует вытяжку I вдоль f как подпроизвольный подпроизведение на X.
LaTeX
$$$(I.comapIso f).inv \cdot (I.comap f).subschemeι = \text{pullback.fst } _ _$$$
Lean4
theorem support_ker (f : X.Hom Y) [QuasiCompact f] : f.ker.support = closure (Set.range f.base) :=
by
apply subset_antisymm
· wlog hY : ∃ S, Y = Spec S
· intro x hx
let 𝒰 := Y.affineCover
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
have inst : QuasiCompact (𝒰.pullbackHom f i) := MorphismProperty.pullback_snd _ _ inferInstance
have :=
this (𝒰.pullbackHom f i) ⟨_, rfl⟩ ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
· have := image_closure_subset_closure_image (f := (𝒰.f i).base) (𝒰.f i).base.1.2 (Set.mem_image_of_mem _ this)
rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, 𝒰.pullbackHom_map] at this
exact closure_mono (Set.range_comp_subset_range _ _) this
· rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i) ((𝒰.pullback₁ f).f i) (𝒰.f i),
Ideal.coe_comap, Set.image_preimage_eq]
· exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
· exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2
· exact (IsPullback.of_hasPullback _ _).flip
obtain ⟨S, rfl⟩ := hY
wlog hX : ∃ R, X = Spec R generalizing X S
· intro x hx
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
let 𝒰 := X.affineCover.finiteSubcover
obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx
have inst : QuasiCompact (𝒰.f i ≫ f) :=
HasAffineProperty.iff_of_isAffine.mpr (by change CompactSpace (Spec _); infer_instance)
exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)
obtain ⟨R, rfl⟩ := hX
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
rw [ker_of_isAffine, coe_support_ofIdealTop, Spec_zeroLocus, ← Ideal.coe_comap, RingHom.comap_ker, ←
PrimeSpectrum.closure_range_comap, ← CommRingCat.hom_comp, ← Scheme.ΓSpecIso_inv_naturality]
simp only [CommRingCat.hom_comp, PrimeSpectrum.comap_comp, ContinuousMap.coe_comp]
exact closure_mono (Set.range_comp_subset_range _ (Spec.map φ).base)
· rw [(support _).isClosed.closure_subset_iff]
exact f.range_subset_ker_support
