Group action on rings
This file defines the typeclass of monoid acting on semirings mul_semiring_action M R,
and the corresponding typeclass of invariant subrings.
Note that algebra does not satisfy the axioms of mul_semiring_action.
Implementation notes
There is no separate typeclass for group acting on rings, group acting on fields, etc.
They are all grouped under mul_semiring_action.
Tags
group action, invariant subring
def
distrib_mul_action.to_add_monoid_hom
(M : Type u)
[monoid M]
(A : Type v)
[add_monoid A]
[distrib_mul_action M A] :
M → A →+ A
Each element of the monoid defines a additive monoid homomorphism.
Equations
- distrib_mul_action.to_add_monoid_hom M A x = {to_fun := has_scalar.smul x, map_zero' := _, map_add' := _}
def
distrib_mul_action.to_add_equiv
(G : Type u)
[group G]
(A : Type v)
[add_monoid A]
[distrib_mul_action G A] :
G → A ≃+ A
Each element of the group defines an additive monoid isomorphism.
Equations
- distrib_mul_action.to_add_equiv G A x = {to_fun := (distrib_mul_action.to_add_monoid_hom G A x).to_fun, inv_fun := (mul_action.to_perm G A x).inv_fun, left_inv := _, right_inv := _, map_add' := _}
def
distrib_mul_action.hom_add_monoid_hom
(M : Type u)
[monoid M]
(A : Type v)
[add_monoid A]
[distrib_mul_action M A] :
M →* add_monoid.End A
Each element of the group defines an additive monoid homomorphism.
Equations
- distrib_mul_action.hom_add_monoid_hom M A = {to_fun := distrib_mul_action.to_add_monoid_hom M A _inst_7, map_one' := _, map_mul' := _}
def
mul_semiring_action.to_semiring_hom
(M : Type u)
[monoid M]
(R : Type v)
[semiring R]
[mul_semiring_action M R] :
M → R →+* R
Each element of the monoid defines a semiring homomorphism.
Equations
- mul_semiring_action.to_semiring_hom M R x = {to_fun := (distrib_mul_action.to_add_monoid_hom M R x).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
def
mul_semiring_action.to_semiring_equiv
(G : Type u)
[group G]
(R : Type v)
[semiring R]
[mul_semiring_action G R] :
G → R ≃+* R
Each element of the group defines a semiring isomorphism.
Equations
- mul_semiring_action.to_semiring_equiv G R x = {to_fun := (distrib_mul_action.to_add_equiv G R x).to_fun, inv_fun := (distrib_mul_action.to_add_equiv G R x).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
theorem
list.smul_prod
(M : Type u)
[monoid M]
(R : Type v)
[semiring R]
[mul_semiring_action M R]
(g : M)
(L : list R) :
theorem
multiset.smul_prod
(M : Type u)
[monoid M]
(S : Type v)
[comm_semiring S]
[mul_semiring_action M S]
(g : M)
(m : multiset S) :
g • m.prod = (multiset.map (has_scalar.smul g) m).prod
@[instance]
def
polynomial.mul_semiring_action
(M : Type u)
[monoid M]
(S : Type v)
[comm_semiring S]
[mul_semiring_action M S] :
Equations
- polynomial.mul_semiring_action M S = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (m : M), polynomial.map (mul_semiring_action.to_semiring_hom M S m)}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}
@[simp]
theorem
polynomial.coeff_smul'
(M : Type u)
[monoid M]
(S : Type v)
[comm_semiring S]
[mul_semiring_action M S]
(m : M)
(p : polynomial S)
(n : ℕ) :
@[simp]
theorem
polynomial.smul_C
(M : Type u)
[monoid M]
(S : Type v)
[comm_semiring S]
[mul_semiring_action M S]
(m : M)
(r : S) :
m • ⇑polynomial.C r = ⇑polynomial.C (m • r)
@[simp]
theorem
polynomial.smul_X
(M : Type u)
[monoid M]
(S : Type v)
[comm_semiring S]
[mul_semiring_action M S]
(m : M) :
theorem
polynomial.smul_eval_smul
(M : Type u)
[monoid M]
(S : Type v)
[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'
(G : Type u)
[group G]
(S : Type v)
[comm_semiring S]
[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
(G : Type u)
[group G]
(S : Type v)
[comm_semiring S]
[mul_semiring_action G S]
(g : G)
(f : polynomial S)
(x : S) :
polynomial.eval x (g • f) = g • polynomial.eval (g⁻¹ • x) f
@[class]
structure
is_invariant_subring
(M : Type u)
[monoid M]
{R : Type v}
[ring R]
[mul_semiring_action M R]
(S : set R)
[is_subring S] :
Prop
A subring invariant under the action.
Instances
@[instance]
def
is_invariant_subring.to_mul_semiring_action
(M : Type u)
[monoid M]
{R : Type v}
[ring R]
[mul_semiring_action M R]
(S : set R)
[is_subring S]
[is_invariant_subring M S] :
Equations
- is_invariant_subring.to_mul_semiring_action M S = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (m : M) (x : ↥S), ⟨m • ↑x, _⟩}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}
@[instance]
Equations
def
prod_X_sub_smul
(G : Type u)
[group G]
[fintype G]
(R : Type v)
[comm_ring R]
[mul_semiring_action G R] :
R → polynomial R
the product of (X - g • x) over distinct g • x.
Equations
- prod_X_sub_smul G R x = finset.univ.prod (λ (g : quotient_group.quotient (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)
[group G]
[fintype G]
(R : Type v)
[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)
[group G]
[fintype G]
(R : Type v)
[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)
[group G]
[fintype G]
(R : Type v)
[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)
[group G]
[fintype G]
(R : Type v)
[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