unit — Mathlib

English

There is a canonical rank-1 free sheaf of modules, the unit object, in the category of sheaves of modules.

Русский

Существует канонический свободный пучок модулей ранга 1, объект единицы, в категории пучков модулей.

LaTeX

$$$\mathrm{rk}(\mathrm{unit}_R) = 1$$$

Lean4

/-- The obvious free sheaf of modules of rank `1`. -/
@[simps]
noncomputable def unit : SheafOfModules R
    where
  val := PresheafOfModules.unit R.val
  isSheaf := ((sheafCompose J (forget₂ RingCat.{u} AddCommGrpCat.{u})).obj R).cond

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