Equality and Equivalence
equality (definitional?, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence in homotopy type theory
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
natural equivalence, natural isomorphism
principle of equivalence
fiber product, pullback
linear equation, differential equation, ordinary differential equation, critical locus
Euler-Lagrange equation, Einstein equation, wave equation
Schrödinger equation, Knizhnik-Zamolodchikov equation, Maurer-Cartan equation, quantum master equation, Euler-Arnold equation, Fuchsian equation, Fokker-Planck equation, Lax equation
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.
In 1-category theory
Typically here a linear function is taken to mean an -linear map over some given ring , hence a homomorphism or of -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.
In -category theory
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.
Solution spaces of homogeneous -linear equations
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 .
Relation to syzygies and projective resolutions of modules
For a ring, there is close relation between
-linear equations in finitely many variables;
finitely generated -modules;
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