English
If a prelocal predicate P is closed under a unary operation op on each open set by a refinement property hop, then the sheafified predicate is closed under op on any open set.
Русский
Если предлокальное предикат P замкнут относительно унарной операции op на каждом открытом множестве по свойству уточнения, то предикат, получаемый после шарлификации, также замкнут относительно op.
LaTeX
$$$\\text{If } Hop: ∀{U,a}, P.pred a → ∀ p: U, ∃ W,i, p.1 ∈ W ∧ P.pred (fun x ∈ W ↦ op (a (i x))). \\; \\Rightarrow \\; P.sheafify.pred (fun x \\mapsto op (a x)).$$$
Lean4
/-- For a unary operation (e.g. `x ↦ -x`) defined at each stalk, if a prelocal predicate is closed
under the operation on each open set (possibly by refinement), then the sheafified predicate is
also closed under the operation. See `sheafify_inductionOn'` for the version without refinement. -/
theorem sheafify_inductionOn {X : TopCat} {T : X → Type*} (P : PrelocalPredicate T) (op : {x : X} → T x → T x)
(hop :
∀ {U : Opens X} {a : (x : U) → T x},
P.pred a → ∀ (p : U), ∃ (W : Opens X) (i : W ⟶ U), p.1 ∈ W ∧ P.pred fun x : W ↦ op (a (i x)))
{U : Opens X} {a : (x : U) → T x} (ha : P.sheafify.pred a) : P.sheafify.pred (fun x : U ↦ op (a x)) :=
by
intro x
rcases ha x with ⟨Va, ma, ia, ha⟩
rcases hop ha ⟨x, ma⟩ with ⟨W, sa, hx, hw⟩
exact ⟨W, hx, sa ≫ ia, hw⟩
