Polynomial actions generated by a commuting family of endomorphisms

The target of MvPolynomial.aeval is required to be commutative. A family of pairwise commuting endomorphisms therefore gives an evaluation map by first landing in the commutative subalgebra which it generates.

noncomputable def AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialAction {k : Type u} [CommRing k] {V : Type v} [AddCommGroup V] [Module k V] {σ : Type w} (v : σ → Module.End k V) (hcomm : ∀ (i j : σ), Commute (v i) (v j)) : MvPolynomial σ k →ₐ[k] Module.End k V

Evaluation of multivariate polynomials at a pairwise commuting family of endomorphisms.

Equations

• AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialAction v hcomm = (Algebra.adjoin k (Set.range v)).val.comp (MvPolynomial.aeval fun (i : σ) => ⟨v i, ⋯⟩)

@[simp]

theorem AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialAction_apply_X {k : Type u} [CommRing k] {V : Type v} [AddCommGroup V] [Module k V] {σ : Type w} (v : σ → Module.End k V) (hcomm : ∀ (i j : σ), Commute (v i) (v j)) (i : σ) : (commutingPolynomialAction v hcomm) (MvPolynomial.X i) = v i

theorem AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialAction_apply_C {k : Type u} [CommRing k] {V : Type v} [AddCommGroup V] [Module k V] {σ : Type w} (v : σ → Module.End k V) (hcomm : ∀ (i j : σ), Commute (v i) (v j)) (a : k) : (commutingPolynomialAction v hcomm) (MvPolynomial.C a) = (algebraMap k (Module.End k V)) a

Evaluation sends constants to scalar endomorphisms. This named compatibility lemma is retained even though generic algebra-hom simplification can also discharge its left-hand side.

theorem AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialAction_intertwines {k : Type u} [CommRing k] {V : Type v} [AddCommGroup V] [Module k V] {σ : Type w} {W : Type z} [AddCommGroup W] [Module k W] (v : σ → Module.End k V) (w : σ → Module.End k W) (hv : ∀ (i j : σ), Commute (v i) (v j)) (hw : ∀ (i j : σ), Commute (w i) (w j)) (f : V →ₗ[k] W) (hgen : ∀ (i : σ), f ∘ₗ v i = w i ∘ₗ f) (p : MvPolynomial σ k) : f ∘ₗ (commutingPolynomialAction v hv) p = (commutingPolynomialAction w hw) p ∘ₗ f

@[instance_reducible]

noncomputable def AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialModule {k : Type u} [CommRing k] {V : Type v} [AddCommGroup V] [Module k V] {σ : Type w} (v : σ → Module.End k V) (hcomm : ∀ (i j : σ), Commute (v i) (v j)) : Module (MvPolynomial σ k) V

The polynomial action as a module structure on the original space.

Equations

• AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialModule v hcomm = Module.compHom V (AlgebraicAnalysis.CommutingPolynomialAction.commutingPolynomialAction v hcomm).toRingHom