English
If M1 → M2 is a morphism of presheaves and α is locally surjective, and M2 is a sheaf, then restricting scalars along α yields a bijection between morphisms M1 → M2 and morphisms (restrictScalars α)M1 → (restrictScalars α)M2.
Русский
Если M1 → M2 — морфизм прешеаф, α локально сюръективен, и M2 — онащ, то ограничение скаляров по α устанавливает биекцию между морфизмами M1 → M2 и морфизмами (restrictScalars α)M1 → (restrictScalars α)M2.
LaTeX
$$$(M_1 \to M_2) \ \simeq\ \big((\operatorname{restrictScalars}(\alpha))M_1 \to (\operatorname{restrictScalars}(\alpha))M_2\big)$$$
Lean4
/-- The functor `PresheafOfModules.restrictScalars α` induces bijections on
morphisms if `α` is locally surjective and the target presheaf is a sheaf. -/
noncomputable def restrictHomEquivOfIsLocallySurjective (hM₂ : Presheaf.IsSheaf J M₂.presheaf)
[Presheaf.IsLocallySurjective J α] : (M₁ ⟶ M₂) ≃ ((restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂)
where
toFun f := (restrictScalars α).map f
invFun
g :=
homMk ((toPresheaf R).map g)
(fun X r' m ↦ by
apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')
rintro Y p ⟨r : R.obj _, hr⟩
have hg : ∀ (z : M₁.obj X), g.app _ (M₁.map p.op z) = M₂.map p.op (g.app X z) := fun z ↦
CategoryTheory.congr_fun (g.naturality p.op) z
change M₂.map p.op (g.app X (r' • m)) = M₂.map p.op (r' • show M₂.obj X from g.app X m)
dsimp at hg ⊢
rw [← hg, M₂.map_smul, ← hg, ← hr]
erw [← (g.app _).hom.map_smul]
rw [M₁.map_smul, ← hr]
rfl)
