equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
Since generally an equation is the statement of equality of two functions and of variables and , so a linear equation is an equation between linear functions.
Typically here a linear function is taken to mean an -linear map over some given ring , hence a homomorphism or of (say left) -modules Mod. If here is an -module of rank greater than 1, one also speaks of a system of linear equations.
Specifically if is a field then these are linear maps of -vector spaces and hence in this case a linear equation is a statement of equality of two vectors in some vector space that depend linearly on vectors in a vector spaces and .
Frequently this is considered specifically for the case that is a constant function, hence just a fixed vector . In this case the linear equation becomes for . If moreover here is represented or representable by a matrix this is typically written as
which is the form that one finds in standard textbooks on linear algebra. If here this is called a homogeneous linear equation.
But linear equations make sense and are important in the greater generality where is not necessarily a field, and in fact in contexts more general than that of -modules even. For instance natural isomorphisms between linear functors are a kind of categorification of linear equations.
Indeed, as discussed at equation, in the formal logic of type theory a an equation as above is a judgement of the form
whose solution space is the dependent sum
and reading this in fact in homotopy type theory says that are homotopy types.
The generalization of a ring to a homotopy type is an E-∞-ring and that of an -module is a module spectrum.
Accordingly a linear equation in homotopy(type) homotopy theory is a statement of equivalence between elements of an -module spectrum that depend -linearly on other -module spectra. More precisely, as discussed at equation, the solution space to such an “-linear equation” is the homotopy pullback
in an (∞,1)-category of -∞-modules.
We discuss solution space of homogeneous linear equations in the general context of linear algebra over a ring (not necessarily a field).
So let be a ring and let Mod be an -module.
Let and let be an an matrix with entries in . By matrix multiplication this defines a linear function
which takes the element to the element with
Consider dually the linear map
on the free modules over .
Consider the quotient module of by the image of this map
hence the cokernel of the map, fitting in the exact sequence
Here the morphism on the left is also called the inclusion of the syzygies of the module on the right.
Applying the left exact hom functor to this yields exact sequence
This identifies as the space of solutions of the homogeneous linear equation .
(…)
For a ring, there is close relation between
-linear equations in finitely many variables;
syzygies in these -modules
and projective resolutions of these -modules.
These relations we discuss in the following.
(…)
Discussion in the context of syzygies and projective resolutions of modules is for instance in section 4.5 of
Linear equations over skewfields were studied in
and more lately in the theory of quasideterminants, see there.
Last revised on May 21, 2024 at 09:39:20. See the history of this page for a list of all contributions to it.