English
There is a natural equivalence between morphisms from a free sheaf on I to M and functions I → M.sections.
Русский
Существует естественное эквивалентное отображение между морфизмами из свободной шары в M и функциями I → разделы M.
LaTeX
$$$(\mathrm{free}\, I \to M) \simeq (I \to M.{\text{sections}})$$$
Lean4
/-- The data of a morphism `free I ⟶ M` from a free sheaf of modules is
equivalent to the data of a family `I → M.sections` of sections of `M`. -/
noncomputable def freeHomEquiv (M : SheafOfModules.{u} R) {I : Type u} : (free I ⟶ M) ≃ (I → M.sections)
where
toFun f i := M.unitHomEquiv (Sigma.ι (fun (_ : I) ↦ unit R) i ≫ f)
invFun s := Sigma.desc (fun i ↦ M.unitHomEquiv.symm (s i))
left_inv s := Sigma.hom_ext _ _ (by simp)
right_inv f := by ext1 i; simp
