Almost complex structures and compatible symplectic forms

This file starts the pointwise linear-algebra API for the analytic Heegaard Floer roadmap. It records almost complex structures on real modules, symplectic bilinear forms, and the standard tameness and compatibility predicates between them.

These are the fiberwise definitions used before introducing smooth bundles, almost complex manifolds, and J-holomorphic maps. The smooth manifold layer should reuse these predicates on tangent fibers rather than restating the linear algebra.

Main declarations

• TauCeti.AlmostComplexStructure: a real-linear endomorphism J with J^2 = -1.
• TauCeti.IsComplexLinearMap: a real-linear map intertwining two almost complex structures.
• TauCeti.SymplecticForm: an alternating, nondegenerate real bilinear form.
• TauCeti.SymplecticForm.apply_smul_add_smul: evaluation of a symplectic form on the plane spanned by two vectors, and TauCeti.SymplecticForm.exists_apply_eq_one: existence of a hyperbolic partner for every nonzero vector.
• TauCeti.SymplecticForm.Tames: the positivity condition 0 < ω v (J v) for v ≠ 0.
• TauCeti.SymplecticForm.Compatible: J-invariance plus positivity of ω(·, J ·).
• TauCeti.AlmostComplexStructure.product: the standard almost complex structure on V × V, sending (x, y) to (-y, x).

The definitions follow the standard conventions in McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.2, specialized here to the pointwise real-linear setting.

structure TauCeti.AlmostComplexStructure (V : Type u_4) [AddCommGroup V] [Module ℝ V] : Type u_4

A pointwise almost complex structure is a real-linear endomorphism whose square is -1.

This is the fiberwise object underlying an almost complex structure on a real vector bundle or manifold. Smoothness is deliberately not bundled here; the analytic roadmap needs the linear algebra separately on each tangent space.

• toLinearMap : V →ₗ[ℝ] V

  The real-linear endomorphism usually denoted J.

• square_neg : self.toLinearMap ∘ₗ self.toLinearMap = -LinearMap.id

  The defining identity J ∘ J = -1.

theorem TauCeti.AlmostComplexStructure.toLinearMap_injective {V : Type u_1} [AddCommGroup V] [Module ℝ V] : Function.Injective toLinearMap

The underlying linear map determines an almost complex structure: the only data is the endomorphism, the defining identity being a proposition.

@[instance_reducible]

instance TauCeti.AlmostComplexStructure.instCoeFunForall {V : Type u_1} [AddCommGroup V] [Module ℝ V] : CoeFun (AlmostComplexStructure V) fun (x : AlmostComplexStructure V) => V → V

Equations

• TauCeti.AlmostComplexStructure.instCoeFunForall = { coe := fun (J : TauCeti.AlmostComplexStructure V) => ⇑J.toLinearMap }

@[simp]

theorem TauCeti.AlmostComplexStructure.apply_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.toLinearMap (J.toLinearMap v) = -v

Applying J twice gives -v.

theorem TauCeti.AlmostComplexStructure.injective {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Function.Injective ⇑J.toLinearMap

The underlying linear map of an almost complex structure is injective.

theorem TauCeti.AlmostComplexStructure.surjective {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Function.Surjective ⇑J.toLinearMap

The underlying linear map of an almost complex structure is surjective.

def TauCeti.AlmostComplexStructure.linearEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : V ≃ₗ[ℝ] V

The linear equivalence attached to an almost complex structure.

Its inverse is -J; this is often the convenient way to move bilinear-form statements across J.

Equations

• J.linearEquiv = { toLinearMap := J.toLinearMap, invFun := fun (v : V) => -J.toLinearMap v, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.AlmostComplexStructure.linearEquiv_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.linearEquiv v = J.toLinearMap v

@[simp]

theorem TauCeti.AlmostComplexStructure.linearEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.linearEquiv.symm v = -J.toLinearMap v

@[simp]

theorem TauCeti.AlmostComplexStructure.map_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {v : V} : J.toLinearMap v = 0 ↔ v = 0

theorem TauCeti.AlmostComplexStructure.map_ne_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {v : V} : J.toLinearMap v ≠ 0 ↔ v ≠ 0

theorem TauCeti.AlmostComplexStructure.ext {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J K : AlmostComplexStructure V} (h : ∀ (v : V), J.toLinearMap v = K.toLinearMap v) : J = K

Two almost complex structures agreeing pointwise are equal.

theorem TauCeti.AlmostComplexStructure.ext_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J K : AlmostComplexStructure V} : J = K ↔ ∀ (v : V), J.toLinearMap v = K.toLinearMap v

def TauCeti.AlmostComplexStructure.neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : AlmostComplexStructure V

The negation of an almost complex structure is again an almost complex structure.

Equations

• J.neg = { toLinearMap := -J.toLinearMap, square_neg := ⋯ }

@[instance_reducible]

instance TauCeti.AlmostComplexStructure.instNeg {V : Type u_1} [AddCommGroup V] [Module ℝ V] : Neg (AlmostComplexStructure V)

Equations

• TauCeti.AlmostComplexStructure.instNeg = { neg := TauCeti.AlmostComplexStructure.neg }

@[simp]

theorem TauCeti.AlmostComplexStructure.neg_toLinearMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : (-J).toLinearMap = -J.toLinearMap

@[simp]

theorem TauCeti.AlmostComplexStructure.neg_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (-J).toLinearMap v = -J.toLinearMap v

def TauCeti.AlmostComplexStructure.product (V : Type u_4) [AddCommGroup V] [Module ℝ V] : AlmostComplexStructure (V × V)

The standard almost complex structure on V × V, sending (x, y) to (-y, x).

Equations

• TauCeti.AlmostComplexStructure.product V = { toLinearMap := { toFun := fun (v : V × V) => (-v.2, v.1), map_add' := ⋯, map_smul' := ⋯ }, square_neg := ⋯ }

@[simp]

theorem TauCeti.AlmostComplexStructure.product_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (v : V × V) : (product V).toLinearMap v = (-v.2, v.1)

def TauCeti.IsComplexLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (F : V →ₗ[ℝ] W) : Prop

A real-linear map is complex-linear with respect to two fixed pointwise almost complex structures if it intertwines them.

Equations

• TauCeti.IsComplexLinearMap J J' F = (F ∘ₗ J.toLinearMap = J'.toLinearMap ∘ₗ F)

theorem TauCeti.isComplexLinearMap_iff_isComplexLinear {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (F : V →ₗ[ℝ] W) : IsComplexLinearMap J J' F ↔ IsComplexLinear J.toLinearMap J'.toLinearMap F

The bundled almost-complex predicate is the raw complex-linearity predicate applied to the underlying endomorphisms.

theorem TauCeti.isComplexLinearMap_iff_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (F : V →ₗ[ℝ] W) : IsComplexLinearMap J J' F ↔ ∀ (v : V), F (J.toLinearMap v) = J'.toLinearMap (F v)

Rewrite complex-linearity of a real-linear map as the pointwise equation F (J v) = J' (F v).

theorem TauCeti.isComplexLinearMap_iff_mem_complexLinearMaps {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (F : V →ₗ[ℝ] W) : IsComplexLinearMap J J' F ↔ F ∈ complexLinearMaps J.toLinearMap J'.toLinearMap

Complex-linearity for almost complex structures is membership in the existing submodule of raw-linear complex-linear maps.

@[simp]

theorem TauCeti.isComplexLinearMap_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) : IsComplexLinearMap J J' 0

The zero map is complex-linear for any source and target almost complex structures.

theorem TauCeti.IsComplexLinearMap.add {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F G : V →ₗ[ℝ] W} (hF : IsComplexLinearMap J J' F) (hG : IsComplexLinearMap J J' G) : IsComplexLinearMap J J' (F + G)

Complex-linear maps are closed under addition.

theorem TauCeti.IsComplexLinearMap.neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (hF : IsComplexLinearMap J J' F) : IsComplexLinearMap J J' (-F)

Complex-linear maps are closed under negation.

@[simp]

theorem TauCeti.isComplexLinearMap_neg_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} : IsComplexLinearMap J J' (-F) ↔ IsComplexLinearMap J J' F

Negating a map preserves and reflects complex-linearity.

theorem TauCeti.IsComplexLinearMap.neg_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (hF : IsComplexLinearMap J J' F) : IsComplexLinearMap (-J) (-J') F

Complex-linearity is unchanged after negating both the source and target almost complex structures.

theorem TauCeti.IsComplexLinearMap.of_neg_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (hF : IsComplexLinearMap (-J) (-J') F) : IsComplexLinearMap J J' F

If a map is complex-linear after negating both structures, then it was complex-linear before the sign change.

@[simp]

theorem TauCeti.isComplexLinearMap_neg_neg_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} : IsComplexLinearMap (-J) (-J') F ↔ IsComplexLinearMap J J' F

Negating both almost complex structures leaves the complex-linearity condition unchanged.

theorem TauCeti.IsComplexLinearMap.sub {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F G : V →ₗ[ℝ] W} (hF : IsComplexLinearMap J J' F) (hG : IsComplexLinearMap J J' G) : IsComplexLinearMap J J' (F - G)

Complex-linear maps are closed under subtraction.

theorem TauCeti.IsComplexLinearMap.smul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (c : ℝ) (hF : IsComplexLinearMap J J' F) : IsComplexLinearMap J J' (c • F)

Complex-linear maps are closed under real scalar multiplication.

@[simp]

theorem TauCeti.isComplexLinearMap_id {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : IsComplexLinearMap J J LinearMap.id

The identity map is complex-linear with respect to the same almost complex structure.

theorem TauCeti.IsComplexLinearMap.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup X] [Module ℝ X] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {J'' : AlmostComplexStructure X} {F : V →ₗ[ℝ] W} {G : W →ₗ[ℝ] X} (hG : IsComplexLinearMap J' J'' G) (hF : IsComplexLinearMap J J' F) : IsComplexLinearMap J J'' (G ∘ₗ F)

Complex-linear maps are closed under composition.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_toLinearMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : IsComplexLinearMap J J J.toLinearMap

An almost complex structure is complex-linear as a map from its module to itself.

theorem TauCeti.IsComplexLinearMap.comp_almostComplexStructure_toLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (hF : IsComplexLinearMap J J' F) : IsComplexLinearMap J J' (F ∘ₗ J.toLinearMap)

Precomposing a complex-linear map by the source almost complex structure again gives a complex-linear map.

theorem TauCeti.IsComplexLinearMap.of_comp_almostComplexStructure_toLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (hF : IsComplexLinearMap J J' (F ∘ₗ J.toLinearMap)) : IsComplexLinearMap J J' F

If precomposition by the source almost complex structure is complex-linear, then the original map was complex-linear.

@[simp]

theorem TauCeti.isComplexLinearMap_comp_almostComplexStructure_toLinearMap_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} : IsComplexLinearMap J J' (F ∘ₗ J.toLinearMap) ↔ IsComplexLinearMap J J' F

Precomposition by the source almost complex structure preserves and reflects complex-linearity.

theorem TauCeti.bilinForm_comp_almostComplexStructure {U : Type u_4} {V : Type u_5} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsAlt) (J₀ : AlmostComplexStructure U) (F : U →ₗ[ℝ] V) (v : U) : (B ((F ∘ₗ J₀.toLinearMap) v)) ((F ∘ₗ J₀.toLinearMap) (J₀.toLinearMap v)) = (B (F v)) (F (J₀.toLinearMap v))

The ordered pairing B (F v) (F (J₀ v)) of an alternating bilinear form B is unchanged when both arguments are precomposed by a source almost complex structure J₀: rotating the source by J₀ sends the pair (v, J₀ v) to (J₀ v, -v), and alternation leaves the pairing unchanged.

Only alternation of B is used, so the statement lives at the LinearMap.BilinForm level; the SymplecticForm corollary is SymplecticForm.symplecticForm_comp_almostComplexStructure.

structure TauCeti.SymplecticForm (V : Type u_4) [AddCommGroup V] [Module ℝ V] : Type u_4

A symplectic form on a real module is an alternating, nondegenerate bilinear form.

This is the pointwise linear-algebra notion. Closedness of a differential form belongs to the manifold layer and is not bundled here.

• toBilinForm : LinearMap.BilinForm ℝ V

  The underlying real bilinear form.

• isAlt : self.toBilinForm.IsAlt

  Symplectic forms are alternating.

• nondegenerate : self.toBilinForm.Nondegenerate

  Symplectic forms are nondegenerate.

theorem TauCeti.SymplecticForm.toBilinForm_injective {V : Type u_1} [AddCommGroup V] [Module ℝ V] : Function.Injective toBilinForm

The underlying bilinear form determines a symplectic form: the only data is the form, the alternating and nondegeneracy conditions being propositions.

@[instance_reducible]

instance TauCeti.SymplecticForm.instCoeFunForallForallReal {V : Type u_1} [AddCommGroup V] [Module ℝ V] : CoeFun (SymplecticForm V) fun (x : SymplecticForm V) => V → V → ℝ

Equations

• TauCeti.SymplecticForm.instCoeFunForallForallReal = { coe := fun (ω : TauCeti.SymplecticForm V) (v w : V) => (ω.toBilinForm v) w }

@[simp]

theorem TauCeti.SymplecticForm.self_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (v : V) : (fun (v w : V) => (ω.toBilinForm v) w) v v = 0

A symplectic form vanishes on the diagonal.

theorem TauCeti.SymplecticForm.neg_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (v w : V) : -(fun (v w : V) => (ω.toBilinForm v) w) v w = (fun (v w : V) => (ω.toBilinForm v) w) w v

A symplectic form is skew-symmetric in the usual additive form.

theorem TauCeti.SymplecticForm.apply_smul_add_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (x y : V) (a b c d : ℝ) : (fun (v w : V) => (ω.toBilinForm v) w) (a • x + b • y) (c • x + d • y) = (a * d - b * c) * (fun (v w : V) => (ω.toBilinForm v) w) x y

Bilinear expansion of ω on the plane spanned by a pair of vectors: only the mixed term ω x y survives.

theorem TauCeti.SymplecticForm.symplecticForm_comp_almostComplexStructure {V : Type u_1} [AddCommGroup V] [Module ℝ V] {U : Type u_4} [AddCommGroup U] [Module ℝ U] (ω : SymplecticForm V) (J₀ : AlmostComplexStructure U) (F : U →ₗ[ℝ] V) (v : U) : (fun (v w : V) => (ω.toBilinForm v) w) ((F ∘ₗ J₀.toLinearMap) v) ((F ∘ₗ J₀.toLinearMap) (J₀.toLinearMap v)) = (fun (v w : V) => (ω.toBilinForm v) w) (F v) (F (J₀.toLinearMap v))

The ordered area density ω (F v) (F (J₀ v)) is unchanged when both arguments are precomposed by a source almost complex structure J₀: rotating the source by J₀ sends the pair (v, J₀ v) to (J₀ v, -v), which has the same symplectic area. This is the SymplecticForm corollary of bilinForm_comp_almostComplexStructure.

theorem TauCeti.SymplecticForm.isRefl {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) : ω.toBilinForm.IsRefl

A symplectic form is reflexive as an orthogonality relation.

theorem TauCeti.SymplecticForm.separatingLeft {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) : LinearMap.SeparatingLeft ω.toBilinForm

Nondegeneracy can be tested on the left variable for a symplectic form.

theorem TauCeti.SymplecticForm.separatingRight {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) : LinearMap.SeparatingRight ω.toBilinForm

Nondegeneracy can be tested on the right variable for a symplectic form.

theorem TauCeti.SymplecticForm.exists_apply_eq_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) {x : V} (hx : x ≠ 0) : ∃ (y : V), (fun (v w : V) => (ω.toBilinForm v) w) x y = 1

Nondegeneracy supplies a hyperbolic partner: every nonzero vector x admits a vector y with ω x y = 1.

def TauCeti.SymplecticForm.pullback {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : LinearMap.BilinForm ℝ V

The bilinear form ω(J ·, J ·).

Equations

• ω.pullback J = ω.toBilinForm.comp J.toLinearMap J.toLinearMap

@[simp]

theorem TauCeti.SymplecticForm.pullback_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v w : V) : ((ω.pullback J) v) w = (fun (v w : V) => (ω.toBilinForm v) w) (J.toLinearMap v) (J.toLinearMap w)

def TauCeti.SymplecticForm.Invariant {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : Prop

A symplectic form is J-invariant when ω(Jv, Jw) = ω(v, w).

Equations

• ω.Invariant J = (ω.pullback J = ω.toBilinForm)

theorem TauCeti.SymplecticForm.invariant_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : ω.Invariant J ↔ ∀ (v w : V), (fun (v w : V) => (ω.toBilinForm v) w) (J.toLinearMap v) (J.toLinearMap w) = (fun (v w : V) => (ω.toBilinForm v) w) v w

def TauCeti.SymplecticForm.associatedBilinForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : LinearMap.BilinForm ℝ V

The bilinear form g(v,w) = ω(v, Jw) associated to ω and J.

Equations

• ω.associatedBilinForm J = ω.toBilinForm.compRight J.toLinearMap

@[simp]

theorem TauCeti.SymplecticForm.associatedBilinForm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v w : V) : ((ω.associatedBilinForm J) v) w = (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap w)

def TauCeti.SymplecticForm.Tames {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : Prop

ω tames J if ω(v, Jv) is positive on every nonzero vector.

Equations

• ω.Tames J = ∀ (v : V), v ≠ 0 → 0 < (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap v)

theorem TauCeti.SymplecticForm.tames_iff_associated_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : ω.Tames J ↔ (LinearMap.BilinMap.toQuadraticMap (ω.associatedBilinForm J)).PosDef

structure TauCeti.SymplecticForm.Compatible {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : Prop

ω is compatible with J if it is J-invariant and ω(·, J ·) is positive definite.

• invariant : ω.Invariant J

  The form is invariant under applying J to both variables.

• positive : (LinearMap.BilinMap.toQuadraticMap (ω.associatedBilinForm J)).PosDef

  The associated quadratic form v ↦ ω(v, Jv) is positive definite.

theorem TauCeti.SymplecticForm.compatible_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : ω.Compatible J ↔ ω.Invariant J ∧ ω.Tames J

Compatibility is equivalently J-invariance plus tameness.

theorem TauCeti.SymplecticForm.Compatible.of_tames {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinvariant : ω.Invariant J) (htames : ω.Tames J) : ω.Compatible J

Build compatibility from J-invariance and the named tameness predicate.

theorem TauCeti.SymplecticForm.Compatible.tames {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) : ω.Tames J

theorem TauCeti.SymplecticForm.Compatible.invariant_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) : (fun (v w : V) => (ω.toBilinForm v) w) (J.toLinearMap v) (J.toLinearMap w) = (fun (v w : V) => (ω.toBilinForm v) w) v w

theorem TauCeti.SymplecticForm.Invariant.associatedBilinForm_apply_swap {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) : (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap w) = (fun (v w : V) => (ω.toBilinForm v) w) w (J.toLinearMap v)

For a J-invariant form, the associated bilinear form is symmetric pointwise. Only invariance is needed.

theorem TauCeti.SymplecticForm.Compatible.associatedBilinForm_apply_swap {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) : (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap w) = (fun (v w : V) => (ω.toBilinForm v) w) w (J.toLinearMap v)

For a compatible pair, the associated bilinear form is symmetric pointwise.

theorem TauCeti.SymplecticForm.Invariant.associatedBilinForm_isSymm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) : (ω.associatedBilinForm J).IsSymm

For a J-invariant form, the associated bilinear form ω(·, J ·) is symmetric. Only invariance is needed.

theorem TauCeti.SymplecticForm.Compatible.associatedBilinForm_isSymm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) : (ω.associatedBilinForm J).IsSymm

For a compatible pair, the associated bilinear form ω(·, J ·) is symmetric.

theorem TauCeti.SymplecticForm.associatedBilinForm_apply_apply_self_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v : V) : ((ω.associatedBilinForm J) (J.toLinearMap v)) (J.toLinearMap v) = ((ω.associatedBilinForm J) v) v

Applying the almost complex structure to both entries preserves the diagonal of the associated bilinear form.

theorem TauCeti.SymplecticForm.Compatible.associated_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) {v : V} (hv : v ≠ 0) : 0 < (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap v)

theorem TauCeti.IsComplexLinearMap.associatedBilinForm_apply_apply_self_eq {V : Type u_1} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {J₀ : AlmostComplexStructure U} {J : AlmostComplexStructure V} {F : U →ₗ[ℝ] V} {ω : SymplecticForm V} (hF : IsComplexLinearMap J₀ J F) (v : U) : ((ω.associatedBilinForm J) (F (J₀.toLinearMap v))) (F (J₀.toLinearMap v)) = ((ω.associatedBilinForm J) (F v)) (F v)

For a complex-linear map from any complex source, the associated-bilinear-form diagonal of the image of J₀ v equals that of the image of v.

theorem TauCeti.IsComplexLinearMap.associatedBilinForm_apply_self_eq_symplecticForm {V : Type u_1} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {J₀ : AlmostComplexStructure U} {J : AlmostComplexStructure V} {F : U →ₗ[ℝ] V} {ω : SymplecticForm V} (hF : IsComplexLinearMap J₀ J F) (v : U) : ((ω.associatedBilinForm J) (F v)) (F v) = (fun (v w : V) => (ω.toBilinForm v) w) (F v) (F (J₀.toLinearMap v))

For a complex-linear map from any complex source, the associated-bilinear-form diagonal of an image vector is the symplectic area density of the ordered pair (F v, F (J₀ v)).