English
For an injective f with hf, killCompl hf is the R-algebra hom from MvPolynomial τ R to MvPolynomial σ R that is left inverse to rename f and sends variables outside range f to 0.
Русский
Для инъективного f с hf, killCompl hf — это R-алгебровое отображение MvPolynomial τ R → MvPolynomial σ R, являющееся левым обратным к rename f и отправляющее переменные за пределами образа f в 0.
LaTeX
$$$\\text{killCompl } hf: MvPolynomial(\\tau,R) \\to MvPolynomial(\\sigma,R) \\text{ — левый обратный к } \\text{rename}_f \\text{ и обнуляет переменные вне образа } f.$$$
Lean4
/-- Given a function between sets of variables `f : σ → τ` that is injective with proof `hf`,
`MvPolynomial.killCompl hf` is the `AlgHom` from `R[τ]` to `R[σ]` that is left inverse to
`rename f : R[σ] → R[τ]` and sends the variables in the complement of the range of `f` to `0`. -/
def killCompl : MvPolynomial τ R →ₐ[R] MvPolynomial σ R :=
aeval fun i => if h : i ∈ Set.range f then X <| (Equiv.ofInjective f hf).symm ⟨i, h⟩ else 0
