English
If the restriction of a global section to each member of a finite open cover is nilpotent, then the section itself is nilpotent.
Русский
Если ограничение глобальной секции к каждому члену конечного открытого покрытия является нилпотентным, то сама секция нилпотентна.
LaTeX
$$$$ \text{If } \forall i, IsNilpotent(\mathcal{U}.f i \;\text{on } s), \text{ then } IsNilpotent(s). $$$$
Lean4
/-- If a global section is nilpotent on each member of a finite open cover, then `f` is
nilpotent. -/
theorem isNilpotent_of_isNilpotent_cover {X : Scheme.{u}} {U : X.Opens} (s : Γ(X, U)) (𝒰 : X.OpenCover) [Finite 𝒰.I₀]
(h : ∀ i : 𝒰.I₀, IsNilpotent ((𝒰.f i).app U s)) : IsNilpotent s :=
by
choose fn hfn using h
have : Fintype 𝒰.I₀ := Fintype.ofFinite 𝒰.I₀
let N : ℕ := Finset.sup Finset.univ fn
have hfnleN (i : 𝒰.I₀) : fn i ≤ N := Finset.le_sup (Finset.mem_univ i)
use N
apply zero_of_zero_cover (𝒰 := 𝒰)
on_goal 1 => intro i;
simp only [map_pow]
-- This closes both remaining goals at once.
exact pow_eq_zero_of_le (hfnleN i) (hfn i)
