English
The unit-map image under toPresheaf aligns with the canonical toSheafify map.
Русский
Изображение единицы через toPresheaf согласуется с каноническим отображением toSheafify.
LaTeX
$$$ (toPresheaf _).map ((sheafificationAdjunction α).unit.app M₀) = CategoryTheory.toSheafify J M₀.presheaf $$$
Lean4
theorem isCompatible_map_smul_aux {Y Z : C} (f : Y ⟶ X) (g : Z ⟶ Y) (r₀ : R₀.obj (Opposite.op Y))
(r₀' : R₀.obj (Opposite.op Z)) (m₀ : M₀.obj (Opposite.op Y)) (m₀' : M₀.obj (Opposite.op Z))
(hr₀ : α.app _ r₀ = R.map f.op r) (hr₀' : α.app _ r₀' = R.map (f.op ≫ g.op) r) (hm₀ : φ.app _ m₀ = A.map f.op m)
(hm₀' : φ.app _ m₀' = A.map (f.op ≫ g.op) m) : φ.app _ (M₀.map g.op (r₀ • m₀)) = φ.app _ (r₀' • m₀') :=
by
rw [← PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective α φ hA (R₀.map g.op r₀) r₀' (M₀.map g.op m₀) m₀',
M₀.map_smul]
· rw [hr₀', R.map_comp, RingCat.comp_apply, ← hr₀, ← RingCat.comp_apply, NatTrans.naturality, RingCat.comp_apply]
· rw [hm₀', A.map_comp, AddCommGrpCat.coe_comp, Function.comp_apply, ← hm₀]
erw [NatTrans.naturality_apply φ]
