optionEquivRight — Mathlib

English

There exists an algebra isomorphism between multivariable polynomials in option variables and polynomials in variables indexed by S1 with polynomial coefficients, i.e., an isomorphism optionEquivRight : MvPolynomial(Option S1) R ≅ MvPolynomial S1 (Polynomial R).

Русский

Существует алгебраическое изоморфизм между многочленами с переменными в виде опций и многочленами в переменных S1 с коэффициентами, являющимися полиномами над R.

LaTeX

$$$\\operatorname{optionEquivRight} : \\operatorname{MvPolynomial}(\\operatorname{Option} S_1) R \\cong_R \\operatorname{MvPolynomial}(S_1) (R[X]).$$$

Lean4

/-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
multivariable polynomials with coefficients in polynomials.
-/
@[simps!]
def optionEquivRight : MvPolynomial (Option S₁) R ≃ₐ[R] MvPolynomial S₁ R[X] :=
  AlgEquiv.ofAlgHom (MvPolynomial.aeval fun o => o.elim (C Polynomial.X) X)
    (MvPolynomial.aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
    (by
      ext : 2 <;>
        simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp,
          IsScalarTower.coe_toAlgHom', comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X, aevalTower_X,
          AlgHom.coe_id, id])
    (by
      ext ⟨i⟩ : 2 <;>
        simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C, Polynomial.aeval_X, AlgHom.coe_id,
          id, aevalTower_X])

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