Mathlib.Algebra.Polynomial.GroupRingAction

Polynomial.smul_eq_map theorem

[MulSemiringAction M R] (m : M) : HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

Full source

theorem smul_eq_map [MulSemiringAction M R] (m : M) :
    HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m) := by
  suffices DistribMulAction.toAddMonoidHom R[X] m =
      (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom by
    ext1 r
    exact DFunLike.congr_fun this r
  ext n r : 2
  change m • monomial n r = map (MulSemiringAction.toRingHom M R m) (monomial n r)
  rw [Polynomial.map_monomial, Polynomial.smul_monomial, MulSemiringAction.toRingHom_apply]

Scalar Multiplication on Polynomials via Semiring Homomorphism

Informal description

For any monoid $M$ with a multiplicative semiring action on a semiring $R$, and for any element $m \in M$, the scalar multiplication action of $m$ on a polynomial $p \in R[X]$ is equal to applying the polynomial map induced by the semiring homomorphism associated to $m$ to $p$. In mathematical notation: $$m \cdot p = \text{map}(\phi_m)(p)$$ where $\phi_m : R \to R$ is the semiring homomorphism induced by $m$.

Polynomial.instMulSemiringAction instance

[MulSemiringAction M R] : MulSemiringAction M R[X]

Full source

noncomputable instance [MulSemiringAction M R] : MulSemiringAction M R[X] :=
  { Polynomial.distribMulAction with
    smul_one := fun m ↦
      smul_eq_map R m ▸ Polynomial.map_one (MulSemiringAction.toRingHom M R m)
    smul_mul := fun m _ _ ↦
      smul_eq_map R m ▸ Polynomial.map_mul (MulSemiringAction.toRingHom M R m) }

Multiplicative Semiring Action on Polynomial Rings

Informal description

For any monoid $M$ with a multiplicative semiring action on a semiring $R$, the polynomial ring $R[X]$ inherits a multiplicative semiring action from $M$. This action is defined such that for any $m \in M$ and polynomial $p \in R[X]$, the action $m \cdot p$ is given by applying the semiring homomorphism associated to $m$ to each coefficient of $p$.

Polynomial.smul_X theorem

(m : M) : (m • X : R[X]) = X

Full source

@[simp]
theorem smul_X (m : M) : (m • X : R[X]) = X :=
  (smul_eq_map R m).symm ▸ map_X _

Invariance of Polynomial Variable under Scalar Multiplication: $m \cdot X = X$

Informal description

For any element $m$ of a monoid $M$ acting multiplicatively on a semiring $R$, the scalar multiplication of $m$ with the polynomial variable $X$ in $R[X]$ is equal to $X$ itself, i.e., $m \cdot X = X$.

Polynomial.smul_eval_smul theorem

(m : M) (f : S[X]) (x : S) : (m • f).eval (m • x) = m • f.eval x

Full source

theorem smul_eval_smul (m : M) (f : S[X]) (x : S) : (m • f).eval (m • x) = m • f.eval x :=
  Polynomial.induction_on f (fun r ↦ by rw [smul_C, eval_C, eval_C])
    (fun f g ihf ihg ↦ by rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]) fun n r _ ↦ by
    rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X, eval_mul, eval_C,
      eval_pow, eval_X, smul_mul', smul_pow']

Evaluation of Scalar-Multiplied Polynomial at Scalar-Multiplied Point: $(m \cdot f)(m \cdot x) = m \cdot f(x)$

Informal description

Let $M$ be a monoid with a multiplicative semiring action on a semiring $S$, and let $S[X]$ be the polynomial ring over $S$. For any $m \in M$, any polynomial $f \in S[X]$, and any $x \in S$, the evaluation of the polynomial $m \cdot f$ at $m \cdot x$ is equal to $m$ acting on the evaluation of $f$ at $x$, i.e., $$(m \cdot f)(m \cdot x) = m \cdot f(x).$$

Polynomial.eval_smul' theorem

[MulSemiringAction G S] (g : G) (f : S[X]) (x : S) : f.eval (g • x) = g • (g⁻¹ • f).eval x

Full source

theorem eval_smul' [MulSemiringAction G S] (g : G) (f : S[X]) (x : S) :
    f.eval (g • x) = g • (g⁻¹ • f).eval x := by
  rw [← smul_eval_smul, smul_inv_smul]

Evaluation of Polynomial at Group Action Point: $f(g \cdot x) = g \cdot (g^{-1} \cdot f)(x)$

Informal description

Let $G$ be a group acting multiplicatively on a semiring $S$, and let $S[X]$ be the polynomial ring over $S$. For any $g \in G$, any polynomial $f \in S[X]$, and any $x \in S$, the evaluation of $f$ at $g \cdot x$ is equal to $g$ acting on the evaluation of $g^{-1} \cdot f$ at $x$, i.e., $$f(g \cdot x) = g \cdot \big((g^{-1} \cdot f)(x)\big).$$

Polynomial.smul_eval theorem

[MulSemiringAction G S] (g : G) (f : S[X]) (x : S) : (g • f).eval x = g • f.eval (g⁻¹ • x)

Full source

theorem smul_eval [MulSemiringAction G S] (g : G) (f : S[X]) (x : S) :
    (g • f).eval x = g • f.eval (g⁻¹ • x) := by
  rw [← smul_eval_smul, smul_inv_smul]

Evaluation of Group-Acted Polynomial: $(g \cdot f)(x) = g \cdot f(g^{-1} \cdot x)$

Informal description

Let $G$ be a group acting multiplicatively on a semiring $S$, and let $S[X]$ be the polynomial ring over $S$. For any $g \in G$, any polynomial $f \in S[X]$, and any $x \in S$, the evaluation of the polynomial $g \cdot f$ at $x$ is equal to $g$ acting on the evaluation of $f$ at $g^{-1} \cdot x$, i.e., $$(g \cdot f)(x) = g \cdot f(g^{-1} \cdot x).$$

prodXSubSMul definition

(x : R) : R[X]

Full source

/-- the product of `(X - g • x)` over distinct `g • x`. -/
noncomputable def prodXSubSMul (x : R) : R[X] :=
  letI := Classical.decEq R
  (Finset.univ : Finset (G ⧸ MulAction.stabilizer G x)).prod fun g ↦
    Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)

Product of $(X - g \cdot x)$ over distinct group action translates of $x$

Informal description

Given a commutative ring $R$ with a group $G$ acting on it via a multiplicative semiring action, and an element $x \in R$, the polynomial $\prod_{g \in G / \text{Stab}(x)} (X - g \cdot x)$ is defined, where the product is taken over distinct cosets of the stabilizer subgroup of $x$ in $G$. Here, $X$ is the polynomial variable and $g \cdot x$ denotes the action of $g$ on $x$.

prodXSubSMul.monic theorem

(x : R) : (prodXSubSMul G R x).Monic

Full source

theorem prodXSubSMul.monic (x : R) : (prodXSubSMul G R x).Monic :=
  Polynomial.monic_prod_of_monic _ _ fun _ _ ↦ Polynomial.monic_X_sub_C _

Monicity of the Polynomial $\prod_{g \in G / \text{Stab}(x)} (X - g \cdot x)$

Informal description

For any element $x$ in a commutative ring $R$ with a group $G$ acting on $R$ via a multiplicative semiring action, the polynomial $\prod_{g \in G / \text{Stab}(x)} (X - g \cdot x)$ is monic, where the product is taken over distinct cosets of the stabilizer subgroup of $x$ in $G$.

prodXSubSMul.eval theorem

(x : R) : (prodXSubSMul G R x).eval x = 0

Full source

theorem prodXSubSMul.eval (x : R) : (prodXSubSMul G R x).eval x = 0 :=
  letI := Classical.decEq R
  (map_prod ((Polynomial.aeval x).toRingHom.toMonoidHom : R[X]R[X] →* R) _ _).trans <|
    Finset.prod_eq_zero (Finset.mem_univ <| QuotientGroup.mk 1) <| by simp

Vanishing of the Orbit Polynomial at $x$

Informal description

For any element $x$ in a commutative ring $R$ with a group $G$ acting on $R$ via a multiplicative semiring action, the polynomial $\prod_{g \in G / \text{Stab}(x)} (X - g \cdot x)$ evaluates to zero at $x$, i.e., \[ \left( \prod_{g \in G / \text{Stab}(x)} (X - g \cdot x) \right)(x) = 0. \]

prodXSubSMul.smul theorem

(x : R) (g : G) : g • prodXSubSMul G R x = prodXSubSMul G R x

Full source

theorem prodXSubSMul.smul (x : R) (g : G) : g • prodXSubSMul G R x = prodXSubSMul G R x :=
  letI := Classical.decEq R
  Finset.smul_prod'.trans <|
    Fintype.prod_bijective _ (MulAction.bijective g) _ _ fun g' ↦ by
      rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]

Invariance of Orbit Polynomial under Group Action: $g \cdot \prod_{h \in G / \text{Stab}(x)} (X - h \cdot x) = \prod_{h \in G / \text{Stab}(x)} (X - h \cdot x)$

Informal description

For any element $x$ in a commutative ring $R$ with a group $G$ acting on $R$ via a multiplicative semiring action, and for any element $g \in G$, the action of $g$ on the polynomial $\prod_{h \in G / \text{Stab}(x)} (X - h \cdot x)$ leaves it invariant, i.e., \[ g \cdot \left( \prod_{h \in G / \text{Stab}(x)} (X - h \cdot x) \right) = \prod_{h \in G / \text{Stab}(x)} (X - h \cdot x). \]

prodXSubSMul.coeff theorem

(x : R) (g : G) (n : ℕ) : g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n

Full source

theorem prodXSubSMul.coeff (x : R) (g : G) (n : ℕ) :
    g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n := by
  rw [← Polynomial.coeff_smul, prodXSubSMul.smul]

Invariance of Orbit Polynomial Coefficients under Group Action

Informal description

Let $R$ be a commutative ring with a group $G$ acting on it via a multiplicative semiring action. For any element $x \in R$, any group element $g \in G$, and any natural number $n$, the action of $g$ on the $n$-th coefficient of the polynomial $\prod_{h \in G / \text{Stab}(x)} (X - h \cdot x)$ leaves it invariant, i.e., \[ g \cdot \left( \left( \prod_{h \in G / \text{Stab}(x)} (X - h \cdot x) \right)_n \right) = \left( \prod_{h \in G / \text{Stab}(x)} (X - h \cdot x) \right)_n. \]

MulSemiringActionHom.polynomial definition

(g : P →+*[M] Q) : P[X] →+*[M] Q[X]

Full source

/-- An equivariant map induces an equivariant map on polynomials. -/
protected noncomputable def polynomial (g : P →+*[M] Q) : P[X]P[X] →+*[M] Q[X] where
  toFun := map g
  map_smul' m p :=
    Polynomial.induction_on p
      (fun b ↦ by rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C])
      (fun p q ihp ihq ↦ by
        rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add])
      fun n b _ ↦ by rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
  map_zero' := Polynomial.map_zero (g : P →+* Q)
  map_add' _ _ := Polynomial.map_add (g : P →+* Q)
  map_one' := Polynomial.map_one (g : P →+* Q)
  map_mul' _ _ := Polynomial.map_mul (g : P →+* Q)

Polynomial extension of an equivariant ring homomorphism

Informal description

Given an equivariant ring homomorphism $ g \colon P \to Q $ with respect to a monoid action of $ M $, the function `MulSemiringActionHom.polynomial` extends $ g $ to a homomorphism $ g[X] \colon P[X] \to Q[X] $ between the corresponding polynomial rings, which is also equivariant with respect to the same monoid action. This extension is defined by applying $ g $ to each coefficient of the polynomial.

MulSemiringActionHom.coe_polynomial theorem

(g : P →+*[M] Q) : (g.polynomial : P[X] → Q[X]) = map g

Full source

@[simp]
theorem coe_polynomial (g : P →+*[M] Q) : (g.polynomial : P[X] → Q[X]) = map g := rfl

Coefficient-wise action of equivariant ring homomorphism on polynomials equals polynomial map

Informal description

Let $M$ be a monoid acting on commutative semirings $P$ and $Q$, and let $g \colon P \to Q$ be an equivariant ring homomorphism with respect to this action. Then the polynomial extension $g[X] \colon P[X] \to Q[X]$, defined by applying $g$ to each coefficient, satisfies $(g[X])(p) = \text{map}\, g\, p$ for any polynomial $p \in P[X]$.