| 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 31964. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 31104) but is also required in order for the
associative law
kbass2 32137 to work.
Our definition of bra and the associated outer product df-kb 31871 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 31871, under the 17-May-2006
entry. (Contributed by NM, 15-May-2006.)
(New usage is discouraged.) |
