(Semi)linear maps #
In this file we define
-
linear_map σ M M₂
,M →ₛₗ[σ] M₂
: a semilinear map between twomodule
s. Here,σ
is aring_hom
fromR
toR₂
and anf : M →ₛₗ[σ] M₂
satisfiesf (c • x) = (σ c) • (f x)
. We recover plain linear maps by choosingσ
to bering_hom.id R
. This is denoted byM →ₗ[R] M₂
. We also add the notationM →ₗ⋆[R] M₂
for star-linear maps. -
is_linear_map R f
: predicate saying thatf : M → M₂
is a linear map. (Note that this was not generalized to semilinear maps.)
We then provide linear_map
with the following instances:
linear_map.add_comm_monoid
andlinear_map.add_comm_group
: the elementwise addition structures corresponding to addition in the codomainlinear_map.distrib_mul_action
andlinear_map.module
: the elementwise scalar action structures corresponding to applying the action in the codomain.module.End.semiring
andmodule.End.ring
: the (semi)ring of endomorphisms formed by taking the additive structure above with composition as multiplication.
Implementation notes #
To ensure that composition works smoothly for semilinear maps, we use the typeclasses
ring_hom_comp_triple
, ring_hom_inv_pair
and ring_hom_surjective
from
algebra/ring/comp_typeclasses
.
Notation #
- Throughout the file, we denote regular linear maps by
fₗ
,gₗ
, etc, and semilinear maps byf
,g
, etc.
TODO #
- Parts of this file have not yet been generalized to semilinear maps (i.e.
compatible_smul
)
Tags #
linear map
A map f
between modules over a semiring is linear if it satisfies the two properties
f (x + y) = f x + f y
and f (c • x) = c • f x
. The predicate is_linear_map R f
asserts this
property. A bundled version is available with linear_map
, and should be favored over
is_linear_map
most of the time.
- to_fun : M → M₂
- map_add' : ∀ (x y : M), self.to_fun (x + y) = self.to_fun x + self.to_fun y
- map_smul' : ∀ (r : R) (x : M), self.to_fun (r • x) = ⇑σ r • self.to_fun x
A map f
between an R
-module and an S
-module over a ring homomorphism σ : R →+* S
is semilinear if it satisfies the two properties f (x + y) = f x + f y
and
f (c • x) = (σ c) • f x
. Elements of linear_map σ M M₂
(available under the notation
M →ₛₗ[σ] M₂
) are bundled versions of such maps. For plain linear maps (i.e. for which
σ = ring_hom.id R
), the notation M →ₗ[R] M₂
is available. An unbundled version of plain linear
maps is available with the predicate is_linear_map
, but it should be avoided most of the time.
The add_hom
underlying a linear_map
.
Equations
- linear_map.add_monoid_hom_class = {coe := linear_map.to_fun _inst_12, coe_injective' := _, map_add := _, map_zero := _}
The distrib_mul_action_hom
underlying a linear_map
.
Helper instance for when there's too many metavariables to apply to_fun.to_coe_fn
directly.
Equations
- linear_map.has_coe_to_fun = {coe := linear_map.to_fun _inst_12}
Copy of a linear_map
with a new to_fun
equal to the old one. Useful to fix definitional
equalities.
Identity map as a linear_map
If two linear maps are equal, they are equal at each point.
A typeclass for has_scalar
structures which can be moved through a linear_map
.
This typeclass is generated automatically from a is_scalar_tower
instance, but exists so that
we can also add an instance for add_comm_group.int_module
, allowing z •
to be moved even if
R
does not support negation.
Equations
convert a linear map to an additive map
If M
and M₂
are both R
-modules and S
-modules and R
-module structures
are defined by an action of R
on S
(formally, we have two scalar towers), then any S
-linear
map from M
to M₂
is R
-linear.
See also linear_map.map_smul_of_tower
.
Composition of two linear maps is a linear map
If a function g
is a left and right inverse of a linear map f
, then g
is linear itself.
Equations
Equations
A distrib_mul_action_hom
between two modules is a linear map.
Equations
Convert an is_linear_map
predicate to a linear_map
Linear endomorphisms of a module, with associated ring structure
module.End.semiring
and algebra structure module.End.algebra
.
Reinterpret an additive homomorphism as a ℕ
-linear map.
Reinterpret an additive homomorphism as a ℤ
-linear map.
Reinterpret an additive homomorphism as a ℚ
-linear map.
Arithmetic on the codomain #
The constant 0 map is linear.
Equations
- linear_map.inhabited = {default := 0}
The sum of two linear maps is linear.
The type of linear maps is an additive monoid.
Equations
- linear_map.add_comm_monoid = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (f : M →ₛₗ[σ₁₂] M₂), {to_fun := λ (x : M), n • ⇑f x, map_add' := _, map_smul' := _}, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
The negation of a linear map is linear.
The negation of a linear map is linear.
The type of linear maps is an additive group.
Equations
- linear_map.add_comm_group = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (f : M →ₛₗ[σ₁₂] N₂), {to_fun := λ (x : M), n • ⇑f x, map_add' := _, map_smul' := _}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg linear_map.has_neg, sub := has_sub.sub linear_map.has_sub, sub_eq_add_neg := _, zsmul := λ (n : ℤ) (f : M →ₛₗ[σ₁₂] N₂), {to_fun := λ (x : M), n • ⇑f x, map_add' := _, map_smul' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Equations
- linear_map.distrib_mul_action = {to_mul_action := {to_has_scalar := linear_map.has_scalar _inst_13, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Equations
- linear_map.module = {to_distrib_mul_action := linear_map.distrib_mul_action _inst_13, add_smul := _, zero_smul := _}
Monoid structure of endomorphisms #
Lemmas about pow
such as linear_map.pow_apply
appear in later files.
Equations
- linear_map.module.End.has_one = {one := linear_map.id _inst_4}
Equations
- linear_map.module.End.has_mul = {mul := linear_map.comp linear_map.module.End.has_mul._proof_1}
Equations
- module.End.monoid = {mul := has_mul.mul linear_map.module.End.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (module.End R M)), npow_zero' := _, npow_succ' := _}
Equations
- module.End.semiring = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul linear_map.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul linear_map.module.End.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul linear_map.module.End.has_mul}, npow_zero' := _, npow_succ' := _}
Equations
- module.End.ring = {add := semiring.add module.End.semiring, add_assoc := _, zero := semiring.zero module.End.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul module.End.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg linear_map.add_comm_group, sub := add_comm_group.sub linear_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul linear_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul module.End.semiring, mul_assoc := _, one := semiring.one module.End.semiring, one_mul := _, mul_one := _, npow := semiring.npow module.End.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
Action by a module endomorphism. #
The tautological action by module.End R M
(aka M →ₗ[R] M
) on M
.
This generalizes function.End.apply_mul_action
.
Equations
- linear_map.apply_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (_x : module.End R M) (_y : M), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
linear_map.apply_module
is faithful.
Actions as module endomorphisms #
Each element of the monoid defines a linear map.
This is a stronger version of distrib_mul_action.to_add_monoid_hom
.
Equations
- distrib_mul_action.to_linear_map R M s = {to_fun := has_scalar.smul s, map_add' := _, map_smul' := _}
Each element of the monoid defines a module endomorphism.
This is a stronger version of distrib_mul_action.to_add_monoid_End
.
Equations
- distrib_mul_action.to_module_End R M = {to_fun := distrib_mul_action.to_linear_map R M _inst_6, map_one' := _, map_mul' := _}
Each element of the monoid defines a module endomorphism.
This is a stronger version of distrib_mul_action.to_module_End
.
Equations
- module.to_module_End R M = {to_fun := distrib_mul_action.to_linear_map R M _inst_6, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}