aeval_injective_iff_of_isEmpty — Mathlib

English

There is a canonical ring isomorphism between the polynomial algebra in no variables and the ground ring R when σ is empty.

Русский

Существет каноническое кольцевое изоморфизм между полиномами без переменных и основанием R при IsEmpty σ.

LaTeX

$$$\text{isEmptyRingEquiv} \;R\;\sigma : MvPolynomial\,\sigma\,R \cong+* R$ (при IsEmpty\,\sigma)$$

Lean4

@[simp]
theorem aeval_injective_iff_of_isEmpty [CommSemiring S₁] [Algebra R S₁] {f : σ → S₁} :
    Function.Injective (aeval f : MvPolynomial σ R →ₐ[R] S₁) ↔ Function.Injective (algebraMap R S₁) :=
  by
  have : aeval f = (Algebra.ofId R S₁).comp (@isEmptyAlgEquiv R σ _ _).toAlgHom :=
    by
    ext i
    exact IsEmpty.elim' ‹IsEmpty σ› i
  rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]
  rfl

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