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
- act : M → N → N
- add_act : ∀ (m m' : M) (n : N), linear_action.act R (m + m') n = linear_action.act R m n + linear_action.act R m' n
- act_add : ∀ (m : M) (n n' : N), linear_action.act R m (n + n') = linear_action.act R m n + linear_action.act R m n'
- act_smul : ∀ (r : R) (m : M) (n : N), linear_action.act R (r • m) n = r • linear_action.act R m n
- smul_act : ∀ (r : R) (m : M) (n : N), linear_action.act R m (r • n) = linear_action.act R (r • m) n
A binary operation representing one module acting linearly on another.
@[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) :
linear_action.act R 0 n = 0
@[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) :
linear_action.act R m 0 = 0
@[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) :
linear_action.act R (m + m') n = linear_action.act R m n + linear_action.act R m' 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) :
linear_action.act R m (n + n') = linear_action.act R m n + linear_action.act R m 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) :
linear_action.act R (r • m) n = r • linear_action.act R m 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) :
linear_action.act R m (r • n) = linear_action.act R (r • m) 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.
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.