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.lean.
We note that, when constructing linear maps, it is convenient to use operations defined on bundled maps (pair, copair, arithmetic operations like +) instead of defining a function and proving it is linear.
linear algebra, vector space, module
A linear map f : M₂ → M whose values lie in a submodule p ⊆ M can be restricted to a linear map M₂ → p.
If a function g is a left and right inverse of a linear map f, then g is linear itself.
The constant 0 map is linear.
The negation of a linear map is linear.
The sum of two linear maps is linear.
The type of linear maps is an additive group.
λb, f b • x is a linear map.
The first projection of a product is a linear map.
The second projection of a product is a linear map.
The pair of two linear maps is a linear map.
The left injection into a product is a linear map.
The right injection into a product is a linear map.
The copair function λ x : M × M₂, f x.1 + g x.2 is a linear map.
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₃.
If two submodules p and p' satisfy p ⊆ p', then of_le p p' is the linear map version of this inclusion.
The set {0} is the bottom element of the lattice of submodules.
The universal set is the top element of the lattice of submodules.
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.
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.
Map associating to an element of M the corresponding element of M/p, when p is a submodule of M.
The range of a linear map f : M → M₂ is a submodule of M₂.
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.
If N ⊆ M then submodules of N are the same as submodules of M contained in N
If p ⊆ M is a submodule, the ordering of submodules of p is embedded in the ordering of submodules of M.
If p ⊆ M is a submodule, the ordering of submodules of p is embedded in the ordering of submodules of M.
The map from a module M to the quotient of M by a submodule p is a linear map.
The map from the quotient of M by a submodule p to M₂ along f : M → M₂ is linear.
The map from the quotient of M by submodule p to the quotient of M₂ by submodule q along f : M → M₂ is linear.
The correspondence theorem for modules: there is an order isomorphism between submodules of the quotient of M by p, and submodules of M larger than p.
The ordering on submodules of the quotient of M by p embeds into the ordering on submodules of M.
The ordering on submodules of the quotient of M by p embeds into the ordering on submodules of M.
A linear equivalence is an invertible linear map.
The identity map is a linear equivalence.
Linear equivalences are symmetric.
Linear equivalences are transitive.
A bijective linear map is a linear equivalence. Here, bijectivity is described by saying that the kernel of f is {0} and the range is the universal set.
If a linear map has an inverse, it is a linear equivalence.
The top submodule of M is linearly equivalent to M.
Multiplying by a unit a of the ring R is a linear equivalence.
A linear isomorphism between the domains and codomains of two spaces of linear maps gives a linear isomorphism between the two function spaces.
If M₂ and M₃ are linearly isomorphic then the two spaces of linear maps from M into M₂ and M into M₃ are linearly isomorphic.
If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to themselves are linearly isomorphic.
Multiplying by a nonzero element a of the field K is a linear equivalence.
An equivalence whose underlying function is linear is a linear equivalence.
The first isomorphism law for modules. The quotient of M by the kernel of f is linearly equivalent to the range of f.
Canonical linear map from the quotient p/(p ∩ p') to (p+p')/p', mapping x + (p ∩ p') to x + p', where p and p' are submodules of an ambient module.
Second Isomorphism Law : the canonical map from p/(p ∩ p') to (p+p')/p' as a linear isomorphism.
The cartesian product of two linear maps as a linear map.
pi construction for linear functions. From a family of linear functions it produces a linear function into a family of modules.
The projections from a family of modules are linear maps.
If I and J are disjoint index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.
diag i j is the identity map if i = j. Otherwise it is the constant 0 map.
The standard basis of the product of φ.
The group of invertible linear maps from M to itself
An invertible linear map f determines an equivalence from M to itself.
An equivalence from M to itself determines an invertible linear map.
The general linear group on R and M is multiplicatively equivalent to the type of linear equivalences between M and itself.