freeSection — Mathlib

English

The freeSection i is the tautological section of the free I at i; it picks out the i-th copy of R inside the free object.

Русский

freeSection i — это тождественный срез свободного объекта по i; он выбирает i-ую копию R внутри свободного объекта.

LaTeX

$$$\text{freeSection} (i) : (\mathrm{free} I).\text{sections}$$$

Lean4

/-- The tautological section of `free I : SheafOfModules R` corresponding to `i : I`. -/
noncomputable abbrev freeSection {I : Type u} (i : I) : (free (R := R) I).sections :=
  (free (R := R) I).freeHomEquiv (𝟙 (free I)) i

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