quasicoherentDataOfIsFinitePresentation

English

For i in the presentation, the generators form a finite set.

Русский

Для i из презентации генераторы образуют конечное множество.

LaTeX

$$$\text{Finite}\ (\mathrm{presentation}_{i}.\mathrm{generators}.I)$$$

Lean4

/-- A choice of local presentations when `M` is a sheaf of modules of finite presentation. -/
noncomputable def quasicoherentDataOfIsFinitePresentation : M.QuasicoherentData :=
  h.exists_quasicoherentData.choose

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