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) (R : Type v) [monoid M] [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.

This combines distrib_mul_action with mul_distrib_mul_action.

Instances

source

@[protected, instance]

def mul_semiring_action.to_mul_distrib_mul_action (M : Type u) [monoid M] (R : Type v) [semiring R] [h : mul_semiring_action M R] :

mul_distrib_mul_action M R

Equations

mul_semiring_action.to_mul_distrib_mul_action M R = {to_mul_action := distrib_mul_action.to_mul_action mul_semiring_action.to_distrib_mul_action, smul_mul := _, smul_one := _}

source

@[simp]

theorem mul_semiring_action.to_ring_hom_apply (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (x : M) (ᾰ : R) :

⇑(mul_semiring_action.to_ring_hom M R x) ᾰ = (mul_distrib_mul_action.to_monoid_hom R x).to_fun ᾰ

source

def mul_semiring_action.to_ring_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_ring_hom M R x = {to_fun := (mul_distrib_mul_action.to_monoid_hom R x).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem to_ring_hom_injective (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] [has_faithful_scalar M R] :

function.injective (mul_semiring_action.to_ring_hom M R)

source

@[simp]

theorem mul_semiring_action.to_ring_equiv_apply (G : Type u) [group G] (R : Type v) [semiring R] [mul_semiring_action G R] (x : G) (ᾰ : R) :

⇑(mul_semiring_action.to_ring_equiv G R x) ᾰ = (distrib_mul_action.to_add_equiv R x).to_fun ᾰ

source

def mul_semiring_action.to_ring_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_ring_equiv G R x = {to_fun := (distrib_mul_action.to_add_equiv R x).to_fun, inv_fun := (distrib_mul_action.to_add_equiv R x).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem mul_semiring_action.to_ring_equiv_symm_apply (G : Type u) [group G] (R : Type v) [semiring R] [mul_semiring_action G R] (x : G) (ᾰ : R) :

⇑((mul_semiring_action.to_ring_equiv G R x).symm) ᾰ = (distrib_mul_action.to_add_equiv R x).inv_fun ᾰ

source

@[protected, instance]

def submonoid.mul_semiring_action {M : Type u} [monoid M] {R : Type v} [semiring R] [mul_semiring_action M R] (H : submonoid M) :

mul_semiring_action ↥H R

A stronger version of submonoid.distrib_mul_action.

Equations

H.mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul H.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}

source

@[protected, instance]

def subgroup.mul_semiring_action {G : Type u} [group G] {R : Type v} [semiring R] [mul_semiring_action G R] (H : subgroup G) :

mul_semiring_action ↥H R

A stronger version of subgroup.distrib_mul_action.

Equations

H.mul_semiring_action = H.to_submonoid.mul_semiring_action

source

@[protected, instance]

def subsemiring.mul_semiring_action {R : Type v} [semiring R] {R' : Type u_1} [semiring R'] [mul_semiring_action R' R] (H : subsemiring R') :

mul_semiring_action ↥H R

A stronger version of subsemiring.distrib_mul_action.

Equations

H.mul_semiring_action = H.to_submonoid.mul_semiring_action

source

@[protected, instance]

def subring.mul_semiring_action {R : Type v} [semiring R] {R' : Type u_1} [ring R'] [mul_semiring_action R' R] (H : subring R') :

mul_semiring_action ↥H R

A stronger version of subring.distrib_mul_action.

Equations

H.mul_semiring_action = H.to_subsemiring.mul_semiring_action

source

@[simp]

theorem smul_inv'' {M : Type u} [monoid M] {F : Type v} [division_ring F] [mul_semiring_action M F] (x : M) (m : F) :

x • m⁻¹ = (x • m)⁻¹

Note that smul_inv' refers to the group case, and smul_inv has an additional inverse on x.

source

@[class]

structure is_invariant_subring (M : Type u) [monoid M] {R : Type v} [ring R] [mul_semiring_action M R] (S : subring R) :

Prop

smul_mem : ∀ (m : M) {x : R}, x ∈ S → m • x ∈ S

A typeclass for subrings invariant under a mul_semiring_action.

Instances

subfield.to_subring.is_invariant_subring

source

@[protected, 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 : subring R) [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 := _}