English
There is a canonical instance showing that a presheaf IsLocallyFull property holds on a functor (e.g., identity on D) provided the underlying structure aligns with WEqualsLocallyBijective.
Русский
Существует стандартный экземпляр, доказывающий локальную полноту преповеса для определенного функторного контекста.
LaTeX
$$$[G\.WEqualsLocallyBijective D] \Rightarrow \text{IsLocallyFull } G$$$
Lean4
theorem ext [G.IsLocallyFaithful K] (ℱ : Sheaf K (Type _)) {X Y : C} (i₁ i₂ : X ⟶ Y) (e : G.map i₁ = G.map i₂)
{s t : ℱ.val.obj (op (G.obj X))}
(h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = 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_equalizer_mem K i₁ i₂ e)).isSeparatedFor.ext
rintro Z _ ⟨W, iWX, iZW, hiWX, rfl⟩
simp [h iWX hiWX]
