Endomorphisms of a module #
In this file we define the type of linear endomorphisms of a module over a ring (Module.End
).
We set up the basic theory,
including the action of Module.End
on the module we are considering endomorphisms of.
Main results #
Module.End.instSemiring
andModule.End.instRing
: the (semi)ring of endomorphisms formed by taking the additive structure above with composition as multiplication.
Linear endomorphisms of a module, with associated ring structure
Module.End.semiring
and algebra structure Module.End.algebra
.
Equations
Instances For
Monoid structure of endomorphisms #
Equations
Equations
Equations
Equations
See also Module.End.natCast_def
.
Equations
See also Module.End.intCast_def
.
Action by a module endomorphism. #
The tautological action by Module.End R M
(aka M →ₗ[R] M
) on M
.
This generalizes Function.End.applyMulAction
.
Equations
LinearMap.applyModule
is faithful.
Actions as module endomorphisms #
Each element of the monoid defines a linear map.
This is a stronger version of DistribMulAction.toAddMonoidHom
.
Equations
Instances For
Each element of the monoid defines a module endomorphism.
This is a stronger version of DistribMulAction.toAddMonoidEnd
.
Equations
Instances For
Each element of the semiring defines a module endomorphism.
This is a stronger version of DistribMulAction.toModuleEnd
.
Equations
Instances For
The canonical (semi)ring isomorphism from Rᵐᵒᵖ
to Module.End R R
induced by the right
multiplication.
Equations
Instances For
The canonical (semi)ring isomorphism from R
to Module.End Rᵐᵒᵖ R
induced by the left
multiplication.
Equations
Instances For
Alias of RingEquiv.moduleEndSelf
.
The canonical (semi)ring isomorphism from Rᵐᵒᵖ
to Module.End R R
induced by the right
multiplication.
Equations
Instances For
Alias of RingEquiv.moduleEndSelfOp
.
The canonical (semi)ring isomorphism from R
to Module.End Rᵐᵒᵖ R
induced by the left
multiplication.
Equations
Instances For
When f
is an R
-linear map taking values in S
, then fun b ↦ f b • x
is an R
-linear
map.
Equations
Instances For
Applying a linear map at v : M
, seen as S
-linear map from M →ₗ[R] M₂
to M₂
.
See LinearMap.applyₗ
for a version where S = R
.
Equations
Instances For
Composition by f : M₂ → M₃
is a linear map from the space of linear maps M → M₂
to the space of linear maps M → M₃
.
Equations
Instances For
Applying a linear map at v : M
, seen as a linear map from M →ₗ[R] M₂
to M₂
.
See also LinearMap.applyₗ'
for a version that works with two different semirings.
This is the LinearMap
version of toAddMonoidHom.eval
.
Equations
Instances For
The family of linear maps M₂ → M
parameterised by f ∈ M₂ → R
, x ∈ M
, is linear in f
, x
.