Restricting a symplectic form to a subspace

A symplectic form restricts to a subspace on which it stays nondegenerate. A subspace L complementary to its symplectic complement L^ω is automatically of that kind, as is L^ω, and then ω is the product of the two restrictions under the linear equivalence supplied by the splitting. A pair of vectors with nonzero symplectic pairing spans such a subspace.

A compatible pair (ω, J) restricts to a compatible pair on a J-invariant subspace, using TauCeti.AlmostComplexStructure.restrict.

Main declarations

• TauCeti.SymplecticForm.restrict: the restriction of ω to a subspace on which it stays nondegenerate, again a symplectic form.
• TauCeti.SymplecticForm.nondegenerate_restrict_orthogonal_of_isCompl: the splitting V = L ⊕ L^ω already forces ω to restrict nondegenerately to L^ω (for L itself this is Mathlib's LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal).
• TauCeti.SymplecticForm.disjoint_span_pair_orthogonal: a pair with nonzero symplectic pairing spans a subspace disjoint from its symplectic complement.
• TauCeti.SymplecticForm.isSymplectomorphism_prodEquivOfIsCompl: the equivalence associated to V = L ⊕ L^ω is a symplectomorphism from the product of the restricted forms to ω.
• TauCeti.SymplecticForm.Compatible.restrict: compatibility passes to these restrictions.

def TauCeti.SymplecticForm.restrict {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) (h : (ω.toBilinForm.restrict L).Nondegenerate) : SymplecticForm ↥L

The restriction of a symplectic form to a subspace on which it remains nondegenerate.

Nondegeneracy is genuinely a hypothesis: ω restricts to 0 on any isotropic subspace.

theorem TauCeti.SymplecticForm.restrict_toBilinForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) (h : (ω.toBilinForm.restrict L).Nondegenerate) : (ω.restrict L h).toBilinForm = ω.toBilinForm.restrict L

@[simp]

theorem TauCeti.SymplecticForm.restrict_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) (h : (ω.toBilinForm.restrict L).Nondegenerate) (v w : ↥L) : (fun (v w : ↥L) => ((ω.restrict L h).toBilinForm v) w) v w = (fun (v w : V) => (ω.toBilinForm v) w) ↑v ↑w

theorem TauCeti.SymplecticForm.nondegenerate_restrict_orthogonal_of_isCompl {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) {L : Submodule ℝ V} (hcompl : IsCompl L (ω.orthogonal L)) : (ω.toBilinForm.restrict (ω.orthogonal L)).Nondegenerate

The symplectic complement of a subspace complementary to it also carries a nondegenerate restriction of ω: a vector of L^ω orthogonal to L^ω is orthogonal to L as well, hence to L ⊔ L^ω = V, and nondegeneracy of ω makes it zero. Unlike LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal this needs no finite-dimensionality.

theorem TauCeti.SymplecticForm.isSymplectomorphism_prodEquivOfIsCompl {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) {L : Submodule ℝ V} (hcompl : IsCompl L (ω.orthogonal L)) : ((ω.restrict L ⋯).prod (ω.restrict (ω.orthogonal L) ⋯)).IsSymplectomorphism ω (L.prodEquivOfIsCompl (ω.orthogonal L) hcompl)

Along the splitting V = L ⊕ L^ω, the symplectic form is the product of its restrictions to the two summands: the cross terms vanish by the very definition of the symplectic complement.

theorem TauCeti.SymplecticForm.disjoint_span_pair_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) {x y : V} (h : (fun (v w : V) => (ω.toBilinForm v) w) x y ≠ 0) : Disjoint (Submodule.span ℝ {x, y}) (ω.orthogonal (Submodule.span ℝ {x, y}))

A pair with nonzero symplectic pairing spans a symplectic plane: it is disjoint from its own symplectic complement, so ω restricts to it nondegenerately.

theorem TauCeti.SymplecticForm.Compatible.restrict {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hJ : ω.Compatible J) (L : Submodule ℝ V) (h : (ω.toBilinForm.restrict L).Nondegenerate) (hL : ∀ x ∈ L, J.toLinearMap x ∈ L) : (ω.restrict L h).Compatible (J.restrict L hL)

A compatible pair (ω, J) restricts to a compatible pair on a J-invariant subspace on which ω stays nondegenerate.