English
If two allowed sections agree at x on some neighborhood, they agree on a common refinement neighborhood.
Русский
Если две допустимые секции совпадают в точке x на некотором окне окружения, то они совпадают на общем дальнейшем окне.
LaTeX
$$$ w: (U,V, fU, fV, hU,hV, hEq) \\Rightarrow \\text{injectivity of } stalkToFiber$$$
Lean4
/-- The `stalkToFiber` map is injective at `x` if any two allowed sections which agree at `x`
agree on some neighborhood of `x`.
-/
theorem stalkToFiber_injective (P : LocalPredicate T) (x : X)
(w :
∀ (U V : OpenNhds x) (fU : ∀ y : U.1, T y) (_ : P.pred fU) (fV : ∀ y : V.1, T y) (_ : P.pred fV)
(_ : fU ⟨x, U.2⟩ = fV ⟨x, V.2⟩),
∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V), ∀ w : W.1, fU (iU w : U.1) = fV (iV w : V.1)) :
Function.Injective (stalkToFiber P x) := fun tU tV h ↦ by
-- We promise to provide all the ingredients of the proof later:
let Q :
∃ (W : (OpenNhds x)ᵒᵖ) (s : ∀ w : (unop W).1, T w) (hW : P.pred s),
tU = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ ∧
tV = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ :=
?_
· choose W s hW e using Q
exact e.1.trans e.2.symm
obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective' tU
obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective' tV
dsimp
simp only [stalkToFiber, Types.Colimit.ι_desc_apply] at h
specialize w (unop U) (unop V) fU hU fV hV h
rcases w with
⟨W, iU, iV, w⟩
-- and put it back together again in the correct order.
refine ⟨op W, fun w ↦ fU (iU w : (unop U).1), P.res ?_ _ hU, ?_⟩
· rcases W with ⟨W, m⟩
exact iU
· exact ⟨colimit_sound iU.op (Subtype.eq rfl), colimit_sound iV.op (Subtype.eq (funext w).symm)⟩
