Transporting symplectic forms along linear equivalences

A real-linear isomorphism e : V ≃ₗ[ℝ] W carries a symplectic form ω on V to one on W by pushing the arguments back along e.symm: (ω.transport e)(v, w) = ω(e.symm v, e.symm w). This is the symplectic companion of TauCeti.AlmostComplexStructure.transport (in TauCeti.Geometry.Symplectic.Transport): together they make e simultaneously a symplectomorphism and a complex-linear isomorphism, so every compatibility relation between ω and an almost complex structure J is preserved when both are transported along e.

This is the pointwise linear algebra that the smooth layer of the analytic Heegaard Floer roadmap needs before stating bundle-level naturality: a symplectic form on a vector bundle is given fiberwise, and a change of trivialization acts on each fiber by exactly this transport. Stating the compatibility transport now keeps the invariance statements naturality-ready, as the roadmap asks. The underlying form transport reuses Mathlib's LinearMap.BilinForm.congr and LinearMap.BilinForm.Nondegenerate.congr.

Main declarations

• TauCeti.SymplecticForm.transport: the symplectic form ω.transport e on W obtained by transporting ω along e : V ≃ₗ[ℝ] W.
• TauCeti.SymplecticForm.transport_refl / transport_trans / transport_symm_transport / transport_transport_symm: functoriality of transport in the linear equivalence.
• TauCeti.SymplecticForm.transport_apply_apply: e is a symplectomorphism onto the transported form, (ω.transport e)(e v, e w) = ω(v, w).
• TauCeti.SymplecticForm.IsSymplectomorphism: a linear equivalence e with ω₂(e v, e w) = ω₁(v, w), together with its pointwise and transport characterizations.
• TauCeti.SymplecticForm.Invariant.transport, Tames.transport, Compatible.transport: invariance, tameness, and compatibility of a pair (ω, J) transport along e to the pair (ω.transport e, J.transport e).

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1, where a symplectomorphism carries a compatible triple to a compatible triple.

noncomputable def TauCeti.SymplecticForm.transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (e : V ≃ₗ[ℝ] W) : SymplecticForm W

Transport a symplectic form along a real-linear equivalence e : V ≃ₗ[ℝ] W by pushing the arguments back along e.symm.

The underlying bilinear form is LinearMap.BilinForm.congr e applied to ω, equivalently (v, w) ↦ ω(e.symm v, e.symm w); it stays alternating and nondegenerate because e.symm is a linear bijection.

Equations

• ω.transport e = { toBilinForm := (LinearMap.BilinForm.congr e) ω.toBilinForm, isAlt := ⋯, nondegenerate := ⋯ }

@[simp]

theorem TauCeti.SymplecticForm.transport_toBilinForm {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (e : V ≃ₗ[ℝ] W) : (ω.transport e).toBilinForm = (LinearMap.BilinForm.congr e) ω.toBilinForm

@[simp]

theorem TauCeti.SymplecticForm.transport_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (e : V ≃ₗ[ℝ] W) (v w : W) : (fun (v w : W) => ((ω.transport e).toBilinForm v) w) v w = (fun (v w : V) => (ω.toBilinForm v) w) (e.symm v) (e.symm w)

@[simp]

theorem TauCeti.SymplecticForm.transport_refl {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) : ω.transport (LinearEquiv.refl ℝ V) = ω

Transporting along the identity equivalence does nothing.

@[simp]

theorem TauCeti.SymplecticForm.transport_trans {V : Type u_1} {W : Type u_2} {X : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup X] [Module ℝ X] (ω : SymplecticForm V) (e₁ : V ≃ₗ[ℝ] W) (e₂ : W ≃ₗ[ℝ] X) : (ω.transport e₁).transport e₂ = ω.transport (e₁ ≪≫ₗ e₂)

Transport is functorial: transporting along e₁ then e₂ is transporting along their composite.

theorem TauCeti.SymplecticForm.transport_symm_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (e : V ≃ₗ[ℝ] W) : (ω.transport e).transport e.symm = ω

Transporting forward along e and back along e.symm returns the original form.

theorem TauCeti.SymplecticForm.transport_transport_symm {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm W) (e : V ≃ₗ[ℝ] W) : (ω.transport e.symm).transport e = ω

Transporting back along e.symm and forward along e returns the original form.

theorem TauCeti.SymplecticForm.transport_apply_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (e : V ≃ₗ[ℝ] W) (v w : V) : (fun (v w : W) => ((ω.transport e).toBilinForm v) w) (e v) (e w) = (fun (v w : V) => (ω.toBilinForm v) w) v w

e is a symplectomorphism onto the transported form: evaluating ω.transport e on images under e recovers ω.

def TauCeti.SymplecticForm.IsSymplectomorphism {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (e : V ≃ₗ[ℝ] W) : Prop

A real-linear equivalence e : V ≃ₗ[ℝ] W is a symplectomorphism from (V, ω₁) to (W, ω₂) when it intertwines the two symplectic forms, ω₂(e v, e w) = ω₁(v, w).

The body is @[no_expose]: downstream code uses this predicate through isSymplectomorphism_iff, IsSymplectomorphism.apply, and isSymplectomorphism_iff_transport_eq rather than by unfolding.

Equations

• ω₁.IsSymplectomorphism ω₂ e = ∀ (v w : V), (fun (v w : W) => (ω₂.toBilinForm v) w) (e v) (e w) = (fun (v w : V) => (ω₁.toBilinForm v) w) v w

theorem TauCeti.SymplecticForm.isSymplectomorphism_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {e : V ≃ₗ[ℝ] W} : ω₁.IsSymplectomorphism ω₂ e ↔ ∀ (v w : V), (fun (v w : W) => (ω₂.toBilinForm v) w) (e v) (e w) = (fun (v w : V) => (ω₁.toBilinForm v) w) v w

A linear equivalence is a symplectomorphism exactly when it preserves the symplectic forms pointwise.

theorem TauCeti.SymplecticForm.IsSymplectomorphism.apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {e : V ≃ₗ[ℝ] W} (h : ω₁.IsSymplectomorphism ω₂ e) (v w : V) : (fun (v w : W) => (ω₂.toBilinForm v) w) (e v) (e w) = (fun (v w : V) => (ω₁.toBilinForm v) w) v w

Apply a symplectomorphism hypothesis to two vectors.

theorem TauCeti.SymplecticForm.isSymplectomorphism_iff_transport_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {e : V ≃ₗ[ℝ] W} : ω₁.IsSymplectomorphism ω₂ e ↔ ω₁.transport e = ω₂

A linear equivalence is a symplectomorphism exactly when ω₂ is the transport of ω₁ along that equivalence.

@[simp]

theorem TauCeti.SymplecticForm.IsSymplectomorphism.refl {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) : ω.IsSymplectomorphism ω (LinearEquiv.refl ℝ V)

The identity equivalence is a symplectomorphism.

theorem TauCeti.SymplecticForm.IsSymplectomorphism.symm {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {e : V ≃ₗ[ℝ] W} (h : ω₁.IsSymplectomorphism ω₂ e) : ω₂.IsSymplectomorphism ω₁ e.symm

The inverse of a symplectomorphism is a symplectomorphism.

theorem TauCeti.SymplecticForm.IsSymplectomorphism.trans {V : Type u_1} {W : Type u_2} {X : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup X] [Module ℝ X] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {ω₃ : SymplecticForm X} {e : V ≃ₗ[ℝ] W} {f : W ≃ₗ[ℝ] X} (h₁ : ω₁.IsSymplectomorphism ω₂ e) (h₂ : ω₂.IsSymplectomorphism ω₃ f) : ω₁.IsSymplectomorphism ω₃ (e ≪≫ₗ f)

Symplectomorphisms compose.

@[simp]

theorem TauCeti.SymplecticForm.invariant_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : (ω.transport e).Invariant (J.transport e) ↔ ω.Invariant J

Transport by a linear equivalence preserves and reflects J-invariance.

theorem TauCeti.SymplecticForm.Invariant.transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (e : V ≃ₗ[ℝ] W) : (ω.transport e).Invariant (J.transport e)

J-invariance transports along a linear equivalence: if ω is J-invariant, then ω.transport e is invariant under the transported almost complex structure J.transport e.

@[simp]

theorem TauCeti.SymplecticForm.tames_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : (ω.transport e).Tames (J.transport e) ↔ ω.Tames J

Transport by a linear equivalence preserves and reflects tameness.

theorem TauCeti.SymplecticForm.Tames.transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (htames : ω.Tames J) (e : V ≃ₗ[ℝ] W) : (ω.transport e).Tames (J.transport e)

Taming transports along a linear equivalence: if ω tames J, then ω.transport e tames the transported almost complex structure J.transport e.

@[simp]

theorem TauCeti.SymplecticForm.compatible_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : (ω.transport e).Compatible (J.transport e) ↔ ω.Compatible J

Transport by a linear equivalence preserves and reflects compatibility.

theorem TauCeti.SymplecticForm.Compatible.transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (e : V ≃ₗ[ℝ] W) : (ω.transport e).Compatible (J.transport e)

Compatibility transports along a linear equivalence: if ω is compatible with J, then ω.transport e is compatible with the transported almost complex structure J.transport e. This expresses that e carries the compatible pair (ω, J) to the compatible pair (ω.transport e, J.transport e).