# mathlibdocumentation

algebra.group_action_hom

# Equivariant homomorphisms

## Main definitions

• mul_action_hom M X Y, the type of equivariant functions from X to Y, where M is a monoid that acts on the types X and Y.
• distrib_mul_action_hom M A B, the type of equivariant additive monoid homomorphisms from A to B, where M is a monoid that acts on the additive monoids A and B.
• mul_semiring_action_hom M R S, the type of equivariant ring homomorphisms from R to S, where M is a monoid that acts on the rings R and S.

## Notations

• X →[M] Y is mul_action_hom M X Y.
• A →+[M] B is distrib_mul_action_hom M X Y.
• R →+*[M] S is mul_semiring_action_hom M X Y.
@[nolint]
structure mul_action_hom (M : Type u_1) [monoid M] (X : Type u_2) [ X] (Y : Type u_3) [ Y] :
Type (max u_2 u_3)

Equivariant functions.

@[instance]
def mul_action_hom.has_coe_to_fun (M : Type u_1) [monoid M] (X : Type u_2) [ X] (Y : Type u_3) [ Y] :

Equations
@[simp]
theorem mul_action_hom.map_smul {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] (f : X →[M] Y) (m : M) (x : X) :
f (m x) = m f x

@[ext]
theorem mul_action_hom.ext {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] {f g : X →[M] Y} :
(∀ (x : X), f x = g x)f = g

theorem mul_action_hom.ext_iff {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] {f g : X →[M] Y} :
f = g ∀ (x : X), f x = g x

def mul_action_hom.id (M : Type u_1) [monoid M] {X : Type u_2} [ X] :
X →[M] X

The identity map as an equivariant map.

Equations
@[simp]
theorem mul_action_hom.id_apply (M : Type u_1) [monoid M] {X : Type u_2} [ X] (x : X) :
x = x

def mul_action_hom.comp {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] {Z : Type u_4} [ Z] :
(Y →[M] Z)(X →[M] Y)(X →[M] Z)

Composition of two equivariant maps.

Equations
@[simp]
theorem mul_action_hom.comp_apply {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] {Z : Type u_4} [ Z] (g : Y →[M] Z) (f : X →[M] Y) (x : X) :
(g.comp f) x = g (f x)

@[simp]
theorem mul_action_hom.id_comp {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] (f : X →[M] Y) :
f = f

@[simp]
theorem mul_action_hom.comp_id {M : Type u_1} [monoid M] {X : Type u_2} [ X] {Y : Type u_3} [ Y] (f : X →[M] Y) :
f.comp = f

def mul_action_hom.to_quotient {G : Type u_15} [group G] (H : subgroup G) :

The canonical map to the left cosets.

Equations
@[simp]
theorem mul_action_hom.to_quotient_apply {G : Type u_15} [group G] (H : subgroup G) (g : G) :

def distrib_mul_action_hom.to_mul_action_hom {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] :
(A →+[M] B)(A →[M] B)

Reinterpret an equivariant additive monoid homomorphism as an equivariant function.

def distrib_mul_action_hom.to_add_monoid_hom {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] :
(A →+[M] B)A →+ B

@[nolint]
structure distrib_mul_action_hom (M : Type u_1) [monoid M] (A : Type u_5) [add_monoid A] [ A] (B : Type u_7) [add_monoid B] [ B] :
Type (max u_5 u_7)

@[instance]
def distrib_mul_action_hom.has_coe (M : Type u_1) [monoid M] (A : Type u_5) [add_monoid A] [ A] (B : Type u_7) [add_monoid B] [ B] :
has_coe (A →+[M] B) (A →+ B)

Equations
@[instance]
def distrib_mul_action_hom.has_coe' (M : Type u_1) [monoid M] (A : Type u_5) [add_monoid A] [ A] (B : Type u_7) [add_monoid B] [ B] :
has_coe (A →+[M] B) (A →[M] B)

Equations
@[instance]
def distrib_mul_action_hom.has_coe_to_fun (M : Type u_1) [monoid M] (A : Type u_5) [add_monoid A] [ A] (B : Type u_7) [add_monoid B] [ B] :

Equations
theorem distrib_mul_action_hom.coe_fn_coe {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) :

theorem distrib_mul_action_hom.coe_fn_coe' {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) :

@[ext]
theorem distrib_mul_action_hom.ext {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] {f g : A →+[M] B} :
(∀ (x : A), f x = g x)f = g

theorem distrib_mul_action_hom.ext_iff {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] {f g : A →+[M] B} :
f = g ∀ (x : A), f x = g x

@[simp]
theorem distrib_mul_action_hom.map_zero {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) :
f 0 = 0

@[simp]
theorem distrib_mul_action_hom.map_add {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) (x y : A) :
f (x + y) = f x + f y

@[simp]
theorem distrib_mul_action_hom.map_neg {M : Type u_1} [monoid M] (A' : Type u_6) [add_group A'] [ A'] (B' : Type u_8) [add_group B'] [ B'] (f : A' →+[M] B') (x : A') :
f (-x) = -f x

@[simp]
theorem distrib_mul_action_hom.map_sub {M : Type u_1} [monoid M] (A' : Type u_6) [add_group A'] [ A'] (B' : Type u_8) [add_group B'] [ B'] (f : A' →+[M] B') (x y : A') :
f (x - y) = f x - f y

@[simp]
theorem distrib_mul_action_hom.map_smul {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) (m : M) (x : A) :
f (m x) = m f x

def distrib_mul_action_hom.id (M : Type u_1) [monoid M] {A : Type u_5} [add_monoid A] [ A] :
A →+[M] A

The identity map as an equivariant additive monoid homomorphism.

Equations
@[simp]
theorem distrib_mul_action_hom.id_apply (M : Type u_1) [monoid M] {A : Type u_5} [add_monoid A] [ A] (x : A) :
= x

def distrib_mul_action_hom.comp {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] {C : Type u_9} [add_monoid C] [ C] :
(B →+[M] C)(A →+[M] B)(A →+[M] C)

Composition of two equivariant additive monoid homomorphisms.

Equations
@[simp]
theorem distrib_mul_action_hom.comp_apply {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] {C : Type u_9} [add_monoid C] [ C] (g : B →+[M] C) (f : A →+[M] B) (x : A) :
(g.comp f) x = g (f x)

@[simp]
theorem distrib_mul_action_hom.id_comp {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) :
= f

@[simp]
theorem distrib_mul_action_hom.comp_id {M : Type u_1} [monoid M] {A : Type u_5} [add_monoid A] [ A] {B : Type u_7} [add_monoid B] [ B] (f : A →+[M] B) :
= f

def mul_semiring_action_hom.to_distrib_mul_action_hom {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] :
(R →+*[M] S)(R →+[M] S)

Reinterpret an equivariant ring homomorphism as an equivariant additive monoid homomorphism.

def mul_semiring_action_hom.to_ring_hom {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] :
(R →+*[M] S)R →+* S

Reinterpret an equivariant ring homomorphism as a ring homomorphism.

@[nolint]
structure mul_semiring_action_hom (M : Type u_1) [monoid M] (R : Type u_10) [semiring R] [ R] (S : Type u_12) [semiring S] [ S] :
Type (max u_10 u_12)

Equivariant ring homomorphisms.

@[instance]
def mul_semiring_action_hom.has_coe (M : Type u_1) [monoid M] (R : Type u_10) [semiring R] [ R] (S : Type u_12) [semiring S] [ S] :
has_coe (R →+*[M] S) (R →+* S)

Equations
@[instance]
def mul_semiring_action_hom.has_coe' (M : Type u_1) [monoid M] (R : Type u_10) [semiring R] [ R] (S : Type u_12) [semiring S] [ S] :
has_coe (R →+*[M] S) (R →+[M] S)

Equations
@[instance]
def mul_semiring_action_hom.has_coe_to_fun (M : Type u_1) [monoid M] (R : Type u_10) [semiring R] [ R] (S : Type u_12) [semiring S] [ S] :

Equations
theorem mul_semiring_action_hom.coe_fn_coe {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) :

theorem mul_semiring_action_hom.coe_fn_coe' {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) :

@[ext]
theorem mul_semiring_action_hom.ext {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] {f g : R →+*[M] S} :
(∀ (x : R), f x = g x)f = g

theorem mul_semiring_action_hom.ext_iff {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] {f g : R →+*[M] S} :
f = g ∀ (x : R), f x = g x

@[simp]
theorem mul_semiring_action_hom.map_zero {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) :
f 0 = 0

@[simp]
theorem mul_semiring_action_hom.map_add {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) (x y : R) :
f (x + y) = f x + f y

@[simp]
theorem mul_semiring_action_hom.map_neg {M : Type u_1} [monoid M] (R' : Type u_11) [ring R'] [ R'] (S' : Type u_13) [ring S'] [ S'] (f : R' →+*[M] S') (x : R') :
f (-x) = -f x

@[simp]
theorem mul_semiring_action_hom.map_sub {M : Type u_1} [monoid M] (R' : Type u_11) [ring R'] [ R'] (S' : Type u_13) [ring S'] [ S'] (f : R' →+*[M] S') (x y : R') :
f (x - y) = f x - f y

@[simp]
theorem mul_semiring_action_hom.map_one {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) :
f 1 = 1

@[simp]
theorem mul_semiring_action_hom.map_mul {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) (x y : R) :
f (x * y) = (f x) * f y

@[simp]
theorem mul_semiring_action_hom.map_smul {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) (m : M) (x : R) :
f (m x) = m f x

def mul_semiring_action_hom.id (M : Type u_1) [monoid M] {R : Type u_10} [semiring R] [ R] :
R →+*[M] R

The identity map as an equivariant ring homomorphism.

Equations
@[simp]
theorem mul_semiring_action_hom.id_apply (M : Type u_1) [monoid M] {R : Type u_10} [semiring R] [ R] (x : R) :
= x

def mul_semiring_action_hom.comp {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] {T : Type u_14} [semiring T] [ T] :
(S →+*[M] T)(R →+*[M] S)(R →+*[M] T)

Composition of two equivariant additive monoid homomorphisms.

Equations
@[simp]
theorem mul_semiring_action_hom.comp_apply {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] {T : Type u_14} [semiring T] [ T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :
(g.comp f) x = g (f x)

@[simp]
theorem mul_semiring_action_hom.id_comp {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) :
= f

@[simp]
theorem mul_semiring_action_hom.comp_id {M : Type u_1} [monoid M] {R : Type u_10} [semiring R] [ R] {S : Type u_12} [semiring S] [ S] (f : R →+*[M] S) :
= f

def mul_semiring_action_hom.polynomial {M : Type u_1} [monoid M] {P : Type u_16} [ P] {Q : Type u_17} [ Q] :
(P →+*[M] Q) →+*[M]

An equivariant map induces an equivariant map on polynomials.

Equations
@[simp]
theorem mul_semiring_action_hom.coe_polynomial {M : Type u_1} [monoid M] {P : Type u_16} [ P] {Q : Type u_17} [ Q] (g : P →+*[M] Q) :

def is_invariant_subring.subtype_hom (M : Type u_1) [monoid M] {R' : Type u_11} [ring R'] [ R'] (U : set R') [is_subring U] [ U] :

The canonical inclusion from an invariant subring.

Equations
@[simp]
theorem is_invariant_subring.coe_subtype_hom (M : Type u_1) [monoid M] {R' : Type u_11} [ring R'] [ R'] (U : set R') [is_subring U] [ U] :

@[simp]
theorem is_invariant_subring.coe_subtype_hom' (M : Type u_1) [monoid M] {R' : Type u_11} [ring R'] [ R'] (U : set R') [is_subring U] [ U] :