exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact

English

In a compact situation, a section of a presheaf restricted to a basic open is nilpotent iff it is trivial on the corresponding range, yielding a finite power annihilating the section.

Русский

В компактной обстановке секция пре-прешаба, ограниченная на базовый открытый, нильпотентна тогда и только тогда, когда она нулевой на соответствующем диапазоне, что приводит к существованию конечной степени, уничтожающей секцию.

LaTeX

$$$\\exists n:\\mathbb{N}, f^{n} \\cdot x = 0$ и эквивалентность по базовому открытому$$

Lean4

/-- If `x : Γ(X, U)` is zero on `D(f)` for some `f : Γ(X, U)`, and `U` is quasi-compact, then
`f ^ n * x = 0` for some `n`. -/
theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme.{u}) {U : X.Opens} (hU : IsCompact U.1)
    (x f : Γ(X, U)) (H : x |_ (X.basicOpen f) = 0) : ∃ n : ℕ, f ^ n * x = 0 :=
  by
  obtain ⟨s, hs, e⟩ := (isCompactOpen_iff_eq_finset_affine_union U.1).mp ⟨hU, U.2⟩
  replace e : U = iSup fun i : s => (i : X.Opens) := by ext1; simpa using e
  have h₁ (i : s) : i.1.1 ≤ U := by
    rw [e]
    exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
  have H' := fun i : s =>
    exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen X i.1.2 (X.presheaf.map (homOfLE (h₁ i)).op x)
      (X.presheaf.map (homOfLE (h₁ i)).op f) ?_
  swap
  · change (X.presheaf.map (homOfLE _).op) ((X.presheaf.map (homOfLE _).op).hom x) = 0
    have H : (X.presheaf.map (homOfLE _).op) x = 0 := H
    convert congr_arg (X.presheaf.map (homOfLE _).op).hom H
    · simp only [← CommRingCat.comp_apply, ← Functor.map_comp]
      · rfl
    · rw [map_zero]
    · simp only [Scheme.basicOpen_res, inf_le_right]
  choose n hn using H'
  haveI := hs.to_subtype
  cases nonempty_fintype s
  use Finset.univ.sup n
  suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0
    by
    subst e
    apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : X.Opens)
    intro i
    change _ = (X.sheaf.val.map _) 0
    rw [map_zero]
    apply this
  intro i
  replace hn := congr_arg (fun x => X.presheaf.map (homOfLE (h₁ i)).op (f ^ (Finset.univ.sup n - n i)) * x) (hn i)
  dsimp at hn
  simp only [← map_mul, ← map_pow] at hn
  rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn
  apply Finset.le_sup (Finset.mem_univ i)

Похожие утверждения