Group action on rings applied to polynomials

This file contains instances and definitions relating MulSemiringAction to Polynomial.

theorem Polynomial.smul_eq_map {M : Type u_1} [Monoid M] (R : Type u_2) [Semiring R] [MulSemiringAction M R] (m : M) : HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

@[instance_reducible]

noncomputable instance Polynomial.instMulSemiringAction (M : Type u_1) [Monoid M] (R : Type u_2) [Semiring R] [MulSemiringAction M R] : MulSemiringAction M (Polynomial R)

Equations

• Polynomial.instMulSemiringAction M R = { toDistribMulAction := Polynomial.distribMulAction, smul_one := ⋯, smul_mul := ⋯ }

@[simp]

theorem Polynomial.smul_X {M : Type u_1} [Monoid M] {R : Type u_2} [Semiring R] [MulSemiringAction M R] (m : M) : m • X = X

theorem Polynomial.smul_eval_smul {M : Type u_1} [Monoid M] (S : Type u_3) [CommSemiring S] [MulSemiringAction M S] (m : M) (f : Polynomial S) (x : S) : eval (m • x) (m • f) = m • eval x f

theorem Polynomial.eval_smul' (S : Type u_3) [CommSemiring S] (G : Type u_4) [Group G] [MulSemiringAction G S] (g : G) (f : Polynomial S) (x : S) : eval (g • x) f = g • eval x (g⁻¹ • f)

theorem Polynomial.smul_eval (S : Type u_3) [CommSemiring S] (G : Type u_4) [Group G] [MulSemiringAction G S] (g : G) (f : Polynomial S) (x : S) : eval x (g • f) = g • eval (g⁻¹ • x) f

noncomputable def prodXSubSMul (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) : Polynomial R

the product of (X - g • x) over distinct g • x.

Equations

• prodXSubSMul G R x = ∏ g : G ⧸ MulAction.stabilizer G x, (Polynomial.X - Polynomial.C (MulAction.ofQuotientStabilizer G x g))

theorem prodXSubSMul.monic (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) : (prodXSubSMul G R x).Monic

theorem prodXSubSMul.eval (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) : Polynomial.eval x (prodXSubSMul G R x) = 0

theorem prodXSubSMul.smul (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) (g : G) : g • prodXSubSMul G R x = prodXSubSMul G R x

theorem prodXSubSMul.coeff (G : Type u_2) [Group G] [Fintype G] (R : Type u_3) [CommRing R] [MulSemiringAction G R] (x : R) (g : G) (n : ℕ) : g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n

noncomputable def MulSemiringActionHom.polynomial {M : Type u_1} [Monoid M] {P : Type u_2} [CommSemiring P] [MulSemiringAction M P] {Q : Type u_3} [CommSemiring Q] [MulSemiringAction M Q] (g : P →+*[M] Q) : Polynomial P →+*[M] Polynomial Q

An equivariant map induces an equivariant map on polynomials.

Equations

• g.polynomial = { toFun := Polynomial.map ↑g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulSemiringActionHom.coe_polynomial {M : Type u_1} [Monoid M] {P : Type u_2} [CommSemiring P] [MulSemiringAction M P] {Q : Type u_3} [CommSemiring Q] [MulSemiringAction M Q] (g : P →+*[M] Q) : ⇑g.polynomial = Polynomial.map ↑g