π — Mathlib · SciLib

English

For a finite-type sheaf M, π(σ) is the epimorphism from the free σ.I to M given by the generating sections σ.

Русский

Для конечного типа M отображение π(σ) — эпиморфизм из свободной части σ.I в M, задаваемый порождающими секциями σ.

LaTeX

$$$\pi(σ) : \mathrm{free}\, σ.I \twoheadrightarrow M$$$

Lean4

/-- The epimorphism `free σ.I ⟶ M` given by `σ : M.GeneratingSections`. -/
noncomputable abbrev π (σ : M.GeneratingSections) : free σ.I ⟶ M :=
  M.freeHomEquiv.symm σ.s

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