Isotropic, coisotropic, Lagrangian, and symplectic subspaces of a symplectic form

A symplectic form ω on a real module gives every submodule L a symplectic complement L^ω = {x | ∀ y ∈ L, ω(y, x) = 0}, the orthogonal complement for the bilinear form ω. The three standard size conditions on L relative to its complement organize the whole subject:

• L is isotropic when L ≤ L^ω, equivalently ω vanishes on L × L;
• L is coisotropic when L^ω ≤ L;
• L is Lagrangian when L^ω = L, i.e. isotropic and coisotropic at once.

The opposite extreme is a symplectic subspace, L ∩ L^ω = 0, on which ω restricts nondegenerately; in finite dimension it splits off, V = L ⊕ L^ω.

Lagrangian subspaces are the linear model for the boundary conditions of Lagrangian Floer homology and for the totally real tori in Sym^g(Σ). Totally real and Lagrangian are kept as separate named hypotheses, so this file builds the Lagrangian notion on the symplectic form ω rather than on an almost complex structure. The two meet on the standard model V × V: its coordinate factors are simultaneously maximal totally real (TauCeti.Submodule.isMaximalTotallyReal_prod_top_bot_product) and Lagrangian (isLagrangian_prod_top_bot below).

This is the pointwise linear-algebra layer, with no topology or smoothness bundled, built directly on Mathlib's bilinear-form orthogonal complement (Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean). Mathlib has the complement and its dimension count but no isotropic/Lagrangian vocabulary, which this file supplies.

Main declarations

• TauCeti.SymplecticForm.orthogonal: the symplectic complement L^ω.
• TauCeti.SymplecticForm.IsIsotropic, IsCoisotropic, IsLagrangian, IsSymplectic: the four predicates on subspaces.
• TauCeti.SymplecticForm.isIsotropic_iff: isotropy is the vanishing of ω on L × L, and isIsotropic_span_iff tests it on spanning vectors.
• TauCeti.SymplecticForm.isLagrangian_iff: Lagrangian is isotropic and coisotropic.
• TauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic: Lagrangian subspaces are exactly the maximal isotropic subspaces, in any dimension.
• TauCeti.SymplecticForm.isSymplectic_iff_nondegenerate_restrict: a subspace is symplectic exactly when ω restricts to it nondegenerately, and in finite dimension isSymplectic_iff_isCompl identifies this with the splitting V = L ⊕ L^ω.
• TauCeti.SymplecticForm.Tames.isSymplectic_of_mem_invtSubmodule: a subspace invariant under an almost complex structure tamed by ω is symplectic.
• TauCeti.SymplecticForm.finrank_add_finrank_orthogonal: dim L + dim L^ω = dim V.
• TauCeti.SymplecticForm.IsLagrangian.two_mul_finrank: a Lagrangian subspace is half-dimensional, 2 · dim L = dim V, and IsIsotropic.isLagrangian_of_finrank and IsCoisotropic.isLagrangian_of_finrank are the converses for an isotropic or coisotropic subspace of half the dimension. Isotropic subspaces have at most and coisotropic subspaces at least half the dimension (IsIsotropic.two_mul_finrank_le, IsCoisotropic.finrank_le_two_mul_finrank).
• TauCeti.SymplecticForm.isLagrangian_bot_iff and isLagrangian_top_iff: the zero subspace, or the whole space, is Lagrangian exactly when the ambient space is zero.
• TauCeti.SymplecticForm.isLagrangian_prod_top_bot and isLagrangian_prod_bot_top: the two coordinate factors of the standard model V × V are Lagrangian.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.3.

def TauCeti.SymplecticForm.orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Submodule ℝ V

The symplectic complement L^ω = {x | ∀ y ∈ L, ω(y, x) = 0} of a submodule L, namely the orthogonal complement of L for the bilinear form ω.

theorem TauCeti.SymplecticForm.orthogonal_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : ω.orthogonal L = ω.toBilinForm.orthogonal L

@[simp]

theorem TauCeti.SymplecticForm.mem_orthogonal_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} {x : V} : x ∈ ω.orthogonal L ↔ ∀ y ∈ L, (fun (v w : V) => (ω.toBilinForm v) w) y x = 0

theorem TauCeti.SymplecticForm.mem_orthogonal_iff' {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} {x : V} : x ∈ ω.orthogonal L ↔ ∀ y ∈ L, (fun (v w : V) => (ω.toBilinForm v) w) x y = 0

Membership in the symplectic complement, tested on the left argument of ω.

theorem TauCeti.SymplecticForm.orthogonal_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L L' : Submodule ℝ V} (h : L ≤ L') : ω.orthogonal L' ≤ ω.orthogonal L

The symplectic complement is antitone: a larger subspace has a smaller complement.

theorem TauCeti.SymplecticForm.le_orthogonal_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : L ≤ ω.orthogonal (ω.orthogonal L)

A subspace is contained in the complement of its complement.

def TauCeti.SymplecticForm.IsIsotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Prop

A submodule is isotropic if it is contained in its symplectic complement, equivalently ω vanishes on it.

def TauCeti.SymplecticForm.IsCoisotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Prop

A submodule is coisotropic if it contains its symplectic complement.

def TauCeti.SymplecticForm.IsLagrangian {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Prop

A submodule is Lagrangian if it equals its own symplectic complement.

theorem TauCeti.SymplecticForm.isIsotropic_iff_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsIsotropic L ↔ L ≤ ω.orthogonal L

Isotropy as an order statement: L is contained in its symplectic complement.

theorem TauCeti.SymplecticForm.isCoisotropic_iff_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsCoisotropic L ↔ ω.orthogonal L ≤ L

Coisotropy as an order statement: the symplectic complement is contained in L.

theorem TauCeti.SymplecticForm.isIsotropic_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsIsotropic L ↔ ∀ v ∈ L, ∀ w ∈ L, (fun (v w : V) => (ω.toBilinForm v) w) v w = 0

Isotropy is the vanishing of the symplectic form on the subspace.

theorem TauCeti.SymplecticForm.isCoisotropic_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsCoisotropic L ↔ ∀ v ∈ ω.orthogonal L, v ∈ L

Coisotropy is containment of the symplectic complement.

theorem TauCeti.SymplecticForm.mem_orthogonal_span_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {s : Set V} {x : V} : x ∈ ω.orthogonal (Submodule.span ℝ s) ↔ ∀ y ∈ s, (fun (v w : V) => (ω.toBilinForm v) w) y x = 0

The symplectic complement of a span is tested on the spanning vectors.

theorem TauCeti.SymplecticForm.isIsotropic_span_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {s : Set V} : ω.IsIsotropic (Submodule.span ℝ s) ↔ ∀ v ∈ s, ∀ w ∈ s, (fun (v w : V) => (ω.toBilinForm v) w) v w = 0

A span is isotropic exactly when ω vanishes on pairs of spanning vectors.

theorem TauCeti.SymplecticForm.IsIsotropic.mono {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L L' : Submodule ℝ V} (h : ω.IsIsotropic L') (hL : L ≤ L') : ω.IsIsotropic L

A subspace of an isotropic subspace is isotropic.

@[simp]

theorem TauCeti.SymplecticForm.isIsotropic_bot {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.IsIsotropic ⊥

The zero subspace is isotropic.

@[simp]

theorem TauCeti.SymplecticForm.isCoisotropic_top {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.IsCoisotropic ⊤

The whole space is coisotropic.

theorem TauCeti.SymplecticForm.isLagrangian_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsLagrangian L ↔ ω.IsIsotropic L ∧ ω.IsCoisotropic L

A Lagrangian subspace is both isotropic and coisotropic, and conversely.

theorem TauCeti.SymplecticForm.IsLagrangian.isIsotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsLagrangian L) : ω.IsIsotropic L

A Lagrangian subspace is isotropic.

theorem TauCeti.SymplecticForm.IsLagrangian.isCoisotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsLagrangian L) : ω.IsCoisotropic L

A Lagrangian subspace is coisotropic.

theorem TauCeti.SymplecticForm.IsLagrangian.symplecticForm_apply_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsLagrangian L) {v w : V} (hv : v ∈ L) (hw : w ∈ L) : (fun (v w : V) => (ω.toBilinForm v) w) v w = 0

The symplectic form vanishes on a Lagrangian subspace.

@[simp]

theorem TauCeti.SymplecticForm.orthogonal_bot {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.orthogonal ⊥ = ⊤

The symplectic complement of the zero subspace is the whole space.

@[simp]

theorem TauCeti.SymplecticForm.orthogonal_top {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.orthogonal ⊤ = ⊥

The symplectic complement of the whole space is zero, by nondegeneracy of ω.

@[simp]

theorem TauCeti.SymplecticForm.isLagrangian_bot_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.IsLagrangian ⊥ ↔ Subsingleton V

The zero subspace is Lagrangian exactly when the ambient space is zero.

@[simp]

theorem TauCeti.SymplecticForm.isLagrangian_top_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.IsLagrangian ⊤ ↔ Subsingleton V

The whole space is Lagrangian exactly when it is zero.

theorem TauCeti.SymplecticForm.IsIsotropic.sup_span_singleton {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsIsotropic L) {v : V} (hv : v ∈ ω.orthogonal L) : ω.IsIsotropic (L ⊔ ℝ ∙ v)

Adjoining a vector of the symplectic complement to an isotropic subspace keeps it isotropic.

theorem TauCeti.SymplecticForm.isCoisotropic_of_maximal_isIsotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : Maximal ω.IsIsotropic L) : ω.IsCoisotropic L

An isotropic subspace contained in no strictly larger isotropic subspace is coisotropic.

theorem TauCeti.SymplecticForm.IsLagrangian.maximal_isIsotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsLagrangian L) : Maximal ω.IsIsotropic L

A Lagrangian subspace is a maximal isotropic subspace.

theorem TauCeti.SymplecticForm.isLagrangian_iff_maximal_isIsotropic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsLagrangian L ↔ Maximal ω.IsIsotropic L

Lagrangian subspaces are exactly the maximal isotropic subspaces, in any dimension.

def TauCeti.SymplecticForm.IsSymplectic {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Prop

A submodule is symplectic if it meets its symplectic complement only in zero, equivalently (isSymplectic_iff_nondegenerate_restrict) ω restricts to it nondegenerately.

theorem TauCeti.SymplecticForm.isSymplectic_iff_disjoint {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsSymplectic L ↔ Disjoint L (ω.orthogonal L)

A symplectic subspace is one disjoint from its symplectic complement.

theorem TauCeti.SymplecticForm.isSymplectic_iff_nondegenerate_restrict {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} : ω.IsSymplectic L ↔ (ω.toBilinForm.restrict L).Nondegenerate

A subspace is symplectic exactly when ω restricts to it as a nondegenerate form, in any dimension.

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

The restriction of ω to a symplectic subspace is nondegenerate, so ω.restrict L applies.

@[simp]

theorem TauCeti.SymplecticForm.isSymplectic_bot {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.IsSymplectic ⊥

The zero subspace is symplectic.

@[simp]

theorem TauCeti.SymplecticForm.isSymplectic_top {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} : ω.IsSymplectic ⊤

The whole space is symplectic.

theorem TauCeti.SymplecticForm.Tames.isSymplectic_of_mem_invtSubmodule {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} {J : AlmostComplexStructure V} (hJ : ω.Tames J) (hL : L ∈ Module.End.invtSubmodule J.toLinearMap) : ω.IsSymplectic L

A subspace invariant under an almost complex structure J tamed by ω is symplectic: a nonzero vector v of it pairs positively with J v, which lies in it too.

theorem TauCeti.SymplecticForm.IsIsotropic.eq_bot_of_isSymplectic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsIsotropic L) (hs : ω.IsSymplectic L) : L = ⊥

A subspace that is both isotropic and symplectic is zero.

theorem TauCeti.SymplecticForm.isLagrangian_graph_iff_of_pairing {V : Type u_2} {D : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup D] [Module ℝ D] (ω : SymplecticForm (V × D)) (pair : D → V → ℝ) (hω : ∀ (x y : V × D), (fun (v w : V × D) => (ω.toBilinForm v) w) x y = pair y.2 x.1 - pair x.2 y.1) (A : V →ₗ[ℝ] D) : ω.IsLagrangian A.graph ↔ ∀ (v w : V), pair (A v) w = pair (A w) v

A graph is Lagrangian exactly when its defining map is symmetric for a pairing whose associated product symplectic form is specified by the hypothesis.

theorem TauCeti.SymplecticForm.finrank_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Module.finrank ℝ ↥(ω.orthogonal L) = Module.finrank ℝ V - Module.finrank ℝ ↥L

The symplectic complement has complementary dimension: dim L^ω = dim V - dim L.

theorem TauCeti.SymplecticForm.orthogonal_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : ω.orthogonal (ω.orthogonal L) = L

The double complement of a subspace is itself.

theorem TauCeti.SymplecticForm.orthogonal_inf {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (L L' : Submodule ℝ V) : ω.orthogonal (L ⊓ L') = ω.orthogonal L ⊔ ω.orthogonal L'

The complement of an intersection is the sum of the complements.

theorem TauCeti.SymplecticForm.IsIsotropic.two_mul_finrank_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsIsotropic L) : 2 * Module.finrank ℝ ↥L ≤ Module.finrank ℝ V

An isotropic subspace has at most half the dimension of the ambient space.

theorem TauCeti.SymplecticForm.IsLagrangian.two_mul_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsLagrangian L) : 2 * Module.finrank ℝ ↥L = Module.finrank ℝ V

A Lagrangian subspace is exactly half-dimensional: 2 · dim L = dim V.

theorem TauCeti.SymplecticForm.IsIsotropic.isLagrangian_of_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsIsotropic L) (hdim : 2 * Module.finrank ℝ ↥L = Module.finrank ℝ V) : ω.IsLagrangian L

An isotropic subspace of half the dimension of the ambient space is Lagrangian.

theorem TauCeti.SymplecticForm.finrank_add_finrank_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (L : Submodule ℝ V) : Module.finrank ℝ ↥L + Module.finrank ℝ ↥(ω.orthogonal L) = Module.finrank ℝ V

The symplectic complement has complementary dimension, in additive form: dim L + dim L^ω = dim V.

theorem TauCeti.SymplecticForm.IsCoisotropic.finrank_le_two_mul_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsCoisotropic L) : Module.finrank ℝ V ≤ 2 * Module.finrank ℝ ↥L

A coisotropic subspace has at least half the dimension of the ambient space.

theorem TauCeti.SymplecticForm.IsCoisotropic.isLagrangian_of_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsCoisotropic L) (hdim : 2 * Module.finrank ℝ ↥L = Module.finrank ℝ V) : ω.IsLagrangian L

A coisotropic subspace of half the dimension of the ambient space is Lagrangian.

theorem TauCeti.SymplecticForm.isSymplectic_iff_isCompl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] : ω.IsSymplectic L ↔ IsCompl L (ω.orthogonal L)

In finite dimension a subspace is symplectic exactly when it splits the space together with its symplectic complement, V = L ⊕ L^ω.

theorem TauCeti.SymplecticForm.IsSymplectic.isCompl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsSymplectic L) : IsCompl L (ω.orthogonal L)

A symplectic subspace splits the space together with its symplectic complement.

@[simp]

theorem TauCeti.SymplecticForm.isSymplectic_orthogonal_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] : ω.IsSymplectic (ω.orthogonal L) ↔ ω.IsSymplectic L

The symplectic complement of a subspace is symplectic exactly when the subspace is.

theorem TauCeti.SymplecticForm.IsSymplectic.orthogonal {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} [FiniteDimensional ℝ V] (h : ω.IsSymplectic L) : ω.IsSymplectic (ω.orthogonal L)

The symplectic complement of a symplectic subspace is symplectic.

theorem TauCeti.SymplecticForm.isLagrangian_prod_top_bot {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : stdSymplecticForm.IsLagrangian (⊤.prod ⊥)

The first coordinate factor V × {0} is Lagrangian for the standard symplectic form.

theorem TauCeti.SymplecticForm.isLagrangian_prod_bot_top {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : stdSymplecticForm.IsLagrangian (⊥.prod ⊤)

The second coordinate factor {0} × V is Lagrangian for the standard symplectic form.