English
If f: X → Y is open, injective on the base map, and appTop injective, then the stalk maps are injective for all x.
Русский
Если f открытое отображение и инъективно на уровне базовых отображений и на уровне appTop, то стебельные отображения инъективны.
LaTeX
$$$IsOpenMap(f.base) \\land IsInjective(f.base) \\land IsInjective(f.appTop) \\Rightarrow \\forall x, IsInjective(f.stalkMap\,x)$$$
Lean4
/-- If `f : X ⟶ Y` is open, injective, `X` is quasi-compact and `Y` is affine, then `f` is stalkwise
injective if it is injective on global sections. -/
theorem stalkMap_injective_of_isOpenMap_of_injective [CompactSpace X] (hfopen : IsOpenMap f.base)
(hfinj₁ : Function.Injective f.base) (hfinj₂ : Function.Injective (f.appTop)) (x : X) :
Function.Injective (f.stalkMap x) := by
let φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := f.appTop
let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover
let res (i : 𝒰.I₀) : Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := (𝒰.f i).appTop
refine stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) h ↦ ?_)
rw [TopCat.Presheaf.Γgerm, Scheme.stalkMap_germ_apply] at h
obtain ⟨U, w, (hx : x ∈ U), hg⟩ := X.toRingedSpace.exists_res_eq_zero_of_germ_eq_zero ⊤ (φ g) ⟨x, trivial⟩ h
obtain ⟨_, ⟨s, rfl⟩, hyv, bsle⟩ :=
Opens.isBasis_iff_nbhd.mp (isBasis_basicOpen Y)
(show f.base x ∈ ⟨f.base '' U.carrier, hfopen U.carrier U.is_open'⟩ from ⟨x, by simpa⟩)
let W (i : 𝒰.I₀) : TopologicalSpace.Opens (𝒰.X i) := (𝒰.X i).basicOpen ((res i) (φ s))
have hwle (i : 𝒰.I₀) : W i ≤ (𝒰.f i) ⁻¹ᵁ U :=
by
change (𝒰.X i).basicOpen ((𝒰.f i ≫ f).appTop s) ≤ _
rw [← Scheme.preimage_basicOpen_top, Scheme.comp_coeBase, Opens.map_comp_obj]
refine Scheme.Hom.preimage_le_preimage_of_le _ (le_trans (f.preimage_le_preimage_of_le bsle) (le_of_eq ?_))
simp [Set.preimage_image_eq _ hfinj₁]
have h0 (i : 𝒰.I₀) : (𝒰.f i).appLE _ (W i) (by simp) (φ g) = 0 :=
by
rw [← Scheme.Hom.appLE_map _ ((Opens.map _).map w).le (homOfLE <| hwle i).op, ← Scheme.Hom.map_appLE _ le_rfl w.op]
simp only [CommRingCat.comp_apply]
rw [hg]
simp only [map_zero]
have h1 (i : 𝒰.I₀) : ∃ n, (res i) (φ (s ^ n * g)) = 0 :=
by
obtain ⟨n, hn⟩ := exists_of_res_zero_of_qcqs_of_top (s := ((res i) (φ s))) (h0 i)
exact ⟨n, by rwa [map_mul, map_mul, map_pow, map_pow]⟩
have h2 : ∃ n, ∀ i, (res i) (φ (s ^ n * g)) = 0 :=
by
choose fn hfn using h1
refine ⟨Finset.sup Finset.univ fn, fun i ↦ ?_⟩
rw [map_mul, map_pow, map_mul, map_pow]
simp only [map_mul, map_pow, map_mul, map_pow] at hfn
apply pow_mul_eq_zero_of_le (Finset.le_sup (Finset.mem_univ i)) (hfn i)
obtain ⟨n, hn⟩ := h2
apply germ_eq_zero_of_pow_mul_eq_zero (U := ⊤) ⟨f.base x, trivial⟩ hyv
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at hfinj₂
exact hfinj₂ _ (Scheme.zero_of_zero_cover _ _ hn)
