nLab
equation
Contents
Context
Equality and Equivalence
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
gauge equivalence
Examples.
principle of equivalence
equation
fiber product , pullback
homotopy pullback
Examples.
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
Contents
Definition
An equation is a proposition of equality .
For
x : X ⊢ ϕ ( x ) : Z
x : X \vdash \phi(x) : Z
and
y : Y ⊢ ψ ( y ) : Z
y : Y \vdash \psi(y) : Z
two terms of some type Z Z dependent on variables x x of type X X and y y of type Y Y , respectively, the equation asserting that these two formulas are equal is as a proposition the bracket type
x : X , y : Y ⊢ [ ϕ ( x ) = ψ ( y ) ] : Type
x : X, y : Y \vdash [\phi(x) = \psi(y)] : Type
and as a not-neccessarily (-1)-truncated type just the identity type
x : X , y : Y ⊢ ( ϕ ( x ) = ψ ( y ) ) : Type
x : X, y : Y \vdash (\phi(x) = \psi(y)) : Type
itself.
The space of solutions of this equation is the dependent sum over all pairs of terms for which equality holds
⊢ ∑ x : X y : Y ( ϕ ( x ) = ψ ( y ) ) : Type .
\vdash \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y)) : Type
\,.
Hence a particular solution sol sol is a term of this type
⊢ sol : ∑ x : X y : Y ( ϕ ( x ) = ψ ( y ) ) ,
\vdash sol : \sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y))
\,,
which means that it is a triple consisting of an x ∈ X x \in X , a y ∈ Y y \in Y and a witness eq : ( ϕ ( x ) = ψ ( y ) ) eq : (\phi(x) = \psi(y)) that these indeed solve the equation.
In categorical semantics this means that the space of solutions to an equation between expression ϕ ( x ) : Z \phi(x) : Z and ψ ( y ) : Z \psi(y) : Z of type Z Z depending on variables of type X X and Y Y , respectively is the pullback
∑ x : X y : Y ( ϕ ( x ) = ψ ( y ) ) → Y ↓ ↓ ψ X → ϕ Z ,
\array{
\sum_{{x : X} \atop {y : Y}} (\phi(x) = \psi(y))
&\to& Y
\\
\downarrow && \downarrow^{\mathrlap{\psi}}
\\
X &\stackrel{\phi}{\to}& Z
}
\,,
the fiber product of ϕ \phi with ψ \psi . In the context of homotopy type theory this is the homotopy pullback /homotopy fiber product .
See at homotopy pullback – concrete constructions – In homotopy type theory for more on this.
Examples
Last revised on September 11, 2019 at 06:32:37.
See the history of this page for a list of all contributions to it.