14.1. Modules and vector spaces
Vector spaces and modules are covered in Mathematics in Lean; this section assumes you have read the linked section. As a complement to MiL, this section of the phrasebook discusses:
-
more details on modules and semi-modules
-
common examples of modules and vector spaces
-
semilinear maps
Recall from Mathematics in Lean that
Mathlib has one typeclass called Module that can be used in combination with other classes
to express semimodules, modules and vector spaces in a uniform way.
The defining characteristic shared between modules and vector spaces is the properties of their scalar multiplication.
Scalar multiplication is written (· • ·) (\bu) and called smul in declaration names,
so for example associativity of multiplication is written (x * y) • v = x • (y • v) (see mul_smul).
To say V is a vector space over the field K, write:
variable {K V : Type*}
[Field K] [AddCommGroup V] [Module K V]
To say M is a module over the ring R, write:
variable {R M : Type*}
[Ring R] [AddCommGroup M] [Module R M]
To say M is a semimodule over the semiring R, write:
variable {R M : Type*}
[Semiring R] [AddCommMonoid M] [Module R M]
The Module R M parameter specifies the behaviour of scalar multiplication, while AddCommMonoid M (and its descendants) and Semiring R (and its descendants) specify behaviour of operations that stay within M and R respectively, such as (· + ·) and (· * ·) respectively.
In this document, we'll use "module" to mean "semimodule, module, or vector space" and "ring" to mean "semiring, ring, or field" if the distinction between those does not matter.
Lean cannot automatically infer that M has negation if R has,
because a priori it cannot guess the correct R given an arbitrary M.
So if we declare variables like:
variable [Ring R] [AddCommMonoid M] [Module R M]
then trying to negate elements of M will fail.
#check fun x : M => -x
The solution is to either declare [AddCommGroup M] in your variables,
or to add the instance inline using Module.addCommMonoidToAddCommGroup.
14.1.1. Examples of modules
The n-dimensional free module over the ring R is written Fin n → R.
Mathlib provides a module structure on the function type i → R for any type i.
It is generally a good idea to use i → R instead of Fin n → R,
unless the order of the indexing elements matters.
The direct sum of copies of R is written i →₀ R,
and the linear equivalence with i → R in the finite case is called Finsupp.linearEquivFunOnFinite.
A ring is a module over itself, with scalar multiplication equal to multiplication.
This module structure is found by typeclass inference. Use smul_eq_mul to state this equality.
Finally, an additive monoid M is a module over the natural numbers,
with the scalar multiplication n • x defined as x + x + ... + x, n times.
Analogously, additive groups are modules over the integers.
These module structures are found by typeclass inference.
14.1.2. Linear maps and semilinear maps
Recall from Mathematics in Lean the definition of a linear map in Mathlib:
For two R-modules M₁, M₂,
the type M₁ →ₗ[R] M₂ (called LinearMap in declaration names)
contains the bundled R-linear maps from M₁ to M₂.
These are maps that preserve zero (see map_zero), addition (see map_add) and scalar multiplication (see map_smul).
The type M₁ ≃ₗ[R] M₂ (called LinearEquiv) contains the bundled R-linear equivalences
between M₁ and M₂: these are the invertible linear maps.
In Mathlib, the types LinearMap and LinearEquiv actually denote semilinear maps and equivalences.
If N is an S-module and (σ : R →+* S) is a ring homomorphism, then
a semilinear map (f : M →ₛₗ[σ] N) preserves scalar multiplication only up to σ:
#check map_smulₛₗ f
The notation M₁ →ₗ[R] M₂ stands for M₁ →ₛₗ[RingHom.id R] M₂.
Since LinearMap can denote both linear and semilinear map,
it is clearer to always use the →ₗ and →ₛₗ notation.
Composing a σ-semilinear and a τ-semilinear map requires Lean to
figure out the composition of σ with τ.
In order to do so, you need to have declared an instance of RingHomCompTriple σ τ _.
For example, that two conjugate-linear maps compose to form a linear map would be expressed
by an instance of type RingHomCompTriple conj conj (RingHom.id ℂ).
Semilinear equivalences are the analogous generalization of linear equivalences,
also requiring that the ring homomorphism σ be invertible.
The RingHomInvPair class expresses this condition.
If you use a ring homomorphism without further assumptions, you will see an error like:
example (σ : R →+* S)
(e : M ≃ₛₗ[σ] N) : N ≃ₛₗ[σ] M := e.symm
The fix is to add the inverse map (σ' : S →+* R) and two RingHomInvPair instances to the context.
The inverse map will be automatically picked up by LinearEquiv.symm.
example (σ : R →+* S) (σ' : S →+* R)
[RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
(e : M ≃ₛₗ[σ] N) : N ≃ₛₗ[σ'] M := e.symm
Note that there is no automatic RingHomInvPair instance for ring isomorphisms:
example (σ : R ≃+* S) (e : M ≃ₛₗ[σ.toRingHom] N) :
N ≃ₛₗ[σ.symm.toRingHom] M := e.symm
Instead, define instances for specific values of σ.
Beware that an instance of the form RingHomInvPair σ.toRingHom σ.symm.toRingHom where σ is a variable
will result in e.symm.symm getting the type M ≃ₛₗ[σ.symm.symm] N instead of the expected M ≃ₛₗ[σ] N.
Background reading on semilinear maps in Mathlib is available in the article Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In ITP 2022.