Documentation

TauCeti.Geometry.Symplectic.Finrank

An almost complex structure forces even real dimension #

A pointwise almost complex structure J on a real module V turns V into a complex vector space (TauCeti.AlmostComplexStructure.complexModule), where multiplication by i is J. Since ℂ is a degree-two extension of ℝ, the tower law forces the real dimension of V to be twice its complex dimension, hence even. This is the classical fact that a manifold (or vector bundle) admitting an almost complex structure is even-dimensional (McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1), recorded here at the pointwise linear-algebra level.

The tower-law identities are stated without a finite-dimensionality hypothesis: Module.finrank_mul_finrank holds for Module.finrank unconditionally (an infinite-dimensional V has Module.finrank ℝ V = 0 = 2 * 0), so the identities below need no FiniteDimensional assumption.

Main declarations #

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

source
noncomputable def TauCeti.AlmostComplexStructure.complexFinrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) :
ℕ

The complex dimension of V with respect to an almost complex structure J: the ℂ-dimension of V under the complex module structure induced by J (AlmostComplexStructure.complexModule).

Instances For
    source
    @[simp]
    theorem TauCeti.AlmostComplexStructure.complexFinrank_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) :
    J.complexFinrank = Module.finrank ℂ V

    The complex dimension of J is the ℂ-dimension of V under the induced complex structure.

    source
    theorem TauCeti.AlmostComplexStructure.finrank_real_eq_two_mul_complexFinrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) :
    Module.finrank ℝ V = 2 * J.complexFinrank

    The real dimension of a module carrying an almost complex structure J is twice its complex dimension: finrank ℝ V = 2 * J.complexFinrank. This is the tower law finrank ℝ V = finrank ℝ ℂ * finrank ℂ V together with finrank ℝ ℂ = 2.

    source
    theorem TauCeti.AlmostComplexStructure.even_finrank_real {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) :
    Even (Module.finrank ℝ V)

    The real dimension of a module carrying an almost complex structure is even.

    source
    theorem TauCeti.AlmostComplexStructure.even_finrank_of_forall_mem {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {p : Submodule ℝ V} (hp : ∀ v ∈ p, J.toLinearMap v ∈ p) :
    Even (Module.finrank ℝ ↥p)

    A real subspace invariant under an almost complex structure has even real dimension: J restricts to an almost complex structure on it.

    source
    theorem TauCeti.AlmostComplexStructure.even_finrank_genEigenspace_zero_of_anticommute {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {f : Module.End ℝ V} (h : f * J.toLinearMap + J.toLinearMap * f = 0) (k : ℕ∞) :
    Even (Module.finrank ℝ ↥((f.genEigenspace 0) k))

    If an endomorphism f anticommutes with an almost complex structure J, then its generalized 0-eigenspaces, in particular its kernel, are J-invariant and therefore have even real dimension.

    source
    theorem TauCeti.AlmostComplexStructure.finrank_eq_complexFinrank_of_isMaximalTotallyReal {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {L : Submodule ℝ V} (hL : IsMaximalTotallyReal J.toLinearMap L) :
    Module.finrank ℝ ↥L = J.complexFinrank

    A maximal totally real subspace L of an almost complex module has real dimension equal to the complex dimension of the ambient module: L is "half-dimensional". (An infinite-dimensional module has both dimensions 0, since L and J L span it.)

    For a Heegaard diagram of genus g, this is the statement that the totally real tori T_α, T_β are g-dimensional inside the g-complex-dimensional symmetric product Sym^g(Σ) (Ozsváth--Szabó, arXiv:math/0101206, Section 2).

    source
    theorem TauCeti.AlmostComplexStructure.isEmpty_of_odd_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] (h : Odd (Module.finrank ℝ V)) :
    IsEmpty (AlmostComplexStructure V)

    An odd-dimensional real module admits no almost complex structure.

    source
    theorem TauCeti.AlmostComplexStructure.span_pair_eq_top_of_finrank_eq_two {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (hV : Module.finrank ℝ V = 2) {v : V} (hv : v ≠ 0) :
    Submodule.span ℝ {v, J.toLinearMap v} = ⊤

    On a two-dimensional real module carrying an almost complex structure J, every nonzero vector v and its image J v span the module.

    source
    theorem TauCeti.AlmostComplexStructure.span_pair_eq_top_of_finrank_le_two {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (J : AlmostComplexStructure V) (hV : Module.finrank ℝ V ≤ 2) {v : V} (hv : v ≠ 0) :
    Submodule.span ℝ {v, J.toLinearMap v} = ⊤

    On a finite-dimensional real module of dimension at most two carrying an almost complex structure J, every nonzero vector v and its image J v span the module.

    source
    theorem TauCeti.AlmostComplexStructure.bilin_eq_zero_of_finrank_le_two {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (J : AlmostComplexStructure V) (hV : Module.finrank ℝ V ≤ 2) {W : Type u_2} [AddCommGroup W] [Module ℝ W] {B : V →ₗ[ℝ] V →ₗ[ℝ] W} (hself : ∀ (v : V), (B v) v = 0) (hJ : ∀ (v : V), (B v) (J.toLinearMap v) = 0) :
    B = 0

    On a finite-dimensional real module of dimension at most two carrying an almost complex structure J, any bilinear map vanishing on (v, v) and (v, J v) for every v vanishes identically.

    source
    theorem TauCeti.AlmostComplexStructure.bilin_eq_zero_of_finrank_eq_two {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (hV : Module.finrank ℝ V = 2) {W : Type u_2} [AddCommGroup W] [Module ℝ W] {B : V →ₗ[ℝ] V →ₗ[ℝ] W} (hself : ∀ (v : V), (B v) v = 0) (hJ : ∀ (v : V), (B v) (J.toLinearMap v) = 0) :
    B = 0

    On a two-dimensional real module carrying an almost complex structure J, any bilinear map vanishing on (v, v) and (v, J v) for every v vanishes identically.