Linear algebra
This file defines the basics of linear algebra. It sets up the "categorical/lattice structure" of
modules over a ring, submodules, and linear maps. If p
and q
are submodules of a module, p ≤ q
means that p ⊆ q
.
Many of the relevant definitions, including module
, submodule
, and linear_map
, are found in
src/algebra/module
.
Main definitions
- Many constructors for linear maps, including
prod
andcoprod
submodule.span s
is defined to be the smallest submodule containing the sets
.- If
p
is a submodule ofM
,submodule.quotient p
is the quotient ofM
with respect top
: that is, elements ofM
are identified if their difference is inp
. This is itself a module. - The kernel
ker
and rangerange
of a linear map are submodules of the domain and codomain respectively. - The general linear group is defined to be the group of invertible linear maps from
M
to itself.
Main statements
- The first and second isomorphism laws for modules are proved as
quot_ker_equiv_range
andquotient_inf_equiv_sup_quotient
.
Notations
- We continue to use the notation
M →ₗ[R] M₂
for the type of linear maps fromM
toM₂
over the ringR
. - We introduce the notations
M ≃ₗ M₂
andM ≃ₗ[R] M₂
forlinear_equiv M M₂
. In the first, the ringR
is implicit. - We introduce the notation
R ∙ v
for the span of a singleton,submodule.span R {v}
. This is\.
, not the same as the scalar multiplication•
/\bub
.
Implementation notes
We note that, when constructing linear maps, it is convenient to use operations defined on bundled
maps (prod
, coprod
, arithmetic operations like +
) instead of defining a function and proving
it is linear.
Tags
linear algebra, vector space, module
Properties of linear maps
The restriction of a linear map f : M → M₂
to a submodule p ⊆ M
gives a linear map
p → M₂
.
Equations
- f.dom_restrict p = f.comp p.subtype
A linear map f : M₂ → M
whose values lie in a submodule p ⊆ M
can be restricted to a
linear map M₂ → p.
Restrict domain and codomain of an endomorphism.
Equations
- f.restrict hf = linear_map.cod_restrict p (f.dom_restrict p) _
The constant 0 map is linear.
Equations
- linear_map.inhabited = {default := 0}
Equations
- linear_map.unique_of_left = {to_inhabited := {default := default (M →ₗ[R] M₂) linear_map.inhabited}, uniq := _}
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 := _, add_comm := _}
λb, f b • x
is a linear map.
Equations
- linear_map.has_one = {one := linear_map.id _inst_6}
Equations
- linear_map.has_mul = {mul := linear_map.comp _inst_6}
Equations
- linear_map.monoid = {mul := has_mul.mul linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
A linear map f
applied to x : ι → R
can be computed using the image under f
of elements
of the canonical basis.
The first projection of a product is a linear map.
The second projection of a product is a linear map.
The prod of two linear maps is a linear map.
The left injection into a product is a linear map.
Equations
- linear_map.inl R M M₂ = {to_fun := ⇑(add_monoid_hom.inl M M₂), map_add' := _, map_smul' := _}
The right injection into a product is a linear map.
Equations
- linear_map.inr R M M₂ = {to_fun := ⇑(add_monoid_hom.inr M M₂), map_add' := _, map_smul' := _}
The coprod function λ x : M × M₂, f x.1 + g x.2
is a linear map.
prod.map
of two linear maps.
Equations
- f.prod_map g = (f.comp (linear_map.fst R M M₂)).prod (g.comp (linear_map.snd R M M₂))
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 := _, neg := has_neg.neg linear_map.has_neg, sub := has_sub.sub linear_map.has_sub, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}
Equations
- linear_map.distrib_mul_action = {to_mul_action := {to_has_scalar := linear_map.has_scalar _inst_10, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Equations
- linear_map.semimodule = {to_distrib_mul_action := linear_map.distrib_mul_action _inst_11, add_smul := _, zero_smul := _}
Applying a linear map at v : M
, seen as S
-linear map from M →ₗ[R] M₂
to M₂
.
See applyₗ
for a version where S = R
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₃
.
Applying a linear map at v : M
, seen as a linear map from M →ₗ[R] M₂
to M₂
.
See also linear_map.applyₗ'
for a version that works with two different semirings.
Equations
Equations
- linear_map.endomorphism_semiring = {add := add_comm_monoid.add linear_map.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero linear_map.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
Equations
- linear_map.endomorphism_ring = {add := semiring.add linear_map.endomorphism_semiring, add_assoc := _, zero := semiring.zero linear_map.endomorphism_semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg linear_map.add_comm_group, sub := add_comm_group.sub linear_map.add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul linear_map.endomorphism_semiring, mul_assoc := _, one := semiring.one linear_map.endomorphism_semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
The family of linear maps M₂ → M
parameterised by f ∈ M₂ → R
, x ∈ M
, is linear in f
, x
.
Properties of submodules
Equations
- submodule.partial_order = {le := λ (p p' : submodule R M), ∀ ⦃x : M⦄, x ∈ p → x ∈ p', lt := partial_order.lt (partial_order.lift coe submodule.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
If two submodules p
and p'
satisfy p ⊆ p'
, then of_le p p'
is the linear map version of
this inclusion.
Equations
- submodule.of_le h = linear_map.cod_restrict p' p.subtype _
The set {0}
is the bottom element of the lattice of submodules.
Equations
Equations
- submodule.order_bot = {bot := ⊥, le := partial_order.le submodule.partial_order, lt := partial_order.lt submodule.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
The universal set is the top element of the lattice of submodules.
Equations
- submodule.order_top = {top := ⊤, le := partial_order.le submodule.partial_order, lt := partial_order.lt submodule.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
Equations
- submodule.complete_lattice = {sup := λ (a b : submodule R M), Inf {x : submodule R M | a ≤ x ∧ b ≤ x}, le := order_top.le submodule.order_top, lt := order_top.lt submodule.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf submodule.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top submodule.order_top, le_top := _, bot := order_bot.bot submodule.order_bot, bot_le := _, Sup := λ (tt : set (submodule R M)), Inf {t : submodule R M | ∀ (t' : submodule R M), t' ∈ tt → t' ≤ t}, Inf := Inf submodule.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
Equations
- submodule.add_comm_monoid_submodule = {add := has_sup.sup (semilattice_sup.to_has_sup (submodule R M)), add_assoc := _, zero := ⊥, zero_add := _, add_zero := _, add_comm := _}
The pushforward of a submodule p ⊆ M
by f : M → M₂
The pullback of a submodule p ⊆ M₂
along f : M → M₂
The span of a set s ⊆ M
is the smallest submodule of M that contains s
.
An induction principle for span membership. If p
holds for 0 and all elements of s
, and is
preserved under addition and scalar multiplication, then p
holds for all elements of the span of
s
.
span
forms a Galois insertion with the coercion from submodule to set.
Equations
- submodule.gi R M = {choice := λ (s : set M) (_x : ↑(submodule.span R s) ≤ s), submodule.span R s, gc := _, le_l_u := _, choice_eq := _}
The product of two submodules is a submodule.
The equivalence relation associated to a submodule p
, defined by x ≈ y
iff y - x ∈ p
.
The quotient of a module M
by a submodule p ⊆ M
.
Equations
Map associating to an element of M
the corresponding element of M/p
,
when p
is a submodule of M
.
Equations
Equations
Equations
- submodule.quotient.inhabited p = {default := 0}
Equations
- submodule.quotient.has_add p = {add := λ (a b : p.quotient), quotient.lift_on₂' a b (λ (a b : M), submodule.quotient.mk (a + b)) _}
Equations
- submodule.quotient.has_neg p = {neg := λ (a : p.quotient), quotient.lift_on' a (λ (a : M), submodule.quotient.mk (-a)) _}
Equations
- submodule.quotient.has_sub p = {sub := λ (a b : p.quotient), quotient.lift_on₂' a b (λ (a b : M), submodule.quotient.mk (a - b)) _}
Equations
- submodule.quotient.add_comm_group p = {add := has_add.add (submodule.quotient.has_add p), add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg (submodule.quotient.has_neg p), sub := has_sub.sub (submodule.quotient.has_sub p), sub_eq_add_neg := _, add_left_neg := _, add_comm := _}
Equations
- submodule.quotient.has_scalar p = {smul := λ (a : R) (x : p.quotient), quotient.lift_on' x (λ (x : M), submodule.quotient.mk (a • x)) _}
Equations
- submodule.quotient.semimodule p = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul (submodule.quotient.has_scalar p)}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
Properties of linear maps
If two linear maps are equal on a set s
, then they are equal on submodule.span s
.
See also linear_map.eq_on_span'
for a version using set.eq_on
.
If two linear maps are equal on a set s
, then they are equal on submodule.span s
.
This version uses set.eq_on
, and the hidden argument will expand to h : x ∈ (span R s : set M)
.
See linear_map.eq_on_span
for a version that takes h : x ∈ span R s
as an argument.
If s
generates the whole semimodule and linear maps f
, g
are equal on s
, then they are
equal.
If the range of v : ι → M
generates the whole semimodule and linear maps f
, g
are equal at
each v i
, then they are equal.
The range of a linear map f : M → M₂
is a submodule of M₂
.
Equations
- f.range = submodule.map f ⊤
Restrict the codomain of a linear map f
to f.range
.
Equations
- f.range_restrict = linear_map.cod_restrict f.range f _
Given an element x
of a module M
over R
, the natural map from
R
to scalar multiples of x
.
Equations
The range of to_span_singleton x
is the span of x
.
The kernel of a linear map f : M → M₂
is defined to be comap f ⊥
. This is equivalent to the
set of x : M
such that f x = 0
. The kernel is a submodule of M
.
Equations
- f.ker = submodule.comap f ⊥