English
If two germs of F at x coming from opens U and V agree, then there exists a common refinement W ⊆ U ∩ V with W ∈ B such that the corresponding restrictions of the sections to W map to equal elements after the appropriate maps F.map.
Русский
Если два гёрма F в точке x, полученные из открытий U и V, совпадают, существует обобщение W ⊆ U ∩ V с W ∈ B, такое что соответствующие ограничения секций на W отображаются в равные элементы через соответствующие отображения.
LaTeX
$$$\forall F: X\text{-Presheaf}, \forall U,V: Opens(X), x:\,X, s:\ToType(F.obj(op\ U)), t:\ToType(F.obj(op\ V)),\ F.germ(U,x,m_U,s)=F.germ(V,x,m_V,t) \Rightarrow \exists W\le U, W\le V, W\in B, F.map(homOfLE(W\le U)).op(s)=F.map(homOfLE(W\le V)).op(t)$$$
Lean4
theorem germ_eq_of_isBasis (F : X.Presheaf C) {U V : Opens X} (x : X) (mU : x ∈ U) (mV : x ∈ V)
{s : ToType (F.obj (op U))} {t : ToType (F.obj (op V))} (h : F.germ U x mU s = F.germ V x mV t) :
∃ (W : Opens X) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
F.map (homOfLE hWU).op s = F.map (homOfLE hWV).op t :=
by
obtain ⟨W, hxW, hWU, hWV, e⟩ := F.germ_eq x mU mV _ _ h
obtain ⟨_, ⟨W', hW', rfl⟩, hxW', hW'W⟩ := hB.exists_subset_of_mem_open hxW W.2
refine ⟨W', hxW', hW', hW'W.trans hWU.le, hW'W.trans hWV.le, ?_⟩
simpa only [← ConcreteCategory.comp_apply, ← F.map_comp] using
DFunLike.congr_arg (ConcreteCategory.hom (F.map (homOfLE hW'W).op)) e
