English
For every x ∈ X, the canonical stalk-to-fiber map F.stalkToFiber x is injective; i.e., two germs in the stalk that agree when evaluated on overlaps must be equal.
Русский
Для каждой точки x ∈ X каноническое отображение стека в стек F стека x инективно; то есть два герма, совпадающих на пересечениях, равны.
LaTeX
$$$\forall x, F.stalkToFiber x \text{ is injective}.$$$
Lean4
theorem stalkToFiber_injective (x : X) : Function.Injective (F.stalkToFiber x) :=
by
apply TopCat.stalkToFiber_injective
intro U V fU hU fV hV e
rcases hU ⟨x, U.2⟩ with ⟨U', mU, iU, gU, wU⟩
rcases hV ⟨x, V.2⟩ with ⟨V', mV, iV, gV, wV⟩
have wUx := wU ⟨x, mU⟩
dsimp at wUx; rw [wUx] at e; clear wUx
have wVx := wV ⟨x, mV⟩
dsimp at wVx; rw [wVx] at e; clear wVx
rcases F.germ_eq x mU mV gU gV e with ⟨W, mW, iU', iV', (e' : F.map iU'.op gU = F.map iV'.op gV)⟩
use ⟨W ⊓ (U' ⊓ V'), ⟨mW, mU, mV⟩⟩
refine ⟨?_, ?_, ?_⟩
· change W ⊓ (U' ⊓ V') ⟶ U.obj
exact Opens.infLERight _ _ ≫ Opens.infLELeft _ _ ≫ iU
· change W ⊓ (U' ⊓ V') ⟶ V.obj
exact Opens.infLERight _ _ ≫ Opens.infLERight _ _ ≫ iV
· intro w
specialize wU ⟨w.1, w.2.2.1⟩
specialize wV ⟨w.1, w.2.2.2⟩
refine wU.trans <| .trans ?_ wV.symm
rw [← F.germ_res iU' w w.2.1, ← F.germ_res iV' w w.2.1, CategoryTheory.types_comp_apply,
CategoryTheory.types_comp_apply, e']
