(Semi)linear maps #
In this file we define
LinearMap σ M M₂
,M →ₛₗ[σ] M₂
: a semilinear map between twoModule
s. Here,σ
is aRingHom
fromR
toR₂
and anf : M →ₛₗ[σ] M₂
satisfiesf (c • x) = (σ c) • (f x)
. We recover plain linear maps by choosingσ
to beRingHom.id R
. This is denoted byM →ₗ[R] M₂
. We also add the notationM →ₗ⋆[R] M₂
for star-linear maps.IsLinearMap R f
: predicate saying thatf : M → M₂
is a linear map. (Note that this was not generalized to semilinear maps.)
We then provide LinearMap
with the following instances:
LinearMap.addCommMonoid
andLinearMap.addCommGroup
: the elementwise addition structures corresponding to addition in the codomainLinearMap.distribMulAction
andLinearMap.module
: the elementwise scalar action structures corresponding to applying the action in the codomain.
Implementation notes #
To ensure that composition works smoothly for semilinear maps, we use the typeclasses
RingHomCompTriple
, RingHomInvPair
and RingHomSurjective
from
Mathlib/Algebra/Ring/CompTypeclasses.lean
.
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.
CompatibleSMul
)
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 IsLinearMap R f
asserts this
property. A bundled version is available with LinearMap
, and should be favored over
IsLinearMap
most of the time.
A linear map preserves addition.
A linear map preserves scalar multiplication.
Instances For
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 LinearMap σ M M₂
(available under the notation
M →ₛₗ[σ] M₂
) are bundled versions of such maps. For plain linear maps (i.e. for which
σ = RingHom.id R
), the notation M →ₗ[R] M₂
is available. An unbundled version of plain linear
maps is available with the predicate IsLinearMap
, but it should be avoided most of the time.
- toFun : M → M₂
Instances For
M →ₛₗ[σ] N
is the type of σ
-semilinear maps from M
to N
.
Equations
Instances For
M →ₗ[R] N
is the type of R
-linear maps from M
to N
.
Equations
Instances For
SemilinearMapClass F σ M M₂
asserts F
is a type of bundled σ
-semilinear maps M → M₂
.
See also LinearMapClass F R M M₂
for the case where σ
is the identity map on R
.
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
.
Instances
LinearMapClass F R M M₂
asserts F
is a type of bundled R
-linear maps M → M₂
.
This is an abbreviation for SemilinearMapClass F (RingHom.id R) M M₂
.
Equations
Instances For
Reinterpret an element of a type of semilinear maps as a semilinear map.
Equations
Instances For
Reinterpret an element of a type of semilinear maps as a semilinear map.
Equations
Reinterpret an element of a type of linear maps as a linear map.
Equations
Instances For
Reinterpret an element of a type of linear maps as a linear map.
Equations
The DistribMulActionHom
underlying a LinearMap
.
Equations
Instances For
Copy of a LinearMap
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Equations
Instances For
Identity map as a LinearMap
Equations
Instances For
A generalisation of LinearMap.id
that constructs the identity function
as a σ
-semilinear map for any ring homomorphism σ
which we know is the identity.
Equations
Instances For
If two linear maps are equal, they are equal at each point.
A typeclass for SMul
structures which can be moved through a LinearMap
.
This typeclass is generated automatically from an IsScalarTower
instance, but exists so that
we can also add an instance for AddCommGroup.toIntModule
, allowing z •
to be moved even if
S
does not support negation.
Scalar multiplication by
R
ofM
can be moved through linear maps.
Instances
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 LinearMap.map_smul_of_tower
.
Equations
Instances For
Equations
Composition of two linear maps is a linear map
Equations
Instances For
∘ₗ
is notation for composition of two linear (not semilinear!) maps into a linear map.
This is useful when Lean is struggling to infer the RingHomCompTriple
instance.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
Composition of two linear maps is a linear map
Equations
Instances For
The linear map version of Function.Surjective.injective_comp_right
The linear map version of Function.Injective.comp_left
If a function g
is a left and right inverse of a linear map f
, then g
is linear itself.
Equations
Instances For
g : R →+* S
is R
-linear when the module structure on S
is Module.compHom S g
.
Equations
Instances For
A DistribMulActionHom
between two modules is a linear map.
Equations
Instances For
A DistribMulActionHom
between two modules is a linear map.
Equations
Instances For
A DistribMulActionHom
between two modules is a linear map.
Convert an IsLinearMap
predicate to a LinearMap
Equations
Instances For
Reinterpret an additive homomorphism as an ℕ
-linear map.
Equations
Instances For
Reinterpret an additive homomorphism as a ℤ
-linear map.
Equations
Instances For
Equations
Arithmetic on the codomain #
Equations
Equations
The type of linear maps is an additive monoid.
Equations
The type of linear maps is an additive group.
Equations
Evaluation of a σ₁₂
-linear map at a fixed a
, as an AddMonoidHom
.
Equations
Instances For
LinearMap.toAddMonoidHom
promoted to an AddMonoidHom
.
Equations
Instances For
If M
is the zero module, then the identity map of M
is the zero map.
Equations
Equations
LinearMap.restrictScalars
as a LinearMap
.