# mathlibdocumentation

linear_algebra.linear_action

# Linear actions

For modules M and N, we can regard a linear map M →ₗ End N as a "linear action" of M on N. In this file we introduce the class linear_action to make it easier to work with such actions.

## Tags

linear action

@[class]
structure linear_action (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] :
Type v
• act : M → N → N
• add_act : ∀ (m m' : M) (n : N), (m + m') n = n + n
• act_add : ∀ (m : M) (n n' : N), (n + n') = n + n'
• act_smul : ∀ (r : R) (m : M) (n : N), (r m) n = r n
• smul_act : ∀ (r : R) (m : M) (n : N), (r n) = (r m) n

A binary operation representing one module acting linearly on another.

Instances
@[simp]
theorem zero_linear_action (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] [ N] (n : N) :
n = 0

@[simp]
theorem linear_action_zero (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] [ N] (m : M) :
0 = 0

@[simp]
theorem linear_action_add_act (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] [ N] (m m' : M) (n : N) :
(m + m') n = n + n

@[simp]
theorem linear_action_act_add (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] [ N] (m : M) (n n' : N) :
(n + n') = n + n'

@[simp]
theorem linear_action_act_smul (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] [ N] (r : R) (m : M) (n : N) :
(r m) n = r n

@[simp]
theorem linear_action_smul_act (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] [ N] (r : R) (m : M) (n : N) :
(r n) = (r m) n

def linear_action.of_endo_map (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] :
(M →ₗ[R] N) N

A linear map to the endomorphism algebra yields a linear action.

Equations
def linear_action.to_endo_map (R : Type u) (M N : Type v) [comm_ring R] [ M] [ N] :
N(M →ₗ[R] N)

A linear action yields a linear map to the endomorphism algebra.

Equations