English
Extensionality principle for locally full presheaves: if local data for maps j: Z→X and f:Z→Y agree after mapping, then global sections coincide, ensuring equality of sections in the target presheaf.
Русский
Принцип экстенсиональности для локально полных преповесов: если локальные данные согласуются после отображения, то секции равны.
LaTeX
$$$\forall Z\; (j:Z\to X)\ (f:Z\to Y),\ (G.map f) = (G.map j)\cdot i\ \Rightarrow\ ℱ.1.map (G.map j)^{op} s = ℱ.1.map (G.map j)^{op} t \Rightarrow s=t$$$
Lean4
theorem ext [G.IsLocallyFull K] (ℱ : Sheaf K (Type _)) {X Y : C} (i : G.obj X ⟶ G.obj Y)
{s t : ℱ.val.obj (op (G.obj X))}
(h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.1.map (G.map j).op s = ℱ.1.map (G.map j).op t) :
s = t :=
by
apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.cond) _ (G.functorPushforward_imageSieve_mem K i)).isSeparatedFor.ext
rintro Z _ ⟨W, iWX, iZW, ⟨iWY, e⟩, rfl⟩
simp [h iWX iWY e]
