English
Let X be reduced and s a section on an open U. If the basic open of s is empty, then s equals zero.
Русский
Пусть X редуцированная схема и s секция на открытом U. Если базовое открытие s пусто, то s равно нулю.
LaTeX
$$$[IsReduced] \Rightarrow X.basicOpen(s) = \emptyset \Rightarrow s = 0$$$
Lean4
theorem eq_zero_of_basicOpen_eq_bot {X : Scheme} [hX : IsReduced X] {U : X.Opens} (s : Γ(X, U))
(hs : X.basicOpen s = ⊥) : s = 0 :=
by
apply TopCat.Presheaf.section_ext X.sheaf U
intro x hx
change (X.sheaf.presheaf.germ U x hx) s = (X.sheaf.presheaf.germ U x hx) 0
rw [RingHom.map_zero]
induction U using reduce_to_affine_global generalizing hX with
| h₁ X U H =>
obtain ⟨V, hx, i, H⟩ := H ⟨x, hx⟩
specialize H (X.presheaf.map i.op s)
rw [Scheme.basicOpen_res, hs] at H
specialize H (inf_bot_eq _) x hx
rw [← X.sheaf.presheaf.germ_res_apply i x hx s]
exact H
| h₂ X Y f =>
refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by simp, rfl, ?_⟩
rintro H hX s hs _ ⟨x, rfl⟩
haveI := isReduced_of_isOpenImmersion f
specialize H (f.app _ s) _ x ⟨x, rfl⟩
· rw [← Scheme.preimage_basicOpen, hs]; ext1; simp [Opens.map]
· have H : (X.presheaf.germ _ x _).hom _ = 0 := H
rw [← Scheme.stalkMap_germ_apply f ⟨_, _⟩ x] at H
apply_fun inv <| f.stalkMap x at H
rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] at H
exact H
| h₃ R =>
rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs
replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero
rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs
rw [hs, map_zero]
