English
The unit component of the adjunction at M₀ corresponds to the canonical Sheafify-toSheaf morphism.
Русский
Единица адъункции на M₀ совпадает с каноническим отображением Sheafify-toSheaf.
LaTeX
$$$ (toPresheaf _).map ((sheafificationAdjunction α).unit.app M₀) = CategoryTheory.toSheafify J M₀.presheaf $$$
Lean4
theorem _root_.PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective {Y : C} (r₀ r₀' : R₀.obj (Opposite.op Y))
(m₀ m₀' : M₀.obj (Opposite.op Y)) (hr₀ : α.app _ r₀ = α.app _ r₀') (hm₀ : φ.app _ m₀ = φ.app _ m₀') :
φ.app _ (r₀ • m₀) = φ.app _ (r₀' • m₀') :=
by
apply hA _ (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve (F := M₀.presheaf) m₀ m₀')
· apply J.intersection_covering
· exact Presheaf.equalizerSieve_mem J α _ _ hr₀
· exact Presheaf.equalizerSieve_mem J φ _ _ hm₀
· intro Z g hg
rw [← NatTrans.naturality_apply (D := Ab), ← NatTrans.naturality_apply (D := Ab)]
erw [M₀.map_smul, M₀.map_smul, hg.1, hg.2]
rfl
