The Hermitian inner product of a compatible pair #
A symplectic form ω compatible with an almost complex structure J packages the real metric
g(v, w) = ω(v, J w) and the symplectic form into a single complex Hermitian inner product
h(v, w) = g(v, w) + i ω(v, w) = ω(v, J w) + i ω(v, w)
on the complex vector space (V, J) (the complex structure of ComplexModule.lean, where
multiplication by i is J). This is the classical statement that a compatible triple
(ω, J, g) is the same data as a Hermitian structure (McDuff--Salamon, J-holomorphic Curves and
Symplectic Topology, Section 2.1): the real and imaginary parts of h recover the
metric and the symplectic form, h is conjugate-symmetric, it is complex linear in the second
argument over the J-induced complex structure, and it is positive definite.
This is the complex companion of TauCeti.SymplecticForm.Compatible.innerProductCore, which
records the real metric g of the same pair as an InnerProductSpace.Core ℝ V. Here the complex
form is built once, as SymplecticForm.complexAssociatedForm, and the Hermitian-structure facts
are proved under
the weakest hypothesis each one needs: conjugate symmetry and conjugate-linearity in the first
argument need only ω.Invariant J, while positive definiteness needs only ω.Tames J.
Compatibility (Invariant plus Tames) is what assembles all of them into the capstone
Compatible.hermitianCore, exhibiting h as an InnerProductSpace.Core ℂ V for the complex
structure J.complexModule.
Main declarations #
TauCeti.SymplecticForm.complexAssociatedForm: the complex formh(v, w) = ω(v, J w) + i ω(v, w).TauCeti.SymplecticForm.complexAssociatedForm_re/complexAssociatedForm_im: the real and imaginary parts ofhare the metricg(v, w) = ω(v, J w)and the symplectic formω(v, w).TauCeti.SymplecticForm.Invariant.complexAssociatedForm_conj_symm:his conjugate-symmetric,conj (h(w, v)) = h(v, w), needing onlyJ-invariance.TauCeti.SymplecticForm.complexAssociatedForm_smul_right:his complex linear in its second argument,h(v, z • w) = z · h(v, w), for the complex structureJ.complexModule(no compatibility needed).TauCeti.SymplecticForm.complexAssociatedForm_self:h(v, v) = ω(v, J v), withTauCeti.SymplecticForm.Tames.complexAssociatedForm_self_re_posadding positivity on nonzero vectors.TauCeti.SymplecticForm.Compatible.hermitianCore: the Hermitian inner product of a compatible pair as anInnerProductSpace.Core ℂ V.
The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology,
Section 2.1: a compatible pair (ω, J) gives the Hermitian form ⟨v, w⟩ = g(v, w) + i ω(v, w).
The complex form associated to a pair (ω, J): h(v, w) = ω(v, J w) + i ω(v, w).
Its real part is the metric ω(·, J ·) and its imaginary part is the symplectic form ω. The
bare definition needs no hypotheses on (ω, J); the Hermitian-structure facts are each proved
under the weakest hypothesis they need: complex linearity in the second argument from J² = -1
alone (complexAssociatedForm_smul_right), conjugate symmetry and conjugate-linearity in the first
argument from ω.Invariant J (Invariant.complexAssociatedForm_conj_symm,
Invariant.complexAssociatedForm_smul_left), and positive definiteness from ω.Tames J
(Tames.complexAssociatedForm_self_re_pos). Full compatibility is needed only to assemble
Compatible.hermitianCore.
Equations
- ω.complexAssociatedForm J v w = ↑((fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap w)) + Complex.I * ↑((fun (v w : V) => (ω.toBilinForm v) w) v w)
Instances For
The real part of the complex associated form is the metric g(v, w) = ω(v, J w).
The imaginary part of the complex associated form is the symplectic form ω(v, w).
The complex associated form is additive in its first argument.
The complex associated form is additive in its second argument.
The complex associated form is complex linear in its second argument over the complex structure
J.complexModule: h(v, z • w) = z · h(v, w). This is one of the defining properties of a
Hermitian inner product on the complex vector space (V, J), and needs only J² = -1, not
compatibility.
The diagonal of the complex associated form is real and equals the metric diagonal
ω(v, J v).
The diagonal of the Hermitian form is positive on nonzero vectors. Only tameness is needed.
The real part of the diagonal of the Hermitian form is nonnegative, in the RCLike.re form
the inner-product-space core expects. Only tameness is needed.
The diagonal of the Hermitian form vanishes exactly at zero. Only tameness is needed.
The Hermitian form is conjugate-symmetric: conj (h(w, v)) = h(v, w). Only J-invariance is
needed.
The Hermitian form is conjugate linear in its first argument over the complex structure
J.complexModule: h(z • v, w) = conj z · h(v, w). Only J-invariance is needed.
The diagonal of the Hermitian form is positive on nonzero vectors.
The real part of the diagonal of the Hermitian form is nonnegative, in the RCLike.re form
the inner-product-space core expects.
The diagonal of the Hermitian form vanishes exactly at zero.
The Hermitian form is conjugate-symmetric: conj (h(w, v)) = h(v, w).
The Hermitian form is conjugate linear in its first argument over the complex structure
J.complexModule: h(z • v, w) = conj z · h(v, w).
The Hermitian inner product of a compatible pair, packaged as an InnerProductSpace.Core ℂ V
for the complex structure J.complexModule.
The inner product is ⟨v, w⟩ = ω(v, J w) + i ω(v, w), conjugate linear in the first argument and
complex linear in the second, with ⟨v, v⟩ = ω(v, J v) > 0 for v ≠ 0.
Equations
- h.hermitianCore = { inner := ω.complexAssociatedForm J, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }
Instances For
The inner product from hermitianCore is the Hermitian form ω(v, J w) + i ω(v, w).