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] (x : 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] (x : 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] (x : 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] (x : 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
@[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