The polynomial commutant after localization #
An endomorphism of a localization which commutes with the coordinate
multiplications is multiplication by its value at 1. The argument only
uses the localization presentation; it does not use a finite-order
hypothesis.
theorem
AlgebraicAnalysis.DifferentialOperators.LocalizedPolynomialCommutant.eq_multiplication_of_commute_coordinate
{k : Type u_1}
[CommRing k]
{n : ℕ}
(B : Type u_2)
[CommRing B]
[Algebra k B]
[Algebra (MvPolynomial (Fin n) k) B]
[IsScalarTower k (MvPolynomial (Fin n) k) B]
(S : Submonoid (MvPolynomial (Fin n) k))
[IsLocalization S B]
(P : Module.End k B)
(hcoord :
∀ (i : Fin n) (b : B),
P ((algebraMap (MvPolynomial (Fin n) k) B) (MvPolynomial.X i) * b) = (algebraMap (MvPolynomial (Fin n) k) B) (MvPolynomial.X i) * P b)
: