English
For unary predicates P1, P2, P3 and a binary operation op, if P1 and P2 hold on respective sections and a refined compatibility p exists, then the composed predicate P3 holds after applying op to the sections.
Русский
Для предикатов P1, P2, P3 и двоичной операции op: если на соответствующих секциях выполняются P1 и P2 и существует совместимость, то после применения op к секциям получается P3.
LaTeX
$$$\\forall U,a,b, P_1.pred a \\land P_2.pred b \\Rightarrow \\forall p: (U)\\, \\exists W,i_U,i_V, p.1\\in W \\land P_3.pred (fun x => op (a (i_U x)) (b (i_V x))).$$$
Lean4
/-- For a binary operation (e.g. `x ↦ y ↦ x + y`) 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₁ T₂ T₃ : X → Type*} (P₁ : PrelocalPredicate T₁)
(P₂ : PrelocalPredicate T₂) (P₃ : PrelocalPredicate T₃) (op : {x : X} → T₁ x → T₂ x → T₃ x)
(hop :
∀ {U V : Opens X} {a : (x : U) → T₁ x} {b : (x : V) → T₂ x},
P₁.pred a →
P₂.pred b →
∀ (p : (U ⊓ V : Opens X)),
∃ (W : Opens X) (ia : W ⟶ U) (ib : W ⟶ V), p.1 ∈ W ∧ P₃.pred fun x : W ↦ op (a (ia x)) (b (ib x)))
{U : Opens X} {a : (x : U) → T₁ x} {b : (x : U) → T₂ x} (ha : P₁.sheafify.pred a) (hb : P₂.sheafify.pred b) :
P₃.sheafify.pred (fun x : U ↦ op (a x) (b x)) := by
intro x
rcases ha x with ⟨Va, ma, ia, ha⟩
rcases hb x with ⟨Vb, mb, ib, hb⟩
rcases hop ha hb ⟨x, ma, mb⟩ with ⟨W, sa, sb, hx, hw⟩
exact ⟨W, hx, sa ≫ ia, hw⟩
