English
Let α be a type and s ⊆ α. There is a natural restriction map restriction_s: FreeCommRing(α) → FreeCommRing(s) which sends each generator a ∈ α to 0 if a ∉ s, and to the corresponding generator in FreeCommRing(s) if a ∈ s.
Русский
Пусть α — множество; пусть s ⊆ α. Существует естественное отображение ограничения restriction_s: FreeCommRing(α) → FreeCommRing(s), которое переводит каждый генератор a ∈ α в 0, если a ∉ s, либо в соответствующий генератор в FreeCommRing(s), если a ∈ s.
LaTeX
$$$\\restriction_s : \\mathrm{FreeCommRing}(\\alpha) \\to^+_* \\mathrm{FreeCommRing}(s), \\\\\\restriction_s(\\mathrm{of}(a)) = \\begin{cases} \\mathrm{of}\\langle a, H\\rangle, & a \\in s \\\\ 0, & a \\notin s \\end{cases}$$$
Lean4
/-- The restriction map from `FreeCommRing α` to `FreeCommRing s` where `s : Set α`, defined
by sending all variables not in `s` to zero. -/
def restriction (s : Set α) [DecidablePred (· ∈ s)] : FreeCommRing α →+* FreeCommRing s :=
lift (fun a => if H : a ∈ s then of ⟨a, H⟩ else 0)
