unitHomEquiv — Mathlib

English

There is a canonical bijection between morphisms from the unit object to M and the global sections of M.

Русский

Существует каноническая биекция между морфизмами из единичного объекта в M и глобальными секциями M.

LaTeX

$$$\mathrm{Hom}(\mathrm{unit}_R, M) \cong \Gamma(M)$$$

Lean4

/-- The bijection `(unit R ⟶ M) ≃ M.sections` for `M : SheafOfModules R`. -/
noncomputable def unitHomEquiv (M : SheafOfModules R) : (unit R ⟶ M) ≃ M.sections :=
  (fullyFaithfulForget R).homEquiv.trans M.val.unitHomEquiv

Похожие утверждения