English
If germs agree locally at each iSup step, then the global equality holds.
Русский
Если гермы совпадают локально на каждом шаге iSup, то глобальное равенство имеет место.
LaTeX
$$$$\forall i, Eq( (F.obj U_i).germ, (F.obj V_i).germ ) \Rightarrow Eq(s,t).$$$$
Lean4
theorem germ_eq (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) (_m : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V), F.map iU.op s = F.map iV.op t :=
by
obtain ⟨W, iU, iV, e⟩ :=
(Types.FilteredColimit.isColimit_eq_iff.{v, v} _
(isColimitOfPreserves (forget C) (colimit.isColimit ((OpenNhds.inclusion x).op ⋙ F)))).mp
h
exact ⟨(unop W).1, (unop W).2, iU.unop, iV.unop, e⟩
