Group action on rings applied to polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains instances and definitions relating mul_semiring_action to polynomial.
theorem
polynomial.smul_eq_map
{M : Type u_1}
[monoid M]
(R : Type u_2)
[semiring R]
[mul_semiring_action M R]
(m : M) :
@[protected, instance]
noncomputable
def
polynomial.mul_semiring_action
(M : Type u_1)
[monoid M]
(R : Type u_2)
[semiring R]
[mul_semiring_action M R] :
Equations
- polynomial.mul_semiring_action M R = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul smul_zero_class.to_has_smul}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
@[simp]
theorem
polynomial.smul_X
{M : Type u_1}
[monoid M]
{R : Type u_2}
[semiring R]
[mul_semiring_action M R]
(m : M) :
theorem
polynomial.smul_eval_smul
{M : Type u_1}
[monoid M]
(S : Type u_3)
[comm_semiring S]
[mul_semiring_action M S]
(m : M)
(f : polynomial S)
(x : S) :
polynomial.eval (m • x) (m • f) = m • polynomial.eval x f
theorem
polynomial.eval_smul'
(S : Type u_3)
[comm_semiring S]
(G : Type u_4)
[group G]
[mul_semiring_action G S]
(g : G)
(f : polynomial S)
(x : S) :
polynomial.eval (g • x) f = g • polynomial.eval x (g⁻¹ • f)
theorem
polynomial.smul_eval
(S : Type u_3)
[comm_semiring S]
(G : Type u_4)
[group G]
[mul_semiring_action G S]
(g : G)
(f : polynomial S)
(x : S) :
polynomial.eval x (g • f) = g • polynomial.eval (g⁻¹ • x) f
noncomputable
def
prod_X_sub_smul
(G : Type u_2)
[group G]
[fintype G]
(R : Type u_3)
[comm_ring R]
[mul_semiring_action G R]
(x : R) :
the product of (X - g • x) over distinct g • x.
Equations
- prod_X_sub_smul G R x = finset.univ.prod (λ (g : G ⧸ mul_action.stabilizer G x), polynomial.X - ⇑polynomial.C (mul_action.of_quotient_stabilizer G x g))
theorem
prod_X_sub_smul.monic
(G : Type u_2)
[group G]
[fintype G]
(R : Type u_3)
[comm_ring R]
[mul_semiring_action G R]
(x : R) :
(prod_X_sub_smul G R x).monic
theorem
prod_X_sub_smul.eval
(G : Type u_2)
[group G]
[fintype G]
(R : Type u_3)
[comm_ring R]
[mul_semiring_action G R]
(x : R) :
polynomial.eval x (prod_X_sub_smul G R x) = 0
theorem
prod_X_sub_smul.smul
(G : Type u_2)
[group G]
[fintype G]
(R : Type u_3)
[comm_ring R]
[mul_semiring_action G R]
(x : R)
(g : G) :
g • prod_X_sub_smul G R x = prod_X_sub_smul G R x
theorem
prod_X_sub_smul.coeff
(G : Type u_2)
[group G]
[fintype G]
(R : Type u_3)
[comm_ring R]
[mul_semiring_action G R]
(x : R)
(g : G)
(n : ℕ) :
g • (prod_X_sub_smul G R x).coeff n = (prod_X_sub_smul G R x).coeff n
@[protected]
noncomputable
def
mul_semiring_action_hom.polynomial
{M : Type u_1}
[monoid M]
{P : Type u_2}
[comm_semiring P]
[mul_semiring_action M P]
{Q : Type u_3}
[comm_semiring Q]
[mul_semiring_action M Q]
(g : P →+*[M] Q) :
polynomial P →+*[M] polynomial Q
An equivariant map induces an equivariant map on polynomials.
@[simp]
theorem
mul_semiring_action_hom.coe_polynomial
{M : Type u_1}
[monoid M]
{P : Type u_2}
[comm_semiring P]
[mul_semiring_action M P]
{Q : Type u_3}
[comm_semiring Q]
[mul_semiring_action M Q]
(g : P →+*[M] Q) :
⇑(g.polynomial) = polynomial.map ↑g