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

source

@[class]

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

Type (max u v)

to_distrib_mul_action : distrib_mul_action M R
smul_one : ∀ (g : M), g • 1 = 1
smul_mul : ∀ (g : M) (x y : R), g • x * y = (g • x) * g • y

Typeclass for multiplicative actions by monoids on semirings.

Instances

source

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

polynomial.faithful_mul_semiring_action

source

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

source

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} (a : ∀ (r : R), m₁ • r = m₂ • r) :

m₁ = m₂

source

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

distrib_mul_action.to_add_monoid_hom M A x = {to_fun := has_scalar.smul x, map_zero' := _, map_add' := _}

source

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

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' := _}

source

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' := _}

source

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

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' := _}

source

theorem injective_to_semiring_hom (M : Type u) [monoid M] (R : Type v) [semiring R] [faithful_mul_semiring_action M R] :

function.injective (mul_semiring_action.to_semiring_hom M R)

source

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

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' := _}

source

theorem list.smul_prod (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (g : M) (L : list R) :

g • L.prod = (list.map (has_scalar.smul g) L).prod

source

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

source

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

source

@[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)⁻¹

source

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

source

@[instance]

def polynomial.mul_semiring_action (M : Type u) [monoid M] (S : Type v) [comm_semiring S] [mul_semiring_action M S] :

mul_semiring_action M (polynomial 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 := _}

source

@[instance]

def polynomial.faithful_mul_semiring_action (M : Type u) [monoid M] (S : Type v) [comm_semiring S] [faithful_mul_semiring_action M S] :

faithful_mul_semiring_action M (polynomial S)

Equations

polynomial.faithful_mul_semiring_action M S = {to_mul_semiring_action := {to_distrib_mul_action := mul_semiring_action.to_distrib_mul_action (polynomial.mul_semiring_action M S), smul_one := _, smul_mul := _}, eq_of_smul_eq_smul' := _}

source

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

source

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

source

@[simp]

theorem polynomial.smul_X (M : Type u) [monoid M] (S : Type v) [comm_semiring S] [mul_semiring_action M S] (m : M) :

m • polynomial.X = polynomial.X

source

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

source

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)

source

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

source

@[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 ∈ S → m • x ∈ S

A subring invariant under the action.

Instances

fixed_points.is_invariant_subring

source

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

mul_semiring_action 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 := _}

source

@[instance]

def quotient_group.quotient.fintype (G : Type u) [group G] [fintype G] (s : subgroup G) :

fintype (quotient_group.quotient s)

Equations

quotient_group.quotient.fintype G s = quotient.fintype (quotient_group.left_rel s)

source

def prod_X_sub_smul (G : Type u) [group G] [fintype G] (R : Type v) [comm_ring R] [mul_semiring_action G R] (x : R) :

polynomial R

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

Equations

prod_X_sub_smul G R x = ∏ (g : quotient_group.quotient (mul_action.stabilizer G x)), (polynomial.X - ⇑polynomial.C (mul_action.of_quotient_stabilizer G x g))

source

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

source

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

source

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

source

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