# Documentation

Mathlib.Algebra.Hom.GroupAction

# Equivariant homomorphisms #

## Main definitions #

• MulActionHom 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.
• DistribMulActionHom 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.
• MulSemiringActionHom 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.

The above types have corresponding classes:

• SMulHomClass F M X Y states that F is a type of bundled X → Y homs preserving scalar multiplication by M
• DistribMulActionHomClass F M A B states that F is a type of bundled A → B homs preserving the additive monoid structure and scalar multiplication by M
• MulSemiringActionHomClass F M R S states that F is a type of bundled R → S homs preserving the ring structure and scalar multiplication by M

## Notations #

• X →[M] Y is MulActionHom M X Y.
• A →+[M] B is DistribMulActionHom M A B.
• R →+*[M] S is MulSemiringActionHom M R S.
structure MulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
Type (max u_2 u_3)
• toFun : XY

The underlying function.

• map_smul' : ∀ (m : M') (x : X), MulActionHom.toFun s (m x) = m

The proposition that the function preserves the action.

Equivariant functions.

Instances For

Equivariant functions.

Instances For
class SMulHomClass (F : Type u_16) (M : outParam (Type u_17)) (X : outParam (Type u_18)) (Y : outParam (Type u_19)) [SMul M X] [SMul M Y] extends :
Type (max (max u_16 u_18) u_19)
• coe : FXY
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : M) (x : X), f (c x) = c f x

The proposition that the function preserves the action.

SMulHomClass F M X Y states that F is a type of morphisms preserving scalar multiplication by M.

You should extend this class when you extend MulActionHom.

Instances
instance instSMulHomClassMulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
SMulHomClass (X →[M'] Y) M' X Y
def SMulHomClass.toMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [SMulHomClass F M X Y] (f : F) :
X →[M] Y

Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

Instances For
instance MulActionHom.instCoeTCMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [SMulHomClass F M X Y] :
CoeTC F (X →[M] Y)

Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

theorem MulActionHom.map_smul {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) (m : M') (x : X) :
f (m x) = m f x
theorem MulActionHom.ext {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :
(∀ (x : X), f x = g x) → f = g
theorem MulActionHom.ext_iff {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :
f = g ∀ (x : X), f x = g x
theorem MulActionHom.congr_fun {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} (h : f = g) (x : X) :
f x = g x
def MulActionHom.id (M' : Type u_1) {X : Type u_2} [SMul M' X] :
X →[M'] X

The identity map as an equivariant map.

Instances For
@[simp]
theorem MulActionHom.id_apply (M' : Type u_1) {X : Type u_2} [SMul M' X] (x : X) :
↑() x = x
def MulActionHom.comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) :
X →[M'] Z

Composition of two equivariant maps.

Instances For
@[simp]
theorem MulActionHom.comp_apply {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) (x : X) :
↑() x = g (f x)
@[simp]
theorem MulActionHom.id_comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) :
= f
@[simp]
theorem MulActionHom.comp_id {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) :
= f
@[simp]
theorem MulActionHom.inverse_apply {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →[M] B) (g : BA) (h₁ : ) (h₂ : ) :
∀ (a : B), ↑(MulActionHom.inverse f g h₁ h₂) a = g a
def MulActionHom.inverse {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →[M] B) (g : BA) (h₁ : ) (h₂ : ) :
B →[M] A

The inverse of a bijective equivariant map is equivariant.

Instances For
@[simp]
theorem SMulCommClass.toMulActionHom_apply {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [] (c : M) :
∀ (x : α), ↑() x = c x
def SMulCommClass.toMulActionHom {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [] (c : M) :
α →[N] α

If actions of M and N on α commute, then for c : M, (c • · : α → α) is an N-action homomorphism.

Instances For
structure DistribMulActionHom (M : Type u_5) [] (A : Type u_6) [] [] (B : Type u_8) [] [] extends :
Type (max u_6 u_8)

Instances For
@[reducible]
abbrev DistribMulActionHom.toAddMonoidHom {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (self : A →+[M] B) :
A →+ B

Instances For

Instances For
class DistribMulActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (A : outParam (Type u_18)) (B : outParam (Type u_19)) [] [] [] [] [] extends :
Type (max (max u_16 u_18) u_19)
• coe : FAB
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : M) (x : A), f (c x) = c f x
• map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y

The proposition that the function preserves addition

• map_zero : ∀ (f : F), f 0 = 0

The proposition that the function preserves 0

DistribMulActionHomClass F M A B states that F is a type of morphisms preserving the additive monoid structure and scalar multiplication by M.

You should extend this class when you extend DistribMulActionHom.

Instances
def DistribMulActionHomClass.toDistribMulActionHom {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {F : Type u_16} [] (f : F) :
A →+[M] B

Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

Instances For
instance DistribMulActionHom.instCoeTCDistribMulActionHom {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {F : Type u_16} [] :
CoeTC F (A →+[M] B)

Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

@[simp]
theorem DistribMulActionHom.toFun_eq_coe {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) :
f.toFun = f
theorem DistribMulActionHom.coe_fn_coe {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) :
f = f
theorem DistribMulActionHom.coe_fn_coe' {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) :
f = f
theorem DistribMulActionHom.ext {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {f : A →+[M] B} {g : A →+[M] B} :
(∀ (x : A), f x = g x) → f = g
theorem DistribMulActionHom.ext_iff {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {f : A →+[M] B} {g : A →+[M] B} :
f = g ∀ (x : A), f x = g x
theorem DistribMulActionHom.congr_fun {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) (x : A) :
f x = g x
theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) :
f = g
theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) :
f = g
theorem DistribMulActionHom.map_zero {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) :
f 0 = 0
theorem DistribMulActionHom.map_add {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) (x : A) (y : A) :
f (x + y) = f x + f y
theorem DistribMulActionHom.map_neg {M : Type u_5} [] (A' : Type u_7) [AddGroup A'] [] (B' : Type u_9) [AddGroup B'] [] (f : A' →+[M] B') (x : A') :
f (-x) = -f x
theorem DistribMulActionHom.map_sub {M : Type u_5} [] (A' : Type u_7) [AddGroup A'] [] (B' : Type u_9) [AddGroup B'] [] (f : A' →+[M] B') (x : A') (y : A') :
f (x - y) = f x - f y
theorem DistribMulActionHom.map_smul {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) (m : M) (x : A) :
f (m x) = m f x
def DistribMulActionHom.id (M : Type u_5) [] {A : Type u_6} [] [] :
A →+[M] A

The identity map as an equivariant additive monoid homomorphism.

Instances For
@[simp]
theorem DistribMulActionHom.id_apply (M : Type u_5) [] {A : Type u_6} [] [] (x : A) :
↑() x = x
instance DistribMulActionHom.instZeroDistribMulActionHom {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] :
Zero (A →+[M] B)
instance DistribMulActionHom.instOneDistribMulActionHom {M : Type u_5} [] {A : Type u_6} [] [] :
One (A →+[M] A)
@[simp]
theorem DistribMulActionHom.coe_zero {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] :
0 = 0
@[simp]
theorem DistribMulActionHom.coe_one {M : Type u_5} [] {A : Type u_6} [] [] :
1 = id
theorem DistribMulActionHom.zero_apply {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (a : A) :
0 a = 0
theorem DistribMulActionHom.one_apply {M : Type u_5} [] {A : Type u_6} [] [] (a : A) :
1 a = a
instance DistribMulActionHom.instInhabitedDistribMulActionHom {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] :
def DistribMulActionHom.comp {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {C : Type u_10} [] [] (g : B →+[M] C) (f : A →+[M] B) :
A →+[M] C

Composition of two equivariant additive monoid homomorphisms.

Instances For
@[simp]
theorem DistribMulActionHom.comp_apply {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] {C : Type u_10} [] [] (g : B →+[M] C) (f : A →+[M] B) (x : A) :
↑() x = g (f x)
@[simp]
theorem DistribMulActionHom.id_comp {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) :
@[simp]
theorem DistribMulActionHom.comp_id {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) :
@[simp]
theorem DistribMulActionHom.inverse_apply {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) (g : BA) (h₁ : ) (h₂ : ) :
∀ (a : B), ↑() a = g a
def DistribMulActionHom.inverse {M : Type u_5} [] {A : Type u_6} [] [] {B : Type u_8} [] [] (f : A →+[M] B) (g : BA) (h₁ : ) (h₂ : ) :
B →+[M] A

The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

Instances For
theorem DistribMulActionHom.ext_ring {M' : Type u_1} {R : Type u_11} [] [] [] {f : R →+[R] M'} {g : R →+[R] M'} (h : f 1 = g 1) :
f = g
theorem DistribMulActionHom.ext_ring_iff {M' : Type u_1} {R : Type u_11} [] [] [] {f : R →+[R] M'} {g : R →+[R] M'} :
f = g f 1 = g 1
@[simp]
theorem SMulCommClass.toDistribMulActionHom_apply {M : Type u_18} (N : Type u_16) (A : Type u_17) [] [] [] [] [] (c : M) :
∀ (x : A), ↑() x = c x
def SMulCommClass.toDistribMulActionHom {M : Type u_18} (N : Type u_16) (A : Type u_17) [] [] [] [] [] (c : M) :
A →+[N] A

If DistribMulAction of M and N on A commute, then for each c : M, (c • ·) is an N-action additive homomorphism.

Instances For
structure MulSemiringActionHom (M : Type u_5) [] (R : Type u_11) [] [] (S : Type u_13) [] [] extends :
Type (max u_11 u_13)

Equivariant ring homomorphisms.

Instances For
@[reducible]
abbrev MulSemiringActionHom.toRingHom {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (self : R →+*[M] S) :
R →+* S

Reinterpret an equivariant ring homomorphism as a ring homomorphism.

Instances For

Equivariant ring homomorphisms.

Instances For
class MulSemiringActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (R : outParam (Type u_18)) (S : outParam (Type u_19)) [] [] [] [] [] extends :
Type (max (max u_16 u_18) u_19)
• coe : FRS
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : M) (x : R), f (c x) = c f x
• map_add : ∀ (f : F) (x y : R), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0
• map_mul : ∀ (f : F) (x y : R), f (x * y) = f x * f y

The proposition that the function preserves multiplication

• map_one : ∀ (f : F), f 1 = 1

The proposition that the function preserves 1

MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and scalar multiplication by M.

You should extend this class when you extend MulSemiringActionHom.

Instances
def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] {F : Type u_16} [] (f : F) :
R →+*[M] S

Turn an element of a type F satisfying MulSemiringActionHomClass F M R S into an actual MulSemiringActionHom. This is declared as the default coercion from F to MulSemiringActionHom M X Y.

Instances For
instance MulSemiringActionHom.instCoeTCMulSemiringActionHom {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] {F : Type u_16} [] :
CoeTC F (R →+*[M] S)

Any type satisfying MulSemiringActionHomClass can be cast into MulSemiringActionHom via MulSemiringActionHomClass.toMulSemiringActionHom.

theorem MulSemiringActionHom.coe_fn_coe {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) :
f = f
theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) :
f = f
theorem MulSemiringActionHom.ext {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] {f : R →+*[M] S} {g : R →+*[M] S} :
(∀ (x : R), f x = g x) → f = g
theorem MulSemiringActionHom.ext_iff {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] {f : R →+*[M] S} {g : R →+*[M] S} :
f = g ∀ (x : R), f x = g x
theorem MulSemiringActionHom.map_zero {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) :
f 0 = 0
theorem MulSemiringActionHom.map_add {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) (x : R) (y : R) :
f (x + y) = f x + f y
theorem MulSemiringActionHom.map_neg {M : Type u_5} [] (R' : Type u_12) [Ring R'] [] (S' : Type u_14) [Ring S'] [] (f : R' →+*[M] S') (x : R') :
f (-x) = -f x
theorem MulSemiringActionHom.map_sub {M : Type u_5} [] (R' : Type u_12) [Ring R'] [] (S' : Type u_14) [Ring S'] [] (f : R' →+*[M] S') (x : R') (y : R') :
f (x - y) = f x - f y
theorem MulSemiringActionHom.map_one {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) :
f 1 = 1
theorem MulSemiringActionHom.map_mul {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) (x : R) (y : R) :
f (x * y) = f x * f y
theorem MulSemiringActionHom.map_smul {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) (m : M) (x : R) :
f (m x) = m f x
def MulSemiringActionHom.id (M : Type u_5) [] {R : Type u_11} [] [] :
R →+*[M] R

The identity map as an equivariant ring homomorphism.

Instances For
@[simp]
theorem MulSemiringActionHom.id_apply (M : Type u_5) [] {R : Type u_11} [] [] (x : R) :
↑() x = x
def MulSemiringActionHom.comp {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] {T : Type u_15} [] [] (g : S →+*[M] T) (f : R →+*[M] S) :
R →+*[M] T

Composition of two equivariant additive monoid homomorphisms.

Instances For
@[simp]
theorem MulSemiringActionHom.comp_apply {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] {T : Type u_15} [] [] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :
↑() x = g (f x)
@[simp]
theorem MulSemiringActionHom.id_comp {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) :
@[simp]
theorem MulSemiringActionHom.comp_id {M : Type u_5} [] {R : Type u_11} [] [] {S : Type u_13} [] [] (f : R →+*[M] S) :