mathlib documentation

algebra.group_ring_action

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

@[class]
structure mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R] :
Type (max u v)

Typeclass for multiplicative actions by monoids on semirings.

Instances
@[class]
structure faithful_mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R] :
Type (max u v)
  • to_mul_semiring_action : mul_semiring_action M R
  • eq_of_smul_eq_smul' : ∀ {m₁ m₂ : M}, (∀ (r : R), m₁ r = m₂ r)m₁ = m₂

Typeclass for faithful multiplicative actions by monoids on semirings.

Instances
@[simp]
theorem smul_mul' {M : Type u} [monoid M] {R : Type v} [semiring R] [mul_semiring_action M R] (g : M) (x y : R) :
g x * y = (g x) * g y

theorem eq_of_smul_eq_smul {M : Type u} [monoid M] (R : Type v) [semiring R] [faithful_mul_semiring_action M R] {m₁ m₂ : M} :
(∀ (r : R), m₁ r = m₂ r)m₁ = m₂

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
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

Each element of the group defines an additive monoid homomorphism.

Equations
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
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
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) :

theorem smul_prod (M : Type u) [monoid M] (S : Type v) [comm_semiring S] [mul_semiring_action M S] (g : M) {ι : Type u_1} (f : ι → S) (s : finset ι) :
g ∏ (i : ι) in s, f i = ∏ (i : ι) in s, g f i

@[simp]
theorem smul_inv {M : Type u} [monoid M] (F : Type v) [field F] [mul_semiring_action M F] (x : M) (m : F) :
x m⁻¹ = (x m)⁻¹

@[simp]
theorem smul_pow {M : Type u} [monoid M] {R : Type v} [semiring R] [mul_semiring_action M R] (x : M) (m : R) (n : ) :
x m ^ n = (x m) ^ n

@[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 : ) :
(m p).coeff n = m p.coeff 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) :

@[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) :

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) :

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) :

@[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
  • smul_mem : ∀ (m : M) {x : R}, x Sm x S

A subring invariant under the action.

Instances
@[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
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) :

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) :

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) :

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 : ) :