The standard complex line as a source for constant-structure J-holomorphic maps

This file records the elementary Cauchy--Riemann bookkeeping for maps whose source is the standard complex line, represented as ℝ × ℝ with the almost complex structure AlmostComplexStructure.product ℝ, (s, t) ↦ (-t, s).

For a real-linear map out of this source, complex-linearity says exactly that the image of the imaginary coordinate vector is J applied to the image of the real coordinate vector. Thus the linear map, and in particular the Frechet derivative of a constant-structure J-holomorphic map from the standard line, is determined by its s-direction.

The area estimates show that, under a taming form, the symplectic area of the ordered pair (∂s u, ∂t u) is nonnegative, and it is positive when ∂s u is nonzero. These pointwise linear-algebra statements supply the local calculus for holomorphic-curve energy and elliptic estimates.

Main declarations

• TauCeti.stdComplexLineReal and TauCeti.stdComplexLineImag: the coordinate vectors (1, 0) and (0, 1) in the standard complex line.
• TauCeti.equivRealProdCLM_symm_stdComplexLineReal and TauCeti.equivRealProdCLM_symm_stdComplexLineImag: under Complex.equivRealProdCLM they are the complex numbers 1 and i; conversely TauCeti.equivRealProdCLM_one and TauCeti.equivRealProdCLM_I.
• TauCeti.fderiv_comp_equivRealProdCLM_one and TauCeti.fderiv_comp_equivRealProdCLM_I: read in the complex coordinate, the derivatives in the directions 1 and i are ∂s and ∂t.
• LinearMap.apply_stdComplexLine: a real-linear map is determined by its values on the coordinate vectors.
• TauCeti.isComplexLinearMap_stdComplexLine_iff: complex-linearity out of the standard complex line is equivalent to the coordinate Cauchy--Riemann equation F (0, 1) = J (F (1, 0)).
• TauCeti.IsComplexLinearMap.apply_stdComplexLineImag: for a complex-linear map F : ℝ × ℝ →ₗ[ℝ] V, F (0, 1) = J (F (1, 0)).
• TauCeti.IsComplexLinearMap.apply_stdComplexLine: such an F is determined by F (1, 0), via F (s, t) = s • v + t • J v.
• TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineImag and TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLine_apply: the corresponding statements for Frechet derivatives of constant-structure J-holomorphic maps.
• TauCeti.IsComplexLinearMap.symplecticForm_apply_apply_*: nonnegativity and positivity of ω(F v, F (J v)) for a complex-linear map under tameness.
• TauCeti.IsComplexLinearMap.symplecticForm_apply_stdComplexLineReal_stdComplexLineImag_*: nonnegativity and positivity of ω(F ∂s, F ∂t) under tameness.

The Cauchy--Riemann sign convention matches McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1: du ∘ j = J ∘ du.

def TauCeti.stdComplexLineReal : ℝ × ℝ

The real coordinate vector (1, 0) in the standard complex line ℝ × ℝ.

def TauCeti.stdComplexLineImag : ℝ × ℝ

The imaginary coordinate vector (0, 1) in the standard complex line ℝ × ℝ.

theorem TauCeti.stdComplexLineReal_eq : stdComplexLineReal = (1, 0)

The real coordinate vector is the standard pair (1, 0).

theorem TauCeti.stdComplexLineImag_eq : stdComplexLineImag = (0, 1)

The imaginary coordinate vector is the standard pair (0, 1).

@[simp]

theorem TauCeti.stdComplexLineReal_fst : stdComplexLineReal.1 = 1

@[simp]

theorem TauCeti.stdComplexLineReal_snd : stdComplexLineReal.2 = 0

@[simp]

theorem TauCeti.stdComplexLineImag_fst : stdComplexLineImag.1 = 0

@[simp]

theorem TauCeti.stdComplexLineImag_snd : stdComplexLineImag.2 = 1

@[simp]

theorem TauCeti.equivRealProdCLM_symm_stdComplexLineReal : Complex.equivRealProdCLM.symm stdComplexLineReal = 1

The real coordinate vector of ℝ × ℝ is the complex number 1.

@[simp]

theorem TauCeti.equivRealProdCLM_symm_stdComplexLineImag : Complex.equivRealProdCLM.symm stdComplexLineImag = Complex.I

The imaginary coordinate vector of ℝ × ℝ is the complex number i.

theorem TauCeti.equivRealProdCLM_one : Complex.equivRealProdCLM 1 = stdComplexLineReal

The complex number 1 is the real coordinate vector of ℝ × ℝ.

theorem TauCeti.equivRealProdCLM_I : Complex.equivRealProdCLM Complex.I = stdComplexLineImag

The complex number i is the imaginary coordinate vector of ℝ × ℝ.

theorem TauCeti.fderiv_comp_equivRealProdCLM_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : ℝ × ℝ → E) (y : ℂ) : (fderiv ℝ (u ∘ ⇑Complex.equivRealProdCLM) y) 1 = (fderiv ℝ u (Complex.equivRealProdCLM y)) stdComplexLineReal

In the complex coordinate Complex.equivRealProdCLM, the derivative of u in the direction 1 is its derivative ∂s u in the real coordinate direction.

theorem TauCeti.fderiv_comp_equivRealProdCLM_I {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : ℝ × ℝ → E) (y : ℂ) : (fderiv ℝ (u ∘ ⇑Complex.equivRealProdCLM) y) Complex.I = (fderiv ℝ u (Complex.equivRealProdCLM y)) stdComplexLineImag

In the complex coordinate Complex.equivRealProdCLM, the derivative of u in the direction i is its derivative ∂t u in the imaginary coordinate direction.

theorem TauCeti.AlmostComplexStructure.product_apply_stdComplexLineReal : (product ℝ).toLinearMap stdComplexLineReal = stdComplexLineImag

theorem TauCeti.AlmostComplexStructure.product_apply_stdComplexLineImag : (product ℝ).toLinearMap stdComplexLineImag = -stdComplexLineReal

theorem TauCeti.stdComplexLine_eq_smul_real_add_smul_imag (z : ℝ × ℝ) : z = z.1 • stdComplexLineReal + z.2 • stdComplexLineImag

Every vector in ℝ × ℝ decomposes in the standard real and imaginary coordinate vectors.

theorem LinearMap.apply_stdComplexLine {V : Type u_2} [AddCommGroup V] [Module ℝ V] (F : ℝ × ℝ →ₗ[ℝ] V) (z : ℝ × ℝ) : F z = z.1 • F TauCeti.stdComplexLineReal + z.2 • F TauCeti.stdComplexLineImag

A real-linear map out of ℝ × ℝ is determined by its values on the real and imaginary coordinate vectors.

theorem TauCeti.isComplexLinearMap_stdComplexLine_iff {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} (F : ℝ × ℝ →ₗ[ℝ] V) : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F ↔ F stdComplexLineImag = J.toLinearMap (F stdComplexLineReal)

Complex-linearity for a real-linear map out of the standard complex line is exactly the coordinate Cauchy--Riemann equation F(0,1) = J(F(1,0)).

theorem TauCeti.IsComplexLinearMap.symplecticForm_apply_apply_nonneg {U : Type u_1} [AddCommGroup U] [Module ℝ U] {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J₀ : AlmostComplexStructure U} {J : AlmostComplexStructure V} {F₀ : U →ₗ[ℝ] V} {ω : SymplecticForm V} (hF : IsComplexLinearMap J₀ J F₀) (hω : ω.Tames J) (v : U) : 0 ≤ (fun (v w : V) => (ω.toBilinForm v) w) (F₀ v) (F₀ (J₀.toLinearMap v))

Under tameness, the pointwise symplectic area of a complex-linear image of (v, J₀ v) is nonnegative.

theorem TauCeti.IsComplexLinearMap.symplecticForm_apply_apply_pos {U : Type u_1} [AddCommGroup U] [Module ℝ U] {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J₀ : AlmostComplexStructure U} {J : AlmostComplexStructure V} {F₀ : U →ₗ[ℝ] V} {ω : SymplecticForm V} (hF : IsComplexLinearMap J₀ J F₀) (hω : ω.Tames J) {v : U} (hv : F₀ v ≠ 0) : 0 < (fun (v w : V) => (ω.toBilinForm v) w) (F₀ v) (F₀ (J₀.toLinearMap v))

Under tameness, the pointwise symplectic area of a complex-linear image of (v, J₀ v) is positive when the image of v is nonzero.

theorem TauCeti.IsComplexLinearMap.of_apply_stdComplexLineImag {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : F stdComplexLineImag = J.toLinearMap (F stdComplexLineReal)) : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F

A real-linear map out of the standard complex line is complex-linear when it satisfies the coordinate Cauchy--Riemann equation F(0,1) = J(F(1,0)).

theorem TauCeti.IsComplexLinearMap.apply_stdComplexLineImag {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) : F stdComplexLineImag = J.toLinearMap (F stdComplexLineReal)

For a complex-linear map from the standard complex line, the imaginary coordinate derivative is J applied to the real coordinate derivative.

theorem TauCeti.IsComplexLinearMap.apply_stdComplexLineReal {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) : F stdComplexLineReal = -J.toLinearMap (F stdComplexLineImag)

The real coordinate derivative is -J applied to the imaginary coordinate derivative.

theorem TauCeti.IsComplexLinearMap.apply_stdComplexLine {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) (z : ℝ × ℝ) : F z = z.1 • F stdComplexLineReal + z.2 • J.toLinearMap (F stdComplexLineReal)

A complex-linear map out of the standard complex line is determined by its real-coordinate value: F (s, t) = s • F(1,0) + t • J(F(1,0)).

theorem TauCeti.IsComplexLinearMap.eq_zero_iff_apply_stdComplexLineReal {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) : F = 0 ↔ F stdComplexLineReal = 0

A complex-linear map from the standard complex line is zero exactly when its real-coordinate value is zero.

theorem TauCeti.IsComplexLinearMap.apply_stdComplexLineReal_ne_zero {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) (hFne : F ≠ 0) : F stdComplexLineReal ≠ 0

The real-coordinate value of a nonzero complex-linear map from the standard complex line is nonzero.

theorem TauCeti.IsComplexLinearMap.symplecticForm_apply_stdComplexLineReal_stdComplexLineImag_nonneg {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} {ω : SymplecticForm V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) (hω : ω.Tames J) : 0 ≤ (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag)

Under tameness, the pointwise symplectic area of a complex-linear image of the standard oriented coordinate pair is nonnegative.

theorem TauCeti.IsComplexLinearMap.symplecticForm_apply_stdComplexLineReal_stdComplexLineImag_pos {V : Type u_2} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {F : ℝ × ℝ →ₗ[ℝ] V} {ω : SymplecticForm V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) (hω : ω.Tames J) (hreal : F stdComplexLineReal ≠ 0) : 0 < (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag)

Under tameness, the pointwise symplectic area of a complex-linear image of the standard oriented coordinate pair is positive if the real-coordinate image is nonzero.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineImag {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {J' : AlmostComplexStructure W} {f : ℝ × ℝ → W} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicAt (AlmostComplexStructure.product ℝ) J' f x) : (fderiv ℝ f x) stdComplexLineImag = J'.toLinearMap ((fderiv ℝ f x) stdComplexLineReal)

For a constant-structure J-holomorphic map from the standard complex line, the Frechet derivative in the imaginary coordinate direction is J applied to the derivative in the real coordinate direction.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLine_apply {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {J' : AlmostComplexStructure W} {f : ℝ × ℝ → W} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicAt (AlmostComplexStructure.product ℝ) J' f x) (z : ℝ × ℝ) : (fderiv ℝ f x) z = z.1 • (fderiv ℝ f x) stdComplexLineReal + z.2 • J'.toLinearMap ((fderiv ℝ f x) stdComplexLineReal)

The Frechet derivative of a constant-structure J-holomorphic map from the standard complex line is determined by its real-coordinate value.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineImag {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {J' : AlmostComplexStructure W} {f : ℝ × ℝ → W} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicWithinAt (AlmostComplexStructure.product ℝ) J' f s x) (hs : UniqueDiffWithinAt ℝ s x) : (fderivWithin ℝ f s x) stdComplexLineImag = J'.toLinearMap ((fderivWithin ℝ f s x) stdComplexLineReal)

For a within-set constant-structure J-holomorphic map from the standard complex line, the Frechet derivative within the set sends the imaginary coordinate direction to J applied to the real direction, provided derivatives within the set are unique.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLine_apply {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {J' : AlmostComplexStructure W} {f : ℝ × ℝ → W} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicWithinAt (AlmostComplexStructure.product ℝ) J' f s x) (hs : UniqueDiffWithinAt ℝ s x) (z : ℝ × ℝ) : (fderivWithin ℝ f s x) z = z.1 • (fderivWithin ℝ f s x) stdComplexLineReal + z.2 • J'.toLinearMap ((fderivWithin ℝ f s x) stdComplexLineReal)

The within-set Frechet derivative of a constant-structure J-holomorphic map from the standard complex line is determined by its real-coordinate value when derivatives within the set are unique.