English
There is a morphism of sheafifications induced by a pair of maps M₀ → M₀' and A → A' that satisfy a compatibility condition; this morphism makes the obvious square commute.
Русский
Существуют отображения между шейфайфицированными объектами, индуцируемые парами карт M₀ → M₀' и A → A' при условии совместимости; полученный морфизм формирует commutative diagram.
LaTeX
$$$\text{there exists }\mathrm{sheafifyMap}(\tau_0,\tau) : \mathrm{sheafify}(\alpha,\phi) \to \mathrm{sheafify}(\alpha,\phi') \text{ given } (\text{toPresheaf}(R_0).map \tau_0) \circ \phi' = \phi \circ \tau.$$$
Lean4
/-- The morphism of sheaves of modules `sheafify α φ ⟶ sheafify α φ'`
induced by morphisms `τ₀ : M₀ ⟶ M₀'` and `τ : A ⟶ A'`
which satisfy `τ₀.hom ≫ φ' = φ ≫ τ.val`. -/
@[simps]
noncomputable def sheafifyMap (fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.val) : sheafify α φ ⟶ sheafify α φ' where
val :=
homMk τ.val
(fun X r m ↦ by
let f := (sheafifyHomEquiv' α φ (by exact A'.cond)).symm (τ₀ ≫ toSheafify α φ')
suffices τ.val = (toPresheaf _).map f by simpa only [this] using (f.app X).hom.map_smul r m
apply ((J.W_of_isLocallyBijective φ).homEquiv _ A'.cond).injective
dsimp [f]
erw [comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom]
rw [← fac, Functor.map_comp, toPresheaf_map_toSheafify])
