basicOpen_eq_bot_of_isNilpotent — Mathlib

English

If a section f is nilpotent in the structure presheaf, then the basic open defined by f is the bottom element.

Русский

Если секция f является nilpotent в предsheaf‑структуры, то базовое открытое, заданное f, является нижним элементом.

LaTeX

$$$$X^{\\mathrm{toRingedSpace}}.basicOpen f = \\bot\\quad\\text{если } f \\text{ nilpotent}$$$$

Lean4

@[simp]
theorem basicOpen_eq_bot_of_isNilpotent (X : LocallyRingedSpace.{u}) (U : Opens X.carrier)
    (f : (X.presheaf.obj <| op U)) (hf : IsNilpotent f) : X.toRingedSpace.basicOpen f = ⊥ :=
  by
  obtain ⟨n, hn⟩ := hf
  cases n.eq_zero_or_pos with
  | inr h =>
    rw [← X.toRingedSpace.basicOpen_pow f n h, hn]
    simp [basicOpen_zero]
  | inl h =>
    rw [h, pow_zero] at hn
    simp [eq_zero_of_zero_eq_one hn.symm f, basicOpen_zero]

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