mathlib documentation

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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] :
Type v

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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [linear_action R M N] (n : N) :

@[simp]
theorem linear_action_zero (R : Type u) (M N : Type v) [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [linear_action R M N] (m : M) :

@[simp]
theorem linear_action_add_act (R : Type u) (M N : Type v) [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [linear_action R M N] (m m' : M) (n : N) :

@[simp]
theorem linear_action_act_add (R : Type u) (M N : Type v) [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [linear_action R M N] (m : M) (n n' : N) :

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

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

def linear_action.of_endo_map (R : Type u) (M N : Type v) [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] :
(M →ₗ[R] module.End R N)linear_action R M 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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] :
linear_action R M N(M →ₗ[R] module.End R N)

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

Equations