Products, transports, and graphs of Lagrangian subspaces

This file collects the linear symplectic constructions that produce isotropic, coisotropic, and Lagrangian subspaces out of existing ones. All three groups are pointwise linear algebra over the symplectic-form API in TauCeti.Geometry.Symplectic.Lagrangian.Basic.

• Products. The direct-sum symplectic form ω₁.prod ω₂ on V × W has the product orthogonal-complement formula (L₁ × L₂)^(ω₁ ⊕ ω₂) = L₁^ω₁ × L₂^ω₂, so isotropy, coisotropy, and Lagrangian-ness of a product subspace are factorwise.
• Transports. A linear equivalence e : V ≃ₗ[ℝ] W transports a symplectic form by pulling arguments back along e.symm, sending a subspace to its image L.map e.toLinearMap. Symplectic complements commute with transport, so all three boundary predicates are invariant under linear coordinate changes.
• Graphs. In the twisted product (V × W, ω₁ ⊖ ω₂) the graph {(v, e v)} of a real-linear isomorphism e : V ≃ W is Lagrangian exactly when e is a symplectomorphism; the special case e = id makes the diagonal of (V × V, ω ⊖ ω) Lagrangian. This is the linear model of the Lagrangian-correspondence principle needed by Lagrangian Floer homology: the boundary conditions of Floer strips between two Lagrangians are packaged as a single Lagrangian in the twisted product, and the diagonal is the model boundary condition for the identity continuation. In the direct-sum product (V × W, ω₁ ⊕ ω₂) the graph of a linear map f is instead a symplectic subspace exactly when (v, w) ↦ ω₁(v, w) + ω₂(f v, f w) is nondegenerate.

Main declarations

• TauCeti.SymplecticForm.orthogonal_prod, isIsotropic_prod_iff, isCoisotropic_prod_iff, isLagrangian_prod_iff, isSymplectic_prod_iff, and the one-way IsIsotropic.prod, IsCoisotropic.prod, IsLagrangian.prod, IsSymplectic.prod: the product API.
• TauCeti.SymplecticForm.orthogonal_map_transport, IsSymplectomorphism.map_orthogonal, isIsotropic_map_transport_iff, isCoisotropic_map_transport_iff, isLagrangian_map_transport_iff, isSymplectic_map_transport_iff, and the one-way IsIsotropic.map_transport, IsCoisotropic.map_transport, IsLagrangian.map_transport, IsSymplectic.map_transport: the transport API.
• TauCeti.SymplecticForm.isIsotropic_graph_iff, isIsotropic_linearEquiv_graph_iff, IsSymplectomorphism.isLagrangian_graph, isLagrangian_graph_iff, isLagrangian_diagonal, and isSymplectic_graph_iff: the graph API.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Sections 2.1 and 2.3. The twisted product form ω₁ ⊖ ω₂ itself lives with the rest of the product-form API in TauCeti.Geometry.Symplectic.Prod.Basic, and the graph is Mathlib's submodule LinearMap.graph.

@[simp]

theorem TauCeti.SymplecticForm.orthogonal_prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} : (ω₁.prod ω₂).orthogonal (L₁.prod L₂) = (ω₁.orthogonal L₁).prod (ω₂.orthogonal L₂)

The symplectic complement of a product subspace is the product of the symplectic complements for the direct-sum symplectic form.

@[simp]

theorem TauCeti.SymplecticForm.isIsotropic_prod_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} : (ω₁.prod ω₂).IsIsotropic (L₁.prod L₂) ↔ ω₁.IsIsotropic L₁ ∧ ω₂.IsIsotropic L₂

A product subspace is isotropic for the direct-sum symplectic form exactly when both factors are isotropic.

theorem TauCeti.SymplecticForm.IsIsotropic.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} (h₁ : ω₁.IsIsotropic L₁) (h₂ : ω₂.IsIsotropic L₂) : (ω₁.prod ω₂).IsIsotropic (L₁.prod L₂)

The product of two isotropic subspaces is isotropic for the direct-sum symplectic form.

@[simp]

theorem TauCeti.SymplecticForm.isCoisotropic_prod_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} : (ω₁.prod ω₂).IsCoisotropic (L₁.prod L₂) ↔ ω₁.IsCoisotropic L₁ ∧ ω₂.IsCoisotropic L₂

A product subspace is coisotropic for the direct-sum symplectic form exactly when both factors are coisotropic.

theorem TauCeti.SymplecticForm.IsCoisotropic.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} (h₁ : ω₁.IsCoisotropic L₁) (h₂ : ω₂.IsCoisotropic L₂) : (ω₁.prod ω₂).IsCoisotropic (L₁.prod L₂)

The product of two coisotropic subspaces is coisotropic for the direct-sum symplectic form.

@[simp]

theorem TauCeti.SymplecticForm.isLagrangian_prod_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} : (ω₁.prod ω₂).IsLagrangian (L₁.prod L₂) ↔ ω₁.IsLagrangian L₁ ∧ ω₂.IsLagrangian L₂

A product subspace is Lagrangian for the direct-sum symplectic form exactly when both factors are Lagrangian.

theorem TauCeti.SymplecticForm.IsLagrangian.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} (h₁ : ω₁.IsLagrangian L₁) (h₂ : ω₂.IsLagrangian L₂) : (ω₁.prod ω₂).IsLagrangian (L₁.prod L₂)

The product of two Lagrangian subspaces is Lagrangian for the direct-sum symplectic form.

@[simp]

theorem TauCeti.SymplecticForm.isSymplectic_prod_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} : (ω₁.prod ω₂).IsSymplectic (L₁.prod L₂) ↔ ω₁.IsSymplectic L₁ ∧ ω₂.IsSymplectic L₂

A product subspace is symplectic for the direct-sum symplectic form exactly when both factors are symplectic.

theorem TauCeti.SymplecticForm.IsSymplectic.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {L₁ : Submodule ℝ V} {L₂ : Submodule ℝ W} (h₁ : ω₁.IsSymplectic L₁) (h₂ : ω₂.IsSymplectic L₂) : (ω₁.prod ω₂).IsSymplectic (L₁.prod L₂)

The product of two symplectic subspaces is symplectic for the direct-sum symplectic form.

@[simp]

theorem TauCeti.SymplecticForm.orthogonal_map_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} : (ω.transport e).orthogonal (Submodule.map (↑e) L) = Submodule.map (↑e) (ω.orthogonal L)

The symplectic complement of a transported subspace is the transport of the symplectic complement.

theorem TauCeti.SymplecticForm.IsSymplectomorphism.map_orthogonal {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {e : V ≃ₗ[ℝ] W} {ω' : SymplecticForm W} (he : ω.IsSymplectomorphism ω' e) (L : Submodule ℝ V) : Submodule.map (↑e) (ω.orthogonal L) = ω'.orthogonal (Submodule.map (↑e) L)

A linear symplectomorphism carries symplectic complements to symplectic complements.

@[simp]

theorem TauCeti.SymplecticForm.isIsotropic_map_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} : (ω.transport e).IsIsotropic (Submodule.map (↑e) L) ↔ ω.IsIsotropic L

Isotropy is invariant under transporting both the symplectic form and the subspace along a linear equivalence.

@[simp]

theorem TauCeti.SymplecticForm.isCoisotropic_map_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} : (ω.transport e).IsCoisotropic (Submodule.map (↑e) L) ↔ ω.IsCoisotropic L

Coisotropy is invariant under transporting both the symplectic form and the subspace along a linear equivalence.

@[simp]

theorem TauCeti.SymplecticForm.isLagrangian_map_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} : (ω.transport e).IsLagrangian (Submodule.map (↑e) L) ↔ ω.IsLagrangian L

Lagrangian-ness is invariant under transporting both the symplectic form and the subspace along a linear equivalence.

@[simp]

theorem TauCeti.SymplecticForm.isSymplectic_map_transport_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} : (ω.transport e).IsSymplectic (Submodule.map (↑e) L) ↔ ω.IsSymplectic L

Being a symplectic subspace is invariant under transporting both the symplectic form and the subspace along a linear equivalence.

theorem TauCeti.SymplecticForm.IsIsotropic.map_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} (h : ω.IsIsotropic L) : (ω.transport e).IsIsotropic (Submodule.map (↑e) L)

Transport an isotropic subspace along a linear equivalence, together with the transported symplectic form.

theorem TauCeti.SymplecticForm.IsCoisotropic.map_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} (h : ω.IsCoisotropic L) : (ω.transport e).IsCoisotropic (Submodule.map (↑e) L)

Transport a coisotropic subspace along a linear equivalence, together with the transported symplectic form.

theorem TauCeti.SymplecticForm.IsLagrangian.map_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} (h : ω.IsLagrangian L) : (ω.transport e).IsLagrangian (Submodule.map (↑e) L)

Transport a Lagrangian subspace along a linear equivalence, together with the transported symplectic form.

theorem TauCeti.SymplecticForm.IsSymplectic.map_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {L : Submodule ℝ V} {e : V ≃ₗ[ℝ] W} (h : ω.IsSymplectic L) : (ω.transport e).IsSymplectic (Submodule.map (↑e) L)

Transport a symplectic subspace along a linear equivalence, together with the transported symplectic form.

@[simp]

theorem TauCeti.SymplecticForm.isIsotropic_graph_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {f : V →ₗ[ℝ] W} : (ω₁.twistedProd ω₂).IsIsotropic f.graph ↔ ∀ (v w : V), (fun (v w : W) => (ω₂.toBilinForm v) w) (f v) (f w) = (fun (v w : V) => (ω₁.toBilinForm v) w) v w

The graph of f is isotropic for the twisted product form iff f preserves the symplectic forms pointwise: ω₂(f v, f w) = ω₁(v, w).

theorem TauCeti.SymplecticForm.isIsotropic_linearEquiv_graph_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {e : V ≃ₗ[ℝ] W} : (ω₁.twistedProd ω₂).IsIsotropic (↑e).graph ↔ ω₁.IsSymplectomorphism ω₂ e

The graph of e is isotropic for the twisted product form iff e is a symplectomorphism.

This is a plain bridging lemma, not a simp lemma: the general isIsotropic_graph_iff already puts graph isotropy into its own normal form, so marking this @[simp] too would leave two competing normal forms for e.toLinearMap.graph.

theorem TauCeti.SymplecticForm.IsSymplectomorphism.isLagrangian_graph {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) : (ω₁.twistedProd ω₂).IsLagrangian (↑e).graph

The graph of a symplectomorphism e : V ≃ₗ[ℝ] W is a Lagrangian subspace of the twisted product (V × W, ω₁ ⊖ ω₂). No finite-dimensionality is required.

@[simp]

theorem TauCeti.SymplecticForm.isLagrangian_graph_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {e : V ≃ₗ[ℝ] W} : (ω₁.twistedProd ω₂).IsLagrangian (↑e).graph ↔ ω₁.IsSymplectomorphism ω₂ e

The graph of e is Lagrangian for the twisted product form iff e is a symplectomorphism.

theorem TauCeti.SymplecticForm.isSymplectic_graph_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {f : V →ₗ[ℝ] W} : (ω₁.prod ω₂).IsSymplectic f.graph ↔ ∀ (v : V), (∀ (w : V), (fun (v w : V) => (ω₁.toBilinForm v) w) v w + (fun (v w : W) => (ω₂.toBilinForm v) w) (f v) (f w) = 0) → v = 0

The graph of f is a symplectic subspace for the direct-sum form exactly when the form (v, w) ↦ ω₁(v, w) + ω₂(f v, f w) on V is nondegenerate: a vector pairing to zero with every vector under it is zero.

theorem TauCeti.SymplecticForm.isLagrangian_diagonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) : (ω.twistedProd ω).IsLagrangian (↑(LinearEquiv.refl ℝ V)).graph

The diagonal of (V × V, ω ⊖ ω), realized as the graph of the identity equivalence, is Lagrangian. This is the boundary condition modeled by the identity continuation in Lagrangian Floer homology.