English
There is a canonical Abelian category structure on the modules over a scheme, i.e., the fiber categories X.Modules form Abelian categories.
Русский
Существует каноническая абелева структура категорий модулей над схемой: X.Modules образуют абелевыe категории.
LaTeX
$$$\forall X:\mathrm{Scheme},\; \mathrm{Abelian}\, X.Modules.$$$
Lean4
theorem isUnit_toStalk (x : PrimeSpectrum.Top R) (r : x.asIdeal.primeCompl) :
IsUnit ((algebraMap R (Module.End R ((tildeInModuleCat M).stalk x))) r) :=
by
rw [Module.End.isUnit_iff]
refine
⟨LinearMap.ker_eq_bot.1 <| eq_bot_iff.2 fun st (h : r.1 • st = 0) ↦ smul_stalk_no_nonzero_divisor M r st h, fun st ↦
?_⟩
obtain ⟨U, mem, s, rfl⟩ := germ_exist (F := M.tildeInModuleCat) x st
let O := U ⊓ (PrimeSpectrum.basicOpen r)
refine
⟨germ M.tildeInModuleCat O x ⟨mem, r.2⟩
⟨fun q ↦ (Localization.mk 1 ⟨r, q.2.2⟩ : Localization.AtPrime q.1.asIdeal) • s.1 ⟨q.1, q.2.1⟩, fun q ↦ ?_⟩,
by
simpa only [Module.algebraMap_end_apply, ← map_smul] using
germ_ext (C := ModuleCat R) (W := O) (hxW := ⟨mem, r.2⟩) (iWU := 𝟙 _) (iWV := homOfLE inf_le_left) _ <|
Subtype.eq <| funext fun y ↦ smul_eq_iff_of_mem (S := y.1.1.primeCompl) r _ _ _ |>.2 rfl⟩
obtain ⟨V, mem_V, iV, num, den, hV⟩ := s.2 ⟨q.1, q.2.1⟩
refine ⟨V ⊓ O, ⟨mem_V, q.2⟩, homOfLE inf_le_right, num, r * den, fun y ↦ ?_⟩
obtain ⟨h1, h2⟩ := hV ⟨y, y.2.1⟩
refine ⟨y.1.asIdeal.primeCompl.mul_mem y.2.2.2 h1, ?_⟩
simp only [Opens.apply_def, isLocallyFraction_pred, mkLinearMap_apply,
smul_eq_iff_of_mem (S := y.1.1.primeCompl) (hr := h1), mk_smul_mk, one_smul, mul_one] at h2 ⊢
simpa only [h2, mk_smul_mk, one_smul, smul'_mk, mk_eq] using ⟨1, by simp only [one_smul]; rfl⟩
