-
Notifications
You must be signed in to change notification settings - Fork 237
/
GroupRingAction.lean
161 lines (121 loc) · 5.92 KB
/
GroupRingAction.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
! This file was ported from Lean 3 source module algebra.polynomial.group_ring_action
! leanprover-community/mathlib commit afad8e438d03f9d89da2914aa06cb4964ba87a18
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupRingAction.Basic
import Mathlib.Algebra.Hom.GroupAction
import Mathlib.Data.Polynomial.AlgebraMap
import Mathlib.Data.Polynomial.Monic
import Mathlib.GroupTheory.GroupAction.Quotient
/-!
# Group action on rings applied to polynomials
This file contains instances and definitions relating `MulSemiringAction` to `Polynomial`.
-/
variable (M : Type _) [Monoid M]
open Polynomial
namespace Polynomial
variable (R : Type _) [Semiring R]
variable {M}
-- porting note: changed `(· • ·) m` to `HSMul.hSMul m`
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 FunLike.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]
#align polynomial.smul_eq_map Polynomial.smul_eq_map
variable (M)
noncomputable instance [MulSemiringAction M R] : MulSemiringAction M R[X] :=
{ Polynomial.distribMulAction with
smul := (· • ·)
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) }
variable {M R}
variable [MulSemiringAction M R]
@[simp]
theorem smul_X (m : M) : (m • X : R[X]) = X :=
(smul_eq_map R m).symm ▸ map_X _
set_option linter.uppercaseLean3 false in
#align polynomial.smul_X Polynomial.smul_X
variable (S : Type _) [CommSemiring S] [MulSemiringAction M S]
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']
#align polynomial.smul_eval_smul Polynomial.smul_eval_smul
variable (G : Type _) [Group G]
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]
#align polynomial.eval_smul' Polynomial.eval_smul'
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]
#align polynomial.smul_eval Polynomial.smul_eval
end Polynomial
section CommRing
set_option linter.uppercaseLean3 false -- porting note: `prod_X_*`
variable (G : Type _) [Group G] [Fintype G]
variable (R : Type _) [CommRing R] [MulSemiringAction G R]
open MulAction
open Classical
/-- the product of `(X - g • x)` over distinct `g • x`. -/
noncomputable def prodXSubSmul (x : R) : R[X] :=
(Finset.univ : Finset (G ⧸ MulAction.stabilizer G x)).prod fun g ↦
Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)
#align prod_X_sub_smul prodXSubSmul
theorem prodXSubSmul.monic (x : R) : (prodXSubSmul G R x).Monic :=
Polynomial.monic_prod_of_monic _ _ fun _ _ ↦ Polynomial.monic_X_sub_C _
#align prod_X_sub_smul.monic prodXSubSmul.monic
theorem prodXSubSmul.eval (x : R) : (prodXSubSmul G R x).eval x = 0 :=
(map_prod ((Polynomial.aeval x).toRingHom.toMonoidHom : R[X] →* R) _ _).trans <|
Finset.prod_eq_zero (Finset.mem_univ <| QuotientGroup.mk 1) <| by simp
#align prod_X_sub_smul.eval prodXSubSmul.eval
theorem prodXSubSmul.smul (x : R) (g : G) : g • prodXSubSmul G R x = prodXSubSmul G R x :=
Finset.smul_prod.trans <|
Fintype.prod_bijective _ (MulAction.bijective g) _ _ fun g' ↦ by
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
#align prod_X_sub_smul.smul prodXSubSmul.smul
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]
#align prod_X_sub_smul.coeff prodXSubSmul.coeff
end CommRing
namespace MulSemiringActionHom
variable {M}
variable {P : Type _} [CommSemiring P] [MulSemiringAction M P]
variable {Q : Type _} [CommSemiring Q] [MulSemiringAction M Q]
open Polynomial
/-- An equivariant map induces an equivariant map on polynomials. -/
protected noncomputable def polynomial (g : P →+*[M] Q) : P[X] →+*[M] Q[X] where
toFun := map g
map_smul' m p :=
Polynomial.induction_on p
(fun b ↦ by rw [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 [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]
-- porting note: added `.toRingHom`
map_zero' := Polynomial.map_zero g.toRingHom
map_add' p q := Polynomial.map_add g.toRingHom
map_one' := Polynomial.map_one g.toRingHom
map_mul' p q := Polynomial.map_mul g.toRingHom
#align mul_semiring_action_hom.polynomial MulSemiringActionHom.polynomial
@[simp]
theorem coe_polynomial (g : P →+*[M] Q) : (g.polynomial : P[X] → Q[X]) = map g := rfl
#align mul_semiring_action_hom.coe_polynomial MulSemiringActionHom.coe_polynomial
end MulSemiringActionHom