English
There is an equivalence between morphisms from the unit presheaf to M and sections of M.
Русский
Существует эквивалентность между морфизмами из единичного прешефа в M и секциями M.
LaTeX
$$$ unitR ⟶ M \simeq M.sections $$$
Lean4
/-- The bijection `(unit R ⟶ M) ≃ M.sections` for `M : PresheafOfModules R`. -/
@[simps! apply_coe]
noncomputable def unitHomEquiv (M : PresheafOfModules R) : (unit R ⟶ M) ≃ M.sections
where
toFun f := sectionsMk (fun X ↦ Hom.app f X (1 : R.obj X)) (by intros; rw [← naturality_apply, unit_map_one])
invFun
s :=
{ app := fun X ↦ ModuleCat.ofHom ((LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).symm (s.val X))
naturality := fun {X Y} f ↦ by
ext
dsimp
change R.map f 1 • s.eval Y = M.map f (1 • s.eval X)
simp }
left_inv
f := by
ext X : 2
exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).symm_apply_apply (f.app X).hom
right_inv
s := by
ext X
exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).apply_symm_apply (s.val X)
