Description: Define the bra of a
vector used by Dirac notation. Based on definition
of bra in [Prugovecki] p. 186 (p.
180 in 1971 edition). In Dirac
bra-ket notation, 〈𝐴 ∣ 𝐵〉 is a complex number equal to
the inner
product (𝐵 ·ih 𝐴). But physicists like
to talk about the
individual components 〈𝐴 ∣ and ∣
𝐵〉, called bra
and ket
respectively. In order for their properties to make sense formally, we
define the ket ∣ 𝐵〉 as the vector 𝐵 itself,
and the bra
〈𝐴 ∣ as a functional from ℋ to ℂ. We represent the
Dirac notation 〈𝐴 ∣ 𝐵〉 by ((bra‘𝐴)‘𝐵); see
braval 30314. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 29454) but is also required in order for the
associative law
kbass2 30487 to work.
Our definition of bra and the associated outer product df-kb 30221 differs
from, but is equivalent to, a common approach in the literature that
makes use of mappings to a dual space. Our approach eliminates the need
to have a parallel development of this dual space and instead keeps
everything in Hilbert space.
For an extensive discussion about how our notation maps to the
bra-ket
notation in physics textbooks, see mmnotes.txt 30221, under the 17-May-2006
entry. (Contributed by NM, 15-May-2006.)
(New usage is discouraged.) |