formulasearchengine - User contributions [en]

Main Page

2014-08-11T15:21:25Z

IeshaEastman:

In [[category theory]], an abstract branch of [[mathematics]], an '''equivalence of categories''' is a relation between two categories that establishes that these categories are "essentially the same". There are numerous examples of categorical equivalences from many areas of mathematics. Establishing an equivalence involves demonstrating strong similarities between the mathematical structures concerned. In some cases, these structures may appear to be unrelated at a superficial or intuitive level, making the notion fairly powerful: it creates the opportunity to "translate" theorems between different kinds of mathematical structures, knowing that the essential meaning of those theorems is preserved under the translation.

If a category is equivalent to the [[dual (category theory)|opposite (or dual)]] of another category then one speaks of
a '''duality of categories''', and says that the two categories are '''dually equivalent'''.

An equivalence of categories consists of a [[functor]] between the involved categories, which is required to have an "inverse" functor. However, in contrast to the situation common for [[isomorphism]]s in an algebraic setting, the composition of the functor and its "inverse" is not necessarily the identity mapping. Instead it is sufficient that each object be ''[[natural transformation|naturally isomorphic]]'' to its image under this composition. Thus one may describe the functors as being "inverse up to isomorphism". There is indeed a concept of [[isomorphism of categories]] where a strict form of inverse functor is required, but this is of much less practical use than the ''equivalence'' concept.

==Definition==
Formally, given two categories ''C'' and ''D'', an ''equivalence of categories'' consists of a functor ''F'' : ''C'' → ''D'', a functor ''G'' : ''D'' → ''C'', and two natural isomorphisms ε: ''FG''→'''I'''''D'' and η : '''I'''''C''→''GF''. Here ''FG'': ''D''→''D'' and ''GF'': ''C''→''C'', denote the respective compositions of ''F'' and ''G'', and '''I'''''C'': ''C''→''C'' and '''I'''''D'': ''D''→''D'' denote the ''identity functors'' on ''C'' and ''D'', assigning each object and morphism to itself. If ''F'' and ''G'' are contravariant functors one speaks of a ''duality of categories'' instead.

One often does not specify all the above data. For instance, we say that the categories ''C'' and ''D'' are ''equivalent'' (respectively ''dually equivalent'') if there exists an equivalence (respectively duality) between them. Furthermore, we say that ''F'' "is" an equivalence of categories if an inverse functor ''G'' and natural isomorphisms as above exist. Note however that knowledge of ''F'' is usually not enough to reconstruct ''G'' and the natural isomorphisms: there may be many choices (see example below).

==Equivalent characterizations==
One can show that a functor ''F'' : ''C'' → ''D'' yields an equivalence of categories if and only if it is:
* [[full functor|full]], i.e. for any two objects ''c''1 and ''c''2 of ''C'', the map Hom''C''(''c''1,''c''2) → Hom''D''(''Fc''1,''Fc''2) induced by ''F'' is [[surjective]];
* [[faithful functor|faithful]], i.e. for any two objects ''c''1 and ''c''2 of ''C'', the map Hom''C''(''c''1,''c''2) → Hom''D''(''Fc''1,''Fc''2) induced by ''F'' is [[injective]]; and
* [[essentially surjective functor|essentially surjective (dense)]], i.e. each object ''d'' in ''D'' is isomorphic to an object of the form ''Fc'', for ''c'' in ''C''.
This is a quite useful and commonly applied criterion, because one does not have to explicitly construct the "inverse" ''G'' and the natural isomorphisms between ''FG'', ''GF'' and the identity functors. On the other hand, though the above properties guarantee the ''existence'' of a categorical equivalence (given a sufficiently strong version of the [[axiom of choice]] in the underlying set theory), the missing data is not completely specified, and often there are many choices. It is a good idea to specify the missing constructions explicitly whenever possible.
Due to this circumstance, a functor with these properties is sometimes called a '''weak equivalence of categories''' (unfortunately this conflicts with terminology from homotopy theory).

There is also a close relation to the concept of [[adjoint functors]]. The following statements are equivalent for functors ''F'' : ''C'' → ''D'' and ''G'' : ''D'' → ''C'':
* There are natural isomorphisms from ''FG'' to '''I'''''D'' and '''I'''''C'' to ''GF''.
* ''F'' is a left adjoint of ''G'' and both functors are full and faithful.
* ''F'' is a right adjoint of ''G'' and both functors are full and faithful.
One may therefore view an adjointness relation between two functors as a "very weak form of equivalence". Assuming that the natural transformations for the adjunctions are given, all of these formulations allow for an explicit construction of the necessary data, and no choice principles are needed. The key property that one has to prove here is that the ''counit'' of an adjunction is an isomorphism if and only if the right adjoint is a full and faithful functor.

==Examples==
* Consider the category <math>C</math> having a single object <math>c</math> and a single morphism <math>1_{c}</math>, and the category <math>D</math> with two objects <math>d_{1}</math>, <math>d_{2}</math> and four morphisms: two identity morphisms <math>1_{d_{1}}</math>, <math>1_{d_{2}}</math> and two isomorphisms <math>\alpha \colon d_{1} \to d_{2}</math> and <math>\beta \colon d_{2} \to d_{1}</math>. The categories <math>C</math> and <math>D</math> are equivalent; we can (for example) have <math>F</math> map <math>c</math> to <math>d_{1}</math> and <math>G</math> map both objects of <math>D</math> to <math>c</math> and all morphisms to <math>1_{c}</math>.

* By contrast, the category <math>C</math> with a single object and a single morphism is ''not'' equivalent to the category <math>E</math> with two objects and only two identity morphisms as the two objects therein are ''not'' isomorphic.

* Consider a category <math>C</math> with one object <math>c</math>, and two morphisms <math>1_{c}, f \colon c \to c</math>. Let <math>1_{c}</math> be the identity morphism on <math>c</math> and set <math>f \circ f = 1</math>. Of course, <math>C</math> is equivalent to itself, which can be shown by taking <math>1_{c}</math> in place of the required natural isomorphisms between the functor <math>\mathbf{I}_{C}</math> and itself. However, it is also true that <math>f</math> yields a natural isomorphism from <math>\mathbf{I}_{C}</math> to itself. Hence, given the information that the identity functors form an equivalence of categories, in this example one still can choose between two natural isomorphisms for each direction.

* Consider the category <math>C</math> of finite-[[dimension of a vector space|dimensional]] [[real number|real]] [[vector space]]s, and the category <math>D = \mathrm{Mat}(\mathbf{R})</math> of all real [[matrix (mathematics)|matrices]] (the latter category is explained in the article on [[additive category|additive categories]]). Then <math>C</math> and <math>D</math> are equivalent: The functor <math>G \colon D \to C</math> which maps the object <math>A_{n}</math> of <math>D</math> to the vector space <math>\mathbf{R}^{n}</math> and the matrices in <math>D</math> to the corresponding linear maps is full, faithful and essentially surjective.

* One of the central themes of [[algebraic geometry]] is the duality of the category of [[affine scheme]]s and the category of [[commutative ring]]s. The functor <math>G</math> associates to every commutative ring its [[spectrum of a ring|spectrum]], the scheme defined by the [[prime ideal]]s of the ring. Its adjoint <math>F</math> associates to every affine scheme its ring of global sections.

* In [[functional analysis]] the category of commutative [[C*-algebra]]s with identity is contravariantly equivalent to the category of [[compact space|compact]] [[Hausdorff space]]s. Under this duality, every compact Hausdorff space <math>X</math> is associated with the algebra of continuous complex-valued functions on <math>X</math>, and every commutative C*-algebra is associated with the space of its [[maximal ideal]]s. This is the [[Gelfand representation]].

* In [[lattice theory]], there are a number of dualities, based on representation theorems that connect certain classes of lattices to classes of [[topology|topological spaces]]. Probably the most well-known theorem of this kind is ''[[Stone's representation theorem for Boolean algebras]]'', which is a special instance within the general scheme of ''[[Stone duality]]''. Each [[Boolean algebra (structure)|Boolean algebra]] <math>B</math> is mapped to a specific topology on the set of [[lattice theory|ultrafilters]] of <math>B</math>. Conversely, for any topology the clopen (i.e. closed and open) subsets yield a Boolean algebra. One obtains a duality between the category of Boolean algebras (with their homomorphisms) and [[Stone space]]s (with continuous mappings). Another case of Stone duality is [[Birkhoff's representation theorem]] stating a duality between finite partial orders and finite distributive lattices.

* In [[pointless topology]] the category of spatial locales is known to be equivalent to the dual of the category of sober spaces.

* Any category is equivalent to its [[skeleton (category theory)|skeleton]].

==Properties==
As a rule of thumb, an equivalence of categories preserves all "categorical" concepts and properties. If ''F'' : ''C'' → ''D'' is an equivalence, then the following statements are all true:
* the object ''c'' of ''C'' is an [[initial object]] (or [[terminal object]], or [[zero object]]), [[if and only if]] ''Fc'' is an [[initial object]] (or [[terminal object]], or [[zero object]]) of ''D''
* the morphism α in ''C'' is a [[monomorphism]] (or [[epimorphism]], or [[isomorphism]]), if and only if ''Fα'' is a monomorphism (or epimorphism, or isomorphism) in ''D''.
* the functor ''H'' : ''I'' → ''C'' has [[limit (category theory)|limit]] (or colimit) ''l'' if and only if the functor ''FH'' : ''I'' → ''D'' has limit (or colimit) ''Fl''. This can be applied to [[equaliser (mathematics)|equalizers]], [[product (category theory)|product]]s and [[coproduct]]s among others. Applying it to [[kernel (category theory)|kernel]]s and [[cokernel]]s, we see that the equivalence ''F'' is an [[Regular_category#Exact_sequences_and_regular_functors|exact functor]].
* ''C'' is a [[cartesian closed category]] (or a [[topos]]) if and only if ''D'' is cartesian closed (or a topos).

Dualities "turn all concepts around": they turn initial objects into terminal objects, monomorphisms into epimorphisms, kernels into cokernels, limits into colimits etc.

If ''F'' : ''C'' → ''D'' is an equivalence of categories, and ''G''1 and ''G''2 are two inverses of ''F'', then ''G''1 and ''G''2 are naturally isomorphic.

If ''F'' : ''C'' → ''D'' is an equivalence of categories, and if ''C'' is a [[preadditive category]] (or [[additive category]], or [[abelian category]]), then ''D'' may be turned into a preadditive category (or additive category, or abelian category) in such a way that ''F'' becomes an [[additive functor]]. On the other hand, any equivalence between additive categories is necessarily additive. (Note that the latter statement is not true for equivalences between preadditive categories.)

An '''auto-equivalence''' of a category ''C'' is an equivalence ''F'' : ''C'' → ''C''. The auto-equivalences of ''C'' form a [[group (mathematics)|group]] under composition if we consider two auto-equivalences that are naturally isomorphic to be identical. This group captures the essential "symmetries" of ''C''. (One caveat: if ''C'' is not a small category, then the auto-equivalences of ''C'' may form a proper [[class (set theory)|class]] rather than a [[Set (mathematics)|set]].)

==References==
*{{Springer|id=e036050|title=Equivalence of categories}}
*{{cite book|last=Mac Lane|first=Saunders|title=Categories for the working mathematician|year=1998|publisher=Springer|location=New York|isbn=0-387-98403-8|pages=xii+314}}

{{DEFAULTSORT:Equivalence Of Categories}}
[[Category:Adjoint functors]]
[[Category:Category theory]]

[[nl:Equivalentie (categorietheorie)]]
[[zh-yue:範疇等價性]]
[[zh:范畴的等价]]

Main Page

2014-08-11T11:52:28Z

IeshaEastman:

'''Intuitionistic type theory''' (also known as '''constructive type theory''', or '''Martin-Löf type theory''') is a [[type theory]] and an alternative [[Foundations of mathematics|foundation of mathematics]] based on the principles of [[mathematical constructivism]]. Intuitionistic type theory was introduced by [[Per Martin-Löf]], a [[Sweden|Swedish]] [[mathematician]] and [[philosopher]], in 1972. Martin-Löf has modified his proposal a few times; his 1971 [[impredicative]] formulation was inconsistent as demonstrated by [[Girard's paradox]]. Later formulations were [[Predicativity|predicative]]. He proposed both [[Intensional logic|intensional]] and [[extensionality|extensional]] variants of the theory.

Intuitionistic type theory is based on a certain analogy or isomorphism between [[proposition]]s and [[Type theory|types]]: a proposition is identified with the type of its proofs. This identification is usually called the [[Curry–Howard isomorphism]], which was originally formulated for [[intuitionistic logic]] and [[simply typed lambda calculus]]. Type theory extends this identification to [[predicate logic]] by introducing [[dependent types]], that is types which contain values.

Type theory internalizes the interpretation of [[intuitionistic logic]] proposed by [[Luitzen Egbertus Jan Brouwer|Brouwer]], [[Arend Heyting|Heyting]] and [[Andrey Kolmogorov|Kolmogorov]], the so-called [[BHK interpretation]]. The types in type theory play a similar role to sets in [[set theory]] but functions definable in type theory are always computable.

==Connectives of type theory==
In the context of type theory a [[Logical connective|connective]] is a way of constructing types, possibly using already given types.
The basic connectives of type theory are:

===Π-types===
{{main|Dependent type}}
Π-types, also called dependent product types, are analogous to the indexed [[Cartesian product|products]] of sets. As such, they generalize the normal [[function space]] to model functions whose result type may vary on their input. E.g. writing <math>\operatorname{Vec}({\mathbb R}, n)</math> for the type of [[tuple|''n''-tuples]] of [[real numbers]] and <math>\mathbb N</math> for the type of [[natural number]]s,

:<math>\prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)</math>

stands for the type of a function that, given a natural number ''n'', returns an ''n''-tuple of real numbers. The usual function space arises as a special case when the range type does not actually depend on the input, e.g., <math>\prod_{n \mathbin{:} {\mathbb N}} {\mathbb R}</math> is the type of functions from natural numbers to the real numbers, which is also written as <math>{\mathbb N} \to {\mathbb R}</math>.

Using the [[Curry–Howard isomorphism]] Π-types also serve to model [[material conditional|implication]] and [[universal quantification]]: e.g., a term inhabiting

<math>\prod_{m, n \mathbin{:} {\mathbb N}} (m + n = n + m)</math>

is a function which assigns to any pair of natural numbers a proof that addition is [[commutative]] for that pair and hence can be considered as a proof that addition is commutative for all natural numbers. (Here we have used the ''equality type'' (<math>x = y</math>) as explained below.)

===Σ-types===
Σ-types, also called dependent sum types, are analogous to the indexed [[disjoint union]]s of sets. As such, they generalize the usual [[Cartesian product]] to model pairs where the type of the second component depends on the first. For example, the type <math>\sum_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)</math> stands for the type of pairs of a natural number <math>n</math> and an <math>n</math>-tuple of real numbers, i.e., this type can be used to model sequences of arbitrary but finite length (usually called lists). The conventional [[Cartesian product]] type arises as a special case when the type of the second component doesn't actually depend on the first, e.g., <math>\sum_{n \mathbin{:} {\mathbb N}} {\mathbb R}</math> is the type of pairs of a [[natural number]] and a [[real number]], which is also written as <math>{\mathbb N} \times {\mathbb R}</math>.

Again, using the [[Curry–Howard isomorphism]], Σ-types also serve to model [[Logical conjunction|conjunction]] and [[existential quantification]].

===Finite types===
Of special importance are '''0''' or ⊥ (the [[empty type]]), '''1''' or ⊤ (the [[unit type]]) and '''2''' (the type of [[Boolean data type|Booleans]] or classical [[truth value]]s). Invoking the [[Curry–Howard isomorphism]] again, ⊥ stands for ''false'' and ⊤ for ''true''.

Using finite types we can define [[negation]] as

<math>\neg A \equiv A \to \bot.</math>

===Equality type===
Given <math>a, b \mathbin{:} A</math>, the expression <math>a = b</math> denotes the type of equality proofs for <math>a</math> is equal to <math>b</math>. That is, if <math>a = b</math> is inhabited, then <math>a</math> is said to be ''equal'' to <math>b</math>. There is only one (canonical) inhabitant of <math>a = a</math> and this is the proof of reflexivity

<math>\operatorname{refl} \mathbin{:} \prod_{a \mathbin{:} A} (a = a).</math>

Examination of the properties of the equality type, or rather, extending it to a notion of equivalence, lead to [[homotopy type theory]].

===Inductive types===
A prime example of an [[inductive type]] is the type of [[natural numbers]] <math>\mathbb{N}</math> which is generated by <math>0 \mathbin{:} {\mathbb N}</math> and <math>\operatorname{succ} \mathbin{:} {\mathbb N} \to {\mathbb N}</math>. An important application of the [[propositions as types principle]] is the identification of (dependent) [[primitive recursion]] and [[mathematical induction|induction]] by one elimination constant:

<math>{\operatorname{{\mathbb N}-elim}}\, \mathbin{:} P(0)\, \to \left(\prod_{n \mathbin{:} {\mathbb N}} P(n) \to P(\operatorname{succ}(n))\right) \to \prod_{n \mathbin{:} {\mathbb N}} P(n)</math>

for any given type <math>P(n)</math> indexed by <math>n \mathbin{:} {\mathbb N}</math>. In general inductive types can be defined in terms of W-types, the type of [[well-founded]] trees.

An important class of inductive types are inductive families like the type of vectors <math>\operatorname{Vec}(A, n)</math> mentioned above, which is inductively generated by the constructors <math>\operatorname{vnil} \mathbin{:} \operatorname{Vec}(A, 0)</math> and

<math>\operatorname{vcons}\, \mathbin{:}\, A \to \prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}(A, n) \to \operatorname{Vec}(A, \operatorname{succ}(n)).</math>

Applying the [[Curry–Howard isomorphism]] once more, inductive families correspond to inductively defined relations.

===Universes===
An example of a universe is <math>\mathcal{U}_0</math>, the universe of all small types, which contains names for all the types introduced so far. To every name <math>a \mathbin{:} \mathcal{U}_0</math> we associate a type <math>\operatorname{El}(a)</math>, its extension or meaning. It is standard to assume a [[Impredicativity|predicative]] hierarchy of universes: <math>\mathcal{U}_n</math> for every natural number <math>n \mathbin{:} {\mathbb N}</math>, where the universe <math>\mathcal{U}_{n+1}</math> contains a code for the previous universe, i.e., we have <math>u_n \mathbin{:} \mathcal{U}_{n+1}</math> with <math>\operatorname{El}(u_n) \equiv \mathcal{U}_n</math>. (A hierarchy with this property is called "cumulative".)

Stronger universe principles have been investigated, i.e., super universes and the Mahlo universe. In 1992 Huet and Coquand introduced the [[calculus of constructions]], a type theory with an impredicative universe, thus combining type theory with [[Jean-Yves Girard|Girard]]'s [[System F]]. This extension is not universally accepted by [[Intuitionist]]s since it allows impredicative, i.e., circular, constructions, which are often identified with classical reasoning.

==Formalisation of type theory==
This formalization is based on the discussion in Nordström, Petersson, and Smith.

The formal theory works with ''types'' and ''objects''.

A type is declared by:
* <math>A\ \mathsf{Type}</math>
An object exists and is in a type if:
* <math>a \mathbin{:} A </math>
Objects can be equal
* <math>a = b</math>
and types can be equal
* <math>A = B</math>
A type that depends on an object from another type is declared
* <math> (x \mathbin{:} A)B</math>
and removed by substitution
* <math> B[x / a] </math>, replacing the variable <math>x</math> with the object <math>a</math> in <math>B</math>.
An object that depends on an object from another type can be done two ways.
If the object is "abstracted", then it is written
* <math>[x]b</math>
and removed by substitution
* <math> b[x / a] </math>, replacing the variable <math>x</math> with the object <math>a</math> in <math>b</math>.
The object-depending-on-object can also be declared as a constant as part of a recursive type. An example of a recursive type is:
* <math>0 \mathbin{:} \mathbb{N} </math>
* <math>\operatorname{succ} \mathbin{:} \mathbb{N} \to \mathbb{N} </math>
Here, <math>\operatorname{succ}</math> is a constant object-depending-on-object. It is not associated with an abstraction.
Constants like <math>\operatorname{succ}</math> can be removed by defining equality. Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of <math>\operatorname{succ}</math>:
: <math>
\begin{align}
\operatorname{add} &\mathbin{:}\ (\mathbb{N} \times \mathbb{N}) \to \mathbb{N} \\
\operatorname{add}(0, b) &= b \\
\operatorname{add}(\operatorname{succ}(a), b) &= \operatorname{succ}(\operatorname{add}(a, b)))
\end{align}
</math>
<math>\operatorname{succ}</math> is manipulated as an opaque constant - it has no internal structure for substitution.

So, objects and types and these relations are used to express formulae in the theory. The following styles of judgements are used to create new objects, types and relations from existing ones:

{| class="wikitable"
|-
| <math>\Gamma\vdash \sigma\ \mathsf{Type}</math>
| ''σ'' is a well-formed type in the context Γ.
|-
| <math>\Gamma\vdash t \mathbin{:} \sigma</math>
| ''t'' is a well-formed term of type ''σ'' in context Γ.
|-
| <math>\Gamma\vdash \sigma \equiv \tau</math>
| ''σ'' and ''τ'' are equal types in context Γ.
|-
| <math>\Gamma\vdash t \equiv u \mathbin{:} \sigma</math>
| ''t'' and ''u'' are judgmentally equal terms of type ''σ'' in context Γ.
|-
| <math>\vdash \Gamma\ \mathsf{Context}</math>
| Γ is a well-formed context of typing assumptions.
|}

By convention, there is a type that represents all other types. It is called <math>\mathcal{U}</math> (or <math>\operatorname{Set}</math>). Since <math>\mathcal{U}</math> is a type, the member of it are objects. There is a dependent type <math>\operatorname{El}</math> that maps each object to its corresponding type. ''In most texts <math>\operatorname{El}</math> is never written.'' From the context of the statement, a reader can almost always tell whether <math>A</math> refers to a type, or whether it refers to the object in <math>\mathcal{U}</math> that corresponds to the type.

This is the complete foundation of the theory. Everything else is derived.

To implement logic, each proposition is given its own type. The objects in those types represent the different possible ways to prove the proposition. Obviously, if there is no proof for the proposition, then the type has no objects in it. Operators like "and" and "or" that work on propositions introduce new types and new objects. So <math>A \times B </math> is a type that depends on the type <math>A</math> and the type <math>B</math>. The objects in that dependent type are defined to exist for every pair of objects in <math>A</math> and <math>B</math>. Obviously, if <math>A</math> or <math>B</math> has no proof and is an empty type, then the new type representing <math> A \times B </math> is also empty.

This can be done for other types (booleans, natural numbers, etc.) and their operators.

==Categorical models of type theory==
Using the language of [[category theory]], [[R.A.G. Seely]] introduced the notion of a [[locally cartesian closed category]] (LCCC) as the basic model of type theory. This has been refined by Hofmann and Dybjer to ''Categories with Families'' or ''Categories with Attributes'' based on earlier work by Cartmell.

A category with families is a category ''C'' of contexts (in which the objects are contexts, and
the context morphisms are substitutions), together with a functor ''T'' : ''C''op → ''Fam(Set)''.

''Fam(Set)'' is the [[category of families]] of Sets, in which objects are pairs ''(A,B)'' of an "index set" ''A'' and a function ''B'': ''X'' → ''A'', and morphisms are pairs of functions ''f'' : ''A'' → ''A' '' and ''g'' : ''X'' → ''X' '', such that ''B' '' ° ''g'' = ''f'' ° ''B'' - in other words, ''f'' maps ''Ba'' to ''B'g(a)''.

The functor ''T'' assigns to a context ''G'' a set ''Ty(G)'' of types, and for each ''A'' : ''Ty(G)'', a set ''Tm(G,A)'' of terms.
The axioms for a functor require that these play harmoniously with substitution. Substitution is usually
written in the form ''Af'' or ''af'', where ''A'' is a type in ''Ty(G)'' and ''a'' is a term in ''Tm(G,A)'', and ''f'' is a substitution
from ''D'' to ''G''. Here ''Af'' : ''Ty(D)'' and ''af'' : ''Tm(D,Af)''.

The category ''C'' must contain a terminal object (the empty context), and a final object for a form
of product called comprehension, or context extension, in which the right element is a type in the context of the left element.
If ''G'' is a context, and ''A'' : ''Ty(G)'', then there should be an object ''(G,A)'' final among
contexts ''D'' with mappings ''p'' : ''D → ''G'', ''q'' : ''Tm(D,Ap)''.

A logical framework, such as Martin-Löf's takes the form of
closure conditions on the context dependent sets of types and terms: that there should be a type called
Set, and for each set a type, that the types should be closed under forms of dependent sum and
product, and so forth.

A theory such as that of predicative set theory expresses closure conditions on the types of sets and
their elements: that they should be closed under operations that reflect dependent sum and product,
and under various forms of inductive definition.

==Extensional versus intensional==
A fundamental distinction is [[Extensional definition|extensional]] vs [[Intensional definition|intensional]] type theory. In extensional type theory definitional (i.e., computational) equality is not distinguished from propositional equality, which requires proof. As a consequence type checking becomes [[undecidable problem|undecidable]] in extensional type theory because programs in the theory might not terminate. For example, such a theory allows one to give a type to [[Fixpoint combinator|Y-Combinator]], a detailed example of this can found in.<ref>Bengt Nordström; Kent Petersson; Jan M. Smith (1990). ''Programming in Martin-Löf's Type Theory''. Oxford University Press p.90</ref> However, this doesn't prevent extensional type theory from being a basis for a practical tool, for example, [[NuPRL]] is based on extensional type theory. From a practical standpoint there's no difference between a program which doesn't terminate and a program which takes a million years to terminate.

In contrast in intensional type theory [[type checking]] is [[Decision problem|decidable]], but the representation of standard mathematical concepts is somewhat more cumbersome, since extensional reasoning requires using [[setoid]]s or similar constructions. There are many common mathematical objects, which are hard to work with or can't be represented without this, for example, [[Integer|integer numbers]], [[rational number]]s, and [[real number]]s. Integers and rational numbers can be represented without setoids, but this representation isn't easy to work with. Real numbers can't be represented without this see.<ref>Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."</ref>

[[Homotopy type theory]] works on resolving this problem. It allows one to define [[higher inductive type]]s, which not only define first order constructors ([[value (computer science)|value]]s or [[point (geometry)|point]]s), but higher order constructors, i.e. equalities between elements ([[path (topology)|path]]s), equalities between equalities ([[homotopy|homotopies]]), ''ad infinitum''.

==Implementations of type theory==
Type theory has been the base of a number of proof assistants, such as [[NuPRL]], [[LEGO (programming)|LEGO]] and [[Coq]]. Recently, [[dependent types]] also featured in the design of [[programming languages]] such as [[ATS (programming language)|ATS]], [[Cayenne (programming language)|Cayenne]], [[Epigram (programming language)|Epigram]], [[Agda (theorem prover)|Agda]], and [[Idris (programming language)|Idris]].

==See also==
* [[Calculus of constructions]]
* [[Intuitionistic logic]]
* [[Per Martin-Löf]]
* [[Type theory]]
* [[Typed lambda calculus]]

==References==
* Per Martin-Löf (1984). ''[http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf Intuitionistic Type Theory]'' Bibliopolis. ISBN 88-7088-105-9.

==Further reading==
* Bengt Nordström; Kent Petersson; Jan M. Smith (1990). ''Programming in Martin-Löf's Type Theory''. Oxford University Press. The book is out of print, but a free version can be picked up from [http://www.cs.chalmers.se/Cs/Research/Logic/book/ here].
* Thompson, Simon (1991). ''[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]'' Addison-Wesley. ISBN 0-201-41667-0.
* Granström, Johan G. (2011). ''[http://www.springer.com/philosophy/book/978-94-007-1735-0 Treatise on Intuitionistic Type Theory]'' Springer. ISBN 978-94-007-1735-0.

==External links==
* [http://www.cs.chalmers.se/Cs/Research/Logic/Types/tutorials.html EU Types Project: Tutorials] - lecture notes and slides from the Types Summer School 2005
* [http://math.ucr.edu/home/baez/ncat.def.html n-Categories - Sketch of a Definition] - letter from John Baez and James Dolan to Ross Street, November 29, 1995

== References ==
{{Reflist}}

{{Non-classical logic}}

{{DEFAULTSORT:Intuitionistic Type Theory}}
[[Category:Dependently typed programming]]
[[Category:Constructivism (mathematics)]]
[[Category:Type theory]]
[[Category:Logic in computer science]]
[[Category:Intuitionism]]

Main Page

2014-08-11T07:51:24Z

IeshaEastman:

In [[mathematics]], an [[integral polytope]] has an associated '''Ehrhart polynomial''' that encodes the relationship between the volume of a polytope and the number of [[integer point]]s the polytope contains. The theory of Ehrhart polynomials can be seen as a higher-dimensional generalization of [[Pick's theorem]] in the [[Euclidean plane]].

These polynomials are named after [[Eugène Ehrhart]] who studied them in the 1960s.

==Definition==
Informally, if ''P'' is a [[polytope]], and ''tP'' is the polytope formed by expanding ''P'' by a factor of ''t'' in each dimension, then ''L''(''P'', ''t'') is the number of [[integer lattice]] points in ''tP''.

More formally, consider a [[lattice (group)|lattice]] ''L'' in [[Euclidean space]] '''R'''''n'' and a ''d''-[[dimension]]al polytope ''P'' in '''R'''''n'' with the property that all vertices of the polytope are points of the lattice. (A common example is ''L'' = '''Z'''''n'' and a polytope for which all vertices have [[integer]] coordinates.) For any positive integer ''t'', let ''tP'' be the ''t''-fold dilation of ''P'' (the polytope formed by multiplying each vertex coordinate, in a basis for the lattice, by a factor of ''t''), and let

:<math>L(P,t) = \#(tP \cap L)\,</math>

be the number of lattice points contained in the polytope ''tP''. Ehrhart showed in 1962 that ''L'' is a rational [[polynomial]] of degree ''d'' in ''t'', i.e. there exist [[rational number]]s ''a''0,...,''a''''d'' such that:

:<math>L(P, t) = a_d t^d + a_{d-1} t^{d-1} + ... + a_0</math>

for all positive integers ''t''.

The Ehrhart polynomial of the [[interior (topology)|interior]] of a closed convex polytope ''P'' can be computed as:
:<math> L(\text{int}(P), t) = (-1)^d L(P, -t),</math>

where ''d'' is the dimension of ''P''. This result is known as Ehrhart-Macdonald reciprocity.<ref>{{cite journal|last=Macdonald|first=Ian G|title=Polynomials Associated with Finite Cell-Complexes|journal=Journal of the London Mathematical Society|year=1971|volume=2|issue=1|pages=181–192|url=http://jlms.oxfordjournals.org/content/s2-4/1/181.full.pdf}}</ref>

[[File:Second dilate of a unit square.png|thumbnail|This is the second dilate, ''t = 2'', of a unit square. It has nine integer points.]]

==Examples of Ehrhart Polynomials==

Let ''P'' be a ''d''-dimensional [[unit cube|unit]] [[hypercube]] whose vertices are the integer lattice points all of whose coordinates are 0 or 1. In terms of inequalities,

: <math> P = \{x\in\mathbb{Q}^d : 0 \le x_i \le 1; 1 \le i \le d\} </math>.

Then the ''t''-fold dilation of ''P'' is a cube with side length ''t'', containing (''t'' + 1)''d'' integer points. That is, the Ehrhart polynomial of the hypercube is ''L''(''P'',''t'') = (''t'' + 1)''d''.<ref>{{harvtxt|De Loera|Rambau|Santos|2010}}</ref><ref>{{harvtxt|Mathar|2010}}</ref> Additionally, if we evaluate ''L(P, t)'' at negative integers, then

: <math>L(P, -t) = (-1)^d (t - 1)^d = (-1)^d L(\text{int}(P), t), </math>

as we would expect from Ehrhart-Macdonald reciprocity.

Many other [[figurate number]]s can be expressed as Ehrhart polynomials. For instance, the [[square pyramidal number]]s are given by the Ehrhart polynomials of a [[square pyramid]] with an integer unit square as its base and with height one; the Ehrhart polynomial in this case is (''t'' + 1)(''t'' + 2)(2''t'' + 3)/6.<ref>{{harvtxt|Beck|De Loera|Develin|Pfeifle|Stanley|2005}}.</ref>

==Ehrhart Quasi-Polynomials==

Let <math> P </math> be a rational polytope. In other words, suppose

: <math>P = \{ x\in\mathbb{Q}^d : Ax \le b\}</math>,

where <math>A\in\mathbb{R}^{k\times d}</math> and <math>b\in\mathbb{Z}^k</math>. (Equivalently, <math> P </math> is the [[convex hull]] of finitely many points in <math> \mathbb{Q}^d </math>.) Then define

: <math> L(P, t) = \#(\{x\in\mathbb{Z}^n : Ax \le tb\}). </math>

In this case, ''L(P, t)'' is a [[quasi-polynomial]] in ''t''. Just as with integral polytopes, Ehrhart-Macdonald reciprocity holds, that is,

: <math> L(\text{int}(P), t) = (-1)^n L(P, -t). </math>

==Examples of Ehrhart Quasi-Polynomials==

Let ''P'' be a polygon with vertices ''(0,0)'', ''(0,2)'', ''(1,1)'' and ''(0,3/2)''. The number of integer points in ''tP'' will be counted by the quasi-polynomial <ref name=MR2271992>{{cite book|title=Computing the Continuous Discretely|year=2007|publisher=Springer|location=New York|pages=46–47|author=Beck, Matthias|author2=Robins, Sinai}}</ref>

<math> L(P, t) = \frac{7}{4}t^2 + \frac{5}{2}t + \frac{7 + (-1)^t}{8}. </math>

==Interpretation of coefficients==
If ''P'' is [[closed set|closed]] (i.e. the boundary faces belong to ''P''), some of the coefficients of ''L''(''P'', ''t'') have an easy interpretation:
* the leading coefficient, ''a''''d'', is equal to the ''d''-dimensional [[volume]] of ''P'', divided by ''d''(''L'') (see [[lattice (group)|lattice]] for an explanation of the content or covolume ''d''(''L'') of a lattice);
* the second coefficient, ''a''''d''−1, can be computed as follows: the lattice ''L'' induces a lattice ''LF'' on any face ''F'' of ''P''; take the (''d''−1)-dimensional volume of ''F'', divide by 2''d''(''LF''), and add those numbers for all faces of ''P'';
* the constant coefficient ''a''0 is the [[Euler characteristic]] of ''P''. When ''P'' is a closed convex polytope, ''a''0 = 1.

==Ehrhart Series==

We can define a [[generating function]] for the Ehrhart polynomial of an integral n-dimensional polytope ''P'' as

<math> Ehr_P(z) = \sum_{t\ge 0} L(P, t)z^t </math>.

This series can be expressed as a [[rational function]]. Specifically, Ehrhart proved (1962) that there exist complex numbers <math> h_i^\ast </math>, <math> 0 \le j \le n </math>, such that the Ehrhart series of ''P'' is

<math> Ehr_P(z) = \frac{\sum_{j=0}^d h_j^\ast z^j}{(1 - z)^{n + 1}}, </math>

with <math> \sum_{j=0}^d h_j^\ast \neq 0 </math>. Additionally, Stanley's non-negativity theorem states that under the given hypotheses, <math> h_i^\ast </math> will be non-negative integers, for <math> 0 \le j \le n. </math>

Another result by Stanley shows that if ''P'' is a lattice polytope contained in ''Q'',
then ''h''*i(''P'')≤''h''*i(''Q'') for all ''i''.

The ''h''*-vector is in general not unimodal, but it is whenever it is symmetric, and the polytope has a
regular unimodal triangulation.<ref>{{cite journal|last1=Athanasiadis|first1=Christos A.|title=h∗-Vectors, Eulerian Polynomials and Stable Polytopes of Graphs|journal=Electronic Journal of Combinatorics|year=2004|volume=11|issue=2|url=http://www.combinatorics.org/ojs/index.php/eljc/article/view/v11i2r6}}</ref>

== Toric Variety ==
The case ''n'' = ''d'' = 2 and ''t'' = 1 of these statements yields [[Pick's theorem]]. Formulas for the other coefficients are much harder to get; [[Todd class]]es of [[toric variety|toric varieties]], the [[Riemann–Roch theorem]] as well as [[Fourier analysis]] have been used for this purpose.

If ''X'' is the [[toric variety]] corresponding to the normal fan of ''P'', then ''P'' defines an [[ample line bundle]] on ''X'', and the Ehrhart polynomial of ''P'' coincides with the [[Hilbert polynomial]] of this line bundle.

Ehrhart polynomials can be studied for their own sake. For instance, one could ask questions related to the roots of an Ehrhart polynomial.<ref>{{cite journal|last=Braun|first=Benjamin|author2=Develin, Mike|title=Ehrhart Polynomial Roots and Stanley's Non-Negativity Theorem|journal=American Mathematical Society|year=2008|volume=452|series=Contemporary Mathematics|pages=67–78|doi=10.1090/conm/452/08773}}</ref> Furthermore, some authors have pursued the question of how these polynomials could be classified.<ref>{{cite journal|last=Higashitani|first=Akihiro|title=Classification of Ehrhart Polynomials of Integral Simplices|journal=DMTCS Proceedings|year=2012|pages=587–594|url=http://www.math.nagoya-u.ac.jp/fpsac12/download/contributed/dmAR0152.pdf}}</ref>

==Generalizations==

It is possible to study the number of integer points in a polytope ''P'' if we dilate some facets of ''P'' but not others. In other words, one would like to know the number of integer points in semi-dilated polytopes. It turns out that such a counting function will be what is called a multivariate quasi-polynomial. An Ehrhart-type reciprocity theorem will also hold for such a counting function.<ref>{{cite journal|last=Beck|first=Matthias|title=Multidimensional Ehrhart reciprocity|journal=Journal of Combinatorial Theory|date=January 2002|volume=97|series=Series A|issue=1|pages=187–194|url=http://www.sciencedirect.com/science/article/pii/S0097316501932200|doi=10.1006/jcta.2001.3220}}</ref>

Counting the number of integer points in semi-dilations of polytopes has applications <ref>{{cite journal|last=Lisonek|first=Petr|title=Combinatorial Families Enumerated by Quasi-polynomials|journal=Journal of Combinatorial Theory|year=2007|volume=114|series=Series A|issue=4|pages=619–630|url=http://www.sciencedirect.com/science/article/pii/S0097316506001427|doi=10.1016/j.jcta.2006.06.013}}</ref> in enumerating the number of different dissections of regular polygons and the number of non-isomorphic unrestricted codes, a particular kind of code in the field of [[coding theory]].

== See also ==
* [[Quasi-polynomial]]

==Notes==
{{reflist}}

== References ==
*{{citation
| last1 = Beck | first1 = M.
| last2 = De Loera | first2 = J. A. | author2-link = Jesús A. De Loera
| last3 = Develin | first3 = M.
| last4 = Pfeifle | first4 = J.
| last5 = Stanley | first5 = R. P. | author5-link = Richard P. Stanley
| contribution = Coefficients and roots of Ehrhart polynomials
| location = Providence, RI
| mr = 2134759
| pages = 15–36
| publisher = Amer. Math. Soc.
| series = Contemp. Math.
| title = Integer points in polyhedra—geometry, number theory, algebra, optimization
| volume = 374
| year = 2005}}.
*{{citation
| last1 = Beck | first1 = Matthias
| last2 = Robins | first2 = Sinai
| mr = 2271992
| isbn = 978-0-387-29139-0
| location = New York
| publisher = Springer-Verlag
| series = Undergraduate Texts in Mathematics
| title = Computing the Continuous Discretely, Integer-point enumeration in polyhedra
| year = 2007}}.
*{{citation|title=Triangulations: Structures for Algorithms and Applications|volume=25|series=Algorithms and Computation in Mathematics|first1=Jesús A.|last1=De Loera|author1-link=Jesús A. De Loera|first2=Jörg|last2=Rambau|first3=Francisco|last3=Santos|publisher=Springer|year=2010|isbn=978-3-642-12970-4|contribution=9.3.3 Ehrhart polynomials and unimodular triangulations|page=475|url=http://books.google.com/books?id=SxY1Xrr12DwC&pg=PA475&lpg=PA475}}.
*{{citation
| last1 = Diaz | first1 = Ricardo
| last2 = Robins | first2 = Sinai
| journal = Electronic Research Announcements of the American Mathematical Society
| pages = 1–6
| title = The Ehrhart polynomial of a lattice ''n''-simplex
| url = http://www.ams.org/era/1996-02-01/S1079-6762-96-00001-7/home.html
| volume = 2
| year = 1996
| doi = 10.1090/S1079-6762-96-00001-7}}. Introduces the Fourier analysis approach and gives references to other related articles.
*{{citation
| last = Ehrhart | first = Eugène
| journal = [[Comptes rendus de l'Académie des sciences|C. R. Acad. Sci. Paris]]
| pages = 616–618
| title = Sur les polyèdres rationnels homothétiques à ''n'' dimensions
| volume = 254
| year = 1962}}. Definition and first properties.
*{{cite arXiv
|first1=Richard J.
|last1=Mathar
|eprint=1002.3844
|title=Point counts of Dk and some Ak and Ek integer lattices inside hypercubes
|year=2010
}}
*{{citation
| last = Mustaţă | first = Mircea
| contribution = Chapter 13: Ehrhart polynomials
| date = February 2005
| title = Lecture notes on toric varieties
| url = http://www.math.lsa.umich.edu/~mmustata/toric_var.html}}.

[[Category:Figurate numbers]]
[[Category:Polynomials]]
[[Category:Lattice points]]
[[Category:Polytopes]]

Main Page

2014-08-11T04:54:18Z

IeshaEastman:

In physics, an '''operator''' is a [[Function (mathematics)|function]] acting on the space of physical states. As a result
of its application on a physical state, another physical state is obtained, very often along with
some extra relevant information.

The simplest example of the utility of operators is the study of [[symmetry]]. Because of this, they
are a very useful tool in [[classical mechanics]]. In [[quantum mechanics]], on the other hand, they
are an intrinsic part of the formulation of the theory.

==Operators in classical mechanics==

In classical mechanics, the dynamics of a particle (or system of particles) are completely determined by the [[Lagrangian]] ''L''(''q, q̇, t'') or equivalently the [[Hamiltonian mechanics|Hamiltonian]] ''H''(''q, p, t''), a function of the [[generalized coordinates]] ''q'', generalized velocities ''q̇'' = d''q''/d''t'' and its [[conjugate momenta]]:

:<math>p = \frac{\partial L}{\partial \dot{q}}</math>

If either ''L'' or ''H'' are independent of a generalized coordinate ''q'', meaning the ''L'' and ''H'' so not change when ''q'' is changed, which in turn means the dynamics of the particle are still the same even when ''q'' changes, the corresponding momenta conjugate to those coordinates will be conserved (this is part of [[Noether's theorem]], and the invariance of motion with respect to the coordinate ''q'' is a [[symmetry (physics)|symmetry]]). Operators in classical mechanics are related to these symmetries.

More technically, when ''H'' is invariant under the action of a certain [[group (mathematics)|group]] of transformations ''G'':

:<math>S\in G, H(S(q,p))=H(q,p)</math>.

the elements of ''G'' are physical operators, which map physical states among themselves.

===Table of classical mechanics operators===

:{| class="wikitable"
|-
! Transformation
! Operator
! Position
! Momentum
|-
| [[Translational symmetry]]
| <math>X(\bold{a})</math>
| <math>\bold{r}\rightarrow \bold{r} + \bold{a}</math>
| <math>\bold{p}\rightarrow \bold{p}</math>
|-
| [[Time evolution|Time translations]]
| <math>U(t_0)</math>
| <math>\bold{r}(t)\rightarrow \bold{r}(t+t_0)</math>
| <math>\bold{p}(t)\rightarrow \bold{p}(t+t_0)</math>
|-
| [[Rotational invariance]]
| <math>R(\bold{\hat{n}},\theta)</math>
| <math>\bold{r}\rightarrow R(\bold{\hat{n}},\theta)\bold{r}</math>
| <math>\bold{p}\rightarrow R(\bold{\hat{n}},\theta)\bold{p}</math>
|-
| [[Galilean transformation]]s
| <math>G(\bold{v})</math>
| <math>\bold{r}\rightarrow \bold{r} + \bold{v}t</math>
| <math>\bold{p}\rightarrow \bold{p} + m\bold{v}</math>
|-
| [[Parity (physics)|Parity]]
| <math>P</math>
| <math>\bold{r}\rightarrow -\bold{r}</math>
| <math>\bold{p}\rightarrow -\bold{p}</math>
|-
| [[T-symmetry]]
| <math>T</math>
| <math>\bold{r}\rightarrow \bold{r}(-t)</math>
| <math>\bold{p}\rightarrow -\bold{p}(-t)</math>
|-
|}

where ''R''('''n̂''', θ) is the [[rotation matrix]] about an axis defined by the [[unit vector]] '''n̂''' and angle θ.

==Concept of generator==
If the transformation is infinitesimal, the operator action should be of the form

: <math> I + \epsilon A </math>

where <math>I</math> is the identity operator, <math>\epsilon</math> is a small parameter, and <math>A</math> will depend on the transformation at hand, and is called a generator of the group. Again, as a simple example, we will derive the generator of the space translations on 1D functions.

As it was stated, <math>T_a f(x)=f(x-a)</math>. If <math>a=\epsilon</math> is infinitesimal, then we may write

: <math>T_\epsilon f(x)=f(x-\epsilon)\approx f(x) - \epsilon f'(x).</math>

This formula may be rewritten as

: <math>T_\epsilon f(x) = (I-\epsilon D) f(x)</math>

where <math>D</math> is the generator of the translation group, which in this case happens to be the ''derivative'' operator. Thus, it is said that the generator of translations is the derivative.

==The exponential map==
The whole group may be recovered, under normal circumstances, from the generators, via the [[exponential map]]. In the case of the translations the idea works like this.

The translation for a finite value of <math>a</math> may be obtained by repeated application of the infinitesimal translation:

: <math>T_a f(x) = \lim_{N\to\infty} T_{a/N} \cdots T_{a/N} f(x)</math>

with the <math>\cdots</math> standing for the application <math>N</math> times. If <math>N</math> is large, each of the factors may be considered to be infinitesimal:

: <math>T_a f(x) = \lim_{N\to\infty} (I -(a/N) D)^N f(x).</math>

But this limit may be rewritten as an exponential:

: <math>T_a f(x)= \exp(-aD) f(x).</math>

To be convinced of the validity of this formal expression, we may expand the exponential in a power series:

: <math>T_a f(x) = \left( I - aD + {a^2D^2\over 2!} - {a^3D^3\over 3!} + \cdots \right) f(x).</math>

The right-hand side may be rewritten as

: <math>f(x) - a f'(x) + {a^2\over 2!} f''(x) - {a^3\over 3!} f'''(x) + \cdots</math>

which is just the Taylor expansion of <math>f(x-a)</math>, which was our original value for <math>T_a f(x)</math>.

The mathematical properties of physical operators are a topic of great importance in itself. For further information, see [[C*-algebra]] and [[Gelfand-Naimark theorem]].

==Operators in quantum mechanics==

The [[mathematical formulation of quantum mechanics]] (QM) is built upon the concept of an operator.

The wavefunction represents the [[probability amplitude]] of finding the system in that state. The terms "wavefunction" and "state" in QM context are usually used interchangeably.

Physical [[pure state]]s in quantum mechanics are represented as [[unit-norm vector]]s (probabilities are normalized to one) in a special [[complex number|complex]] [[vector space]]: a [[Hilbert space]]. [[Time evolution]] in this vector space is given by the application of the [[evolution operator]].

Any [[observable]], i.e., any quantity which can be measured in a physical experiment, should be associated with a [[self-adjoint]] [[linear operator]]. The operators must yield real [[eigenvalue]]s, since they are values which may come up as the result of the experiment. Mathematically this means the operators must be [[Hermitian matrix|Hermitian]].<ref>Molecular Quantum Mechanics Parts I and II: An Introduction to QUANTUM CHEMISRTY (Volume 1), P.W. Atkins, Oxford University Press, 1977, ISBN 0-19-855129-0</ref> The probability of each eigenvalue is related to the projection of the physical state on the subspace related to that eigenvalue. See below for mathematical details.

In the [[wave mechanics]] formulation of QM, the wavefunction varies with space and time, or equivalently momentum and time (see [[position and momentum space]] for details), so observables are [[differential operator]]s.

In the [[matrix mechanics]] formulation, the [[Norm (mathematics)|norm]] of the physical state should stay fixed, so the evolution operator should be [[unitary transformation|unitary]], and the operators can be represented as matrices. Any other symmetry, mapping a physical state into another, should keep this restriction.

===Wavefunction ===

{{Main|wavefunction}}

The wavefunction must be [[square-integrable]] on the Hilbert space (see [[Lp spaces]]) meaning:

:<math>\int_{-\infty}^\infty\int_{-\infty}^\infty\int_{-\infty}^\infty |\psi(\bold{r})|^2 {\rm d}^3\bold{r} = \int_{-\infty}^\infty\int_{-\infty}^\infty\int_{-\infty}^\infty \psi(\bold{r})^*\psi(\bold{r}){\rm d}^3\bold{r} < \infty </math>

and normalizable, so that:

:<math>\int_{-\infty}^\infty\int_{-\infty}^\infty\int_{-\infty}^\infty |\psi(\bold{r})|^2 {\rm d}^3\bold{r} = 1 </math>

Two cases of eigenstates (and eigenvalues) are:
*for '''discrete''' eigenstates <math> | \psi_i \rangle </math> forming a discrete basis, so the state is a [[sum]]
::<math>|\psi\rangle = \sum_i c_i|\phi_i\rangle</math>
:where ''ci'' are complex numbers such that |''ci''|2 = ''ci''*''ci'' = probability of measuring the state <math>|\phi_i\rangle</math>, and has the corresponding set of eigenvalues ''ai'' is also discrete - either [[finite]] or [[countably infinite]],
*for a '''continuum''' of eigenstates <math> | \psi \rangle </math> forming a continuous basis, so the state is an [[integral]]
::<math>|\psi\rangle = \int c(\phi){\rm d}\phi|\phi_i\rangle </math>
:where ''c''(φ) is a complex function such that |''c''(φ)|2 = ''c''(φ)*''c''(φ) = probability of measuring the state <math>|\phi\rangle</math>, there is an [[uncountably infinite]] set of eigenvalues ''a''.

===Linear operators in wave mechanics===

{{Main|Wave function|Bra-ket notation}}

Let ''ψ'' be the wavefunction for a quantum system, and <math>\hat{A}</math> be any [[linear operator]] for some observable ''A'' (such as position, momentum, energy, angular momentum etc.), then

:<math>\hat{A} \psi = a \psi ,</math>

where:

* ''a'' is the [[Eigenvalues and eigenvectors|eigenvalue]] of the operator, corresponding to the measured value of the observable, i.e. observable ''A'' has a measured value ''a''
*''ψ'' is the [[eigenfunction]] of <math>\hat{A}</math> if this relation holds.

If ''ψ'' is an eigenfunction of an operator, it means the eigenvalue can be found and so the observable can be measured, conversely if is not an eigenfunction then the eigenvalue can't be found and the observable can't be measured for that case.

In bra-ket notation the above can be written;

:<math>\begin{align} & \hat{A} \psi = \hat{A} \psi ( \mathbf{r} ) = \hat{A} \langle \mathbf{r} | \psi \rangle = \langle \mathbf{r} | \hat {A} | \psi \rangle \\
& a \psi = a \psi ( \mathbf{r} ) = a \langle \mathbf{r} | \psi \rangle = \langle \mathbf{r} | a | \psi \rangle \\
\end{align} </math>

in which case <math> | \psi \rangle </math> is an [[eigenvector]], or [[eigenket]].

Due to linearity, vectors can be defined in any number of dimensions, as each component of the vector acts on the function separately. One mathematical example is the [[del operator]], which is itself a vector (useful in momentum-related quantum operators, in the table below).

An operator in ''n''-dimensional space can be written:

:<math> \mathbf{\hat{A}} = \sum_{j=1}^n \mathbf{e}_\mathrm{j} \hat{A}_j </math>

where '''e'''''j'' are basis vectors corresponding to each component operator ''Aj''. Each component will yield a corresponding eigenvalue. Acting this on the wave function ''ψ'':

:<math> \mathbf{\hat{A}} \psi = \left ( \sum_{j=1}^n \mathbf{e}_\mathrm{j} \hat{A}_j \right ) \psi = \sum_{j=1}^n \left ( \mathbf{e}_\mathrm{j} \hat{A}_j \psi \right ) = \sum_{j=1}^n \left ( \mathbf{e}_\mathrm{j} a_j \psi \right ) </math>

in which

:<math> \hat{A}_j \psi = a_j \psi .</math>

In bra-ket notation:

:<math>\begin{align} & \mathbf{\hat{A}} \psi = \mathbf{\hat{A}} \psi ( \mathbf{r} ) = \mathbf{\hat{A}} \langle \mathbf{r} | \psi \rangle = \langle \mathbf{r} | \mathbf{\hat{A}} | \psi \rangle \\

& \left ( \sum_{j=1}^n \mathbf{e}_\mathrm{j} \hat{A}_j \right ) \psi = \left ( \sum_{j=1}^n \mathbf{e}_\mathrm{j} \hat{A}_j \right ) \psi ( \mathbf{r} ) = \left ( \sum_{j=1}^n \mathbf{e}_\mathrm{j} \hat{A}_j \right ) \langle \mathbf{r} | \psi \rangle = \left \langle \mathbf{r} \Bigg | \sum_{j=1}^n \mathbf{e}_\mathrm{j} \hat{A}_j \Bigg | \psi \right \rangle \\

\end{align} \,\!</math>

===Commutation of operators on ''Ψ''===

{{main|Commutator}}

If two observables ''A'' and ''B'' have linear operators <math> \hat{A} </math> and <math> \hat{B} </math>, the commutator is defined by,

:<math> \left [ \hat{A}, \hat{B} \right ] = \hat{A} \hat{B} - \hat{B} \hat{A} </math>

The commutator is itself a (composite) operator. Acting the commutator on ''ψ'' gives:

:<math> \left [ \hat{A}, \hat{B} \right ] \psi = \hat{A} \hat{B} \psi - \hat{B} \hat{A} \psi . </math>

If ''ψ'' is an eigenfunction with eigenvalues ''a'' and ''b'' for observables ''A'' and ''B'' respectively, and if the operators commute:

:<math> \left [ \hat{A}, \hat{B} \right ] \psi = 0, </math>

then the observables ''A'' and ''B'' can be measured at the same time with measurable eigenvalues ''a'' and ''b'' respectively. To illustrate this:

:<math> \begin{align}\left [ \hat{A}, \hat{B} \right ] \psi & = \hat{A} \hat{B} \psi - \hat{B} \hat{A} \psi \\
& = a(b \psi) - b(a \psi) \\
& = 0 .\\
\end{align} </math>

If the operators do not commute:

:<math> \left [ \hat{A}, \hat{B} \right ] \psi \neq 0, </math>

they can't be measured simultaneously to arbitrary precision, and there is an uncertainty relation between the observables, even if ''ψ'' is an eigenfunction. Notable pairs are position and momentum, and energy and time - [[Uncertainty principle|Hiesenberg's uncertainty relations]], and the angular momenta (spin, orbital and total) about any two orthogonal axes (such as ''Lx'' and ''Ly'', or ''sy'' and ''sz'' etc.).

===Expectation values of operators on ''Ψ''===

The [[expectation value]] (equivalently the average or mean value) is the average measurement of an observable, for particle in region ''R''. The expectation value <math>\langle \hat{A} \rangle </math> of the operator <math> \hat{A} </math> is calculated from<ref>Quantum Mechanics Demystified, D. McMahon, Mc Graw Hill (USA), 2006, ISBN(10) 0 07 145546 9</ref>:

:<math>\langle \hat{A} \rangle = \int_R \psi^{*}\left( \mathbf{r} \right ) \hat{A} \psi \left( \mathbf{r} \right ) \mathrm{d}^3\mathbf{r} = \langle \psi | \hat{A} | \psi \rangle .</math>

This can be generalized to any function ''F'' of an operator:

:<math> \langle F ( \hat{A} ) \rangle = \int_R \psi(\mathbf{r})^{*} \left [ F ( \hat{A} ) \psi(\mathbf{r}) \right ] \mathrm{d}^3 \mathbf{r} = \langle \psi | F ( \hat{A} ) | \psi \rangle , </math>

An example of ''F'' is the 2-fold action of ''A'' on ''ψ'', i.e. squaring an operator or doing it twice:

:<math>\begin{align}
& F(\hat{A}) = \hat{A}^2 \\
& \Rightarrow \langle \hat{A}^2 \rangle = \int_R \psi^{*} \left( \mathbf{r} \right ) \hat{A}^2 \psi \left( \mathbf{r} \right ) \mathrm{d}^3\mathbf{r} = \langle \psi \vert \hat{A}^2 \vert \psi \rangle \\
\end{align}\,\!</math>

===Hermitian operators===

{{Main|Self-adjoint operator}}

The definition of a [[Hermitian operator]] is <ref>Molecular Quantum Mechanics Parts I and II: An Introduction to QUANTUM CHEMISRTY (Volume 1), P.W. Atkins, Oxford University Press, 1977, ISBN 0-19-855129-0</ref>:

:<math>\hat{A} = \hat{A}^\dagger</math>

Following from this, in bra-ket notation:

:<math>\langle \phi_i | \hat{A} | \phi_j \rangle = \langle \phi_j | \hat{A} | \phi_i \rangle^*.</math>

Important properties of Hermitian operators include:

*real eigenvalues,
*eigenvectors with different eigenvalues are [[orthogonal]],
*eigenvectors can be chosen to be a complete [[orthonormal basis]],

===Operators in Matrix mechanics ===

An operator can be written in matrix form to map one basis vector to another. Since the operators and basis vectors are linear, the matrix is a [[linear transformation]] (aka transition matrix) between bases. Each basis element <math>\phi_j </math> can be connected to another<ref>Quantum Mechanics Demystified, D. McMahon, Mc Graw Hill (USA), 2006, ISBN(10) 0 07 145546 9</ref>, by the expression:

:<math>A_{ij} = \langle \phi_i | \hat{A} | \phi_j \rangle,</math>

which is a matrix element:

:<math>\hat{A} = \begin{pmatrix}
A_{11} & A_{12} & \cdots & A_{1n} \\
A_{21} & A_{22} & \cdots & A_{2n} \\
\vdots & \vdots & \ddots & \vdots \\
A_{n1} & A_{n2} & \cdots & A_{nn} \\
\end{pmatrix}
</math>

A further property of a Hermitian operator is that eigenfunctions corresponding to different eigenvalues are orthogonal.<ref>Molecular Quantum Mechanics Parts I and II: An Introduction to QUANTUM CHEMISRTY (Volume 1), P.W. Atkins, Oxford University Press, 1977, ISBN 0-19-855129-0</ref> In matrix form, operators allow real eigenvalues to be found, corresponding to measurements. Orthogonality allows a suitable basis set of vectors to represent the state of the quantum system. The eigenvalues of the operator are also evaluated in the same way as for the square matrix, by solving the [[characteristic polynomial]]:

:<math> \det\left ( \hat{A} - a \hat{I} \right ) = 0 ,</math>

where ''I'' is the ''n'' × ''n'' [[identity matrix]], as an operator it corresponds to the identity operator. For a discrete basis:

:<math> \hat{I} = \sum_i |\phi_i\rangle\langle\phi_i|</math>

while for a continuous basis:

:<math> \hat{I} = \int |\phi\rangle\langle\phi|d\phi</math>

=== Inverse of an operator ===

A non-singular operator <math>\hat{A}</math> has an inverse <math> \hat{A}^{-1} </math> defined by:

:<math> \hat{A}\hat{A}^{-1} = \hat{A}^{-1}\hat{A} = \hat{I} </math>

If an operator has no inverse, it is a singular operator. In a finite-dimensional space, the determinant of a non-singular operator is non-zero:

:<math> \det(\hat{A}) \neq 0</math>

and hence it is zero for a singular operator.

===Table of QM operators===

The operators used in quantum mechanics are collected in the table below (see for example,<ref>Molecular Quantum Mechanics Parts I and II: An Introduction to QUANTUM CHEMISRTY (Volume 1), P.W. Atkins, Oxford University Press, 1977, ISBN 0-19-855129-0</ref><ref>Quanta: A handbook of concepts, P.W. Atkins, Oxford University Press, 1974, ISBN 0-19-855493-1</ref>). The bold-face vectors with circumflexes are not [[unit vector]]s, they are 3-vector operators; all three spatial components taken together.

:{| class="wikitable"
|-valign="top"

! scope="col" width="200" | Operator (common name/s)
! scope="col" width="200" | Cartesian component
! scope="col" width="200" | General definition
! scope="col" width="100" | SI unit
! scope="col" width="100" | Dimension
|-valign="top"
! [[Position operator|Position]]
|<math>\begin{align} \hat{x} = x \\
\hat{y} = y \\
\hat{z} = z
\end{align}</math>
|<math> \mathbf{\hat{r}} = \mathbf{r} \,\!</math>
| m
| [L]
|-valign="top"
!rowspan="2"| [[Momentum operator|Momentum]]
|General

<math> \begin{align}
\hat{p}_x & = -i \hbar \frac{\partial }{\partial x} \\
\hat{p}_y & = -i \hbar \frac{\partial }{\partial y} \\
\hat{p}_z & = -i \hbar \frac{\partial }{\partial z}
\end{align}</math>
|General

<math> \mathbf{\hat{p}} = -i \hbar \nabla \,\!</math>
| J s m−1 = N s
| [M] [L] [T]−1
|-valign="top"
|Electromagnetic field

<math> \begin{align}
\hat{p}_x = -i \hbar \frac{\partial }{\partial x} - qA_x \\
\hat{p}_y = -i \hbar \frac{\partial }{\partial y} - qA_y \\
\hat{p}_z = -i \hbar \frac{\partial }{\partial z} - qA_z
\end{align}</math>
|Electromagnetic field (uses [[kinetic momentum]], '''A''' = vector potential)

<math> \begin{align}
\mathbf{\hat{p}} & = \bold{\hat{P}} - q\bold{A} \\
& = -i \hbar \nabla - q\bold{A} \\
\end{align}\,\!</math>
| J s m−1 = N s
| [M] [L] [T]−1
|-valign="top"
!rowspan="3"| [[Kinetic energy]]
| Translation
<math> \begin{align} \hat{T}_x & = -\frac{\hbar^2}{2m}\frac{\partial^2 }{\partial x^2} \\
\hat{T}_y & = -\frac{\hbar^2}{2m}\frac{\partial^2 }{\partial y^2} \\
\hat{T}_z & = -\frac{\hbar^2}{2m}\frac{\partial^2 }{\partial z^2} \\
\end{align} </math>
|
<math> \begin{align} \hat{T} & = \frac{\mathbf{\hat{p}}\cdot\mathbf{\hat{p}}}{2m} \\
& = \frac{(-i \hbar \nabla)\cdot(-i \hbar \nabla)}{2m} \\
& = \frac{-\hbar^2 }{2m}\nabla^2
\end{align}\,\!</math>
| J
| [M] [L]2 [T]−2
|-valign="top"
|Electromagnetic field

<math> \begin{align} \hat{T}_x & = \frac{1}{2m}\left(-i \hbar \frac{\partial }{\partial x } - q A_x \right)^2 \\
\hat{T}_y & = \frac{1}{2m}\left(-i \hbar \frac{\partial }{\partial y} - q A_y \right)^2 \\
\hat{T}_z & = \frac{1}{2m}\left(-i \hbar \frac{\partial }{\partial z} - q A_z \right)^2
\end{align}\,\!</math>
|Electromagnetic field ('''A''' = [[vector potential]])

<math> \begin{align} \hat{T} & = \frac{\mathbf{\hat{p}}\cdot\mathbf{\hat{p}}}{2m} \\
& = \frac{1}{2m}(-i \hbar \nabla - q\bold{A})\cdot(-i \hbar \nabla - q\bold{A}) \\
& = \frac{1}{2m}(-i \hbar \nabla - q\bold{A})^2
\end{align}\,\!</math>
| J
| [M] [L]2 [T]−2
|-valign="top"
|Rotation (''I'' = [[moment of inertia]])

<math> \begin{align}
\hat{T}_{xx} & = \frac{\hat{J}_x^2}{2I_{xx}} \\
\hat{T}_{yy} & = \frac{\hat{J}_y^2}{2I_{yy}} \\
\hat{T}_{zz} & = \frac{\hat{J}_y^2}{2I_{zz}} \\
\end{align}\,\!</math>
|Rotation

<math> \hat{T} = \frac{\bold{\hat{J}}\cdot\bold{\hat{J}}}{2I} \,\!</math>
| J
| [M] [L]2 [T]−2
|-valign="top"
! Potential energy
| N/A
|<math> \hat{V} = V\left ( \mathbf{r}, t \right ) = V \,\!</math>
| J
| [M] [L]2 [T]−2
|-valign="top"
! Total [[Energy operator|energy]]
|N/A
|Time-dependent potential: 
<math> \hat{E} = i \hbar \frac{\partial }{\partial t} \,\!</math>

Time-independent: 
<math> \hat{E} = E \,\!</math>
| J
| [M] [L]2 [T]−2
|-valign="top"
! [[Hamiltonian operator|Hamiltonian]]
|
|<math> \begin{align} \hat{H} & = \hat{T} + \hat{V} \\
& = \frac{\bold{\hat{p}}\cdot\bold{\hat{p}}}{2m} + V \\
& = \frac{\hat{p}^2}{2m} + V \\
\end{align} \,\!</math>
| J
| [M] [L]2 [T]−2
|-valign="top"
! [[Angular momentum operator]]
|<math>\begin{align}
\hat{L}_x & = -i\hbar \left(y {\partial\over \partial z} - z {\partial\over \partial y}\right)\\
\hat{L}_y & = -i\hbar \left(z {\partial\over \partial x} - x {\partial\over \partial z}\right)\\
\hat{L}_z & = -i\hbar \left(x {\partial\over \partial y} - y {\partial\over \partial x}\right)
\end{align}</math>
||<math>\mathbf{\hat{L}} = -i\hbar \mathbf{r} \times \nabla </math>
|| J s = N s m−1
|| [M] [L]2 [T]−1
|-valign="top"
! [[Spin (physics)|Spin]] angular momentum
|<math>\begin{align}
\hat{S}_x & = {\hbar \over 2} \sigma_x \\
\hat{S}_y = {\hbar \over 2} \sigma_y \\
\hat{S}_z = {\hbar \over 2} \sigma_z
\end{align}</math>

where

<math>
\sigma_x = \begin{pmatrix}
0&1\\
1&0
\end{pmatrix}
</math>

<math>
\sigma_y = \begin{pmatrix}
0&-i\\
i&0
\end{pmatrix}
</math>

<math>
\sigma_z = \begin{pmatrix}
1&0\\
0&-1
\end{pmatrix}
</math>

are the [[pauli matrices]] for [[spin-½]] particles.
|<math>\mathbf{\hat{S}} = {\hbar \over 2} \boldsymbol{\sigma} \,\!</math>

where '''σ''' is the vector whose components are the pauli matrices.
| J s = N s m−1
| [M] [L]2 [T]−1
|-valign="top"

! Total angular momentum
||<math>\begin{align}
\hat{J}_x & = \hat{L}_x + \hat{S}_x\\
\hat{J}_y & = \hat{L}_y + \hat{S}_y\\
\hat{J}_z & = \hat{L}_z + \hat{S}_z
\end{align}</math>
||<math>\begin{align}
\mathbf{\hat{J}} & = \mathbf{\hat{L}}+\mathbf{\hat{S}} \\
& = -i\hbar \bold{r}\times\nabla + \frac{\hbar}{2}\boldsymbol{\sigma}
\end{align}</math>
|| C m
|| [I] [T] [L]
|-valign="top"
! [[Transition dipole moment]] (electric)
||<math>\begin{align}
\hat{d}_x & = q\hat{x}\\
\hat{d}_y & = q\hat{y}\\
\hat{d}_z & = q\hat{z}
\end{align}</math>
||<math>\mathbf{\hat{d}} = q \mathbf{\hat{r}} </math>
|| C m
|| [I] [T] [L]
|-valign="top"
|}

===Examples of applying quantum operators===

The procedure for extracting information from a wave function is as follows. Consider the momentum ''p'' of a particle as an example. The momentum operator in one dimension is:

:<math>\hat{p} = -i\hbar\frac{\partial }{\partial x}</math>

Letting this act on ''ψ'' we obtain:

:<math>\hat{p} \psi = -i\hbar\frac{\partial }{\partial x} \psi ,</math>

if ''ψ'' is an eigenfunction of <math>\hat{p}</math>, then the momentum eigenvalue ''p'' is the value of the particle's momentum, found by:

:<math> -i\hbar\frac{\partial }{\partial x} \psi = p \psi.</math>

For three dimensions the momentum operator uses the [[nabla symbol|nabla]] operator to become:

:<math>\mathbf{\hat{p}} = -i\hbar\nabla .</math>

In Cartesian coordinates (using the standard Cartesian basis vectors '''e'''x, '''e'''y, '''e'''z) this can be written;

:<math>\mathbf{e}_\mathrm{x}\hat{p}_x + \mathbf{e}_\mathrm{y}\hat{p}_y + \mathbf{e}_\mathrm{z}\hat{p}_z = -i\hbar\left ( \mathbf{e}_\mathrm{x} \frac{\partial }{\partial x} + \mathbf{e}_\mathrm{y} \frac{\partial }{\partial y} + \mathbf{e}_\mathrm{z} \frac{\partial }{\partial z} \right ),</math>

that is:

:<math> \hat{p}_x = -i\hbar \frac{\partial}{\partial x}, \quad \hat{p}_y = -i\hbar \frac{\partial}{\partial y} , \quad \hat{p}_z = -i\hbar \frac{\partial}{\partial z} \,\!</math>

The process of finding eigenvalues is the same. Since this is a vector and operator equation, if ''ψ'' is an eigenfunction, then each component of the momentum operator will have an eigenvalue corresponding to that component of momentum. Acting <math> \mathbf{\hat{p}} </math> on ''ψ'' obtains:

:<math> \begin{align}
\hat{p}_x \psi & = -i\hbar \frac{\partial}{\partial x} \psi = p_x \psi \\
\hat{p}_y \psi & = -i\hbar \frac{\partial}{\partial y} \psi = p_y \psi \\
\hat{p}_z \psi & = -i\hbar \frac{\partial}{\partial z} \psi = p_z \psi \\
\end{align} \,\!</math>

==See also==
<div class="references-small" style="-moz-column-count:3; column-count:3;">
*[[Bounded linear operator]]
*[[Representation theory]]
</div>

==References==

{{reflist}}

{{Physics operator}}

{{DEFAULTSORT:Operator (Physics)}}
[[Category:Operator theory]]
[[Category:Theoretical physics]]

[[ar:مؤثر (فيزياء)]]
[[de:Operator (Mathematik)#Operatoren der Physik]]
[[fr:Opérateur (physique)]]
[[lt:Operatoriai kvantinėje mechanikoje]]
[[pt:Operador (física)]]
[[ru:Оператор (физика)]]
[[zh:算符 (物理學)]]