Pseudoholomorphic maps between almost complex manifolds #
A map u : M → M' between manifolds carrying smooth almost complex structures j and J is
pseudoholomorphic (a J-holomorphic curve, when M is a Riemann surface) at x when it has a
manifold Fréchet derivative there which intertwines the two structures:
du_x ∘ j(x) = J(u x) ∘ du_x. This is the nonlinear Cauchy--Riemann equation, here with a target
structure that genuinely varies over a manifold rather than over a normed space.
Why the name is not IsJHolomorphic #
TauCeti.IsJHolomorphic is already the varying-structure predicate for maps between normed
spaces (TauCeti/Geometry/Symplectic/JHolomorphic/Varying.lean), which is the local coordinate
model of this one, and TauCeti.IsConstStructureJHolomorphic is the flat, single-structure model
below that. The manifold-level predicate therefore takes the equally standard name
pseudoholomorphic (Gromov's term, used interchangeably with J-holomorphic in
McDuff--Salamon). isPseudoholomorphicAt_iff_isJHolomorphicAt below identifies the two on a
model vector space, so the naming records a difference of setting, not of mathematics.
Main declarations #
TauCeti.IsPseudoholomorphicWithinAt,TauCeti.IsPseudoholomorphicAt: the Cauchy--Riemann equation for the derivative within a set, respectively at a point.TauCeti.IsPseudoholomorphicOn,TauCeti.IsPseudoholomorphic: the setwise and global predicates.TauCeti.IsPseudoholomorphicAt.mfderiv_apply_commuteandTauCeti.IsPseudoholomorphicAt.mfderiv_isComplexLinear: the manifold derivative of a pseudoholomorphic map intertwines the two structures, and their within-set analogues.TauCeti.IsPseudoholomorphicAt.comp: pseudoholomorphic maps compose.TauCeti.IsPseudoholomorphicAt.of_comp: a map whose composite with a pseudoholomorphic immersion is pseudoholomorphic is pseudoholomorphic.TauCeti.isPseudoholomorphicAt_neg_neg_iffand its within-set, setwise, and global analogues: reversing both structures changes nothing.TauCeti.isPseudoholomorphicAt_stdComplexLine_iff: for a curve out of the standard complex line the equation reduces to the single coordinate identity∂_t w = J(w) ∂_s w.TauCeti.isPseudoholomorphicAt_iff_isJHolomorphicAtand its within-set, setwise, and global analogues: on model vector spaces the predicate is the normed-space one.TauCeti.isPseudoholomorphicAt_constSmooth_iffand its within-set, setwise, and global analogues: for constant structures on model vector spaces it is the flat, constant-structure predicate.
No regularity beyond the existence of a derivative is imposed: as with the normed-space predicates,
smoothness of u is a separate hypothesis for the results that need it, and taming or compatibility
with a symplectic form is not part of the definition. This keeps the analytic hypotheses unbundled.
The convention follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology,
Section 2.1: the Cauchy--Riemann equation is du ∘ j = J ∘ du.
def
TauCeti.IsPseudoholomorphicWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(u : M → M')
(s : Set M)
(x : M)
:
A map between almost complex manifolds is pseudoholomorphic within a set at a point when it has a manifold derivative within that set intertwining the source structure at the point with the target structure at the image point.
Instances For
def
TauCeti.IsPseudoholomorphicAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(u : M → M')
(x : M)
:
A map between almost complex manifolds is pseudoholomorphic at a point when it has a manifold derivative there intertwining the source structure at the point with the target structure at the image point.
Instances For
def
TauCeti.IsPseudoholomorphicOn
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(u : M → M')
(s : Set M)
:
A map is pseudoholomorphic on a set when it is pseudoholomorphic within that set at each of its points.
Instances For
def
TauCeti.IsPseudoholomorphic
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(u : M → M')
:
A map is pseudoholomorphic when it is pseudoholomorphic at every point.
Instances For
Building and unfolding the predicates #
theorem
TauCeti.isPseudoholomorphicAt_of_hasMFDerivAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
{u' : TangentSpace I x →L[ℝ] TangentSpace I' (u x)}
(hu : HasMFDerivAt% u x u')
(hlin :
∀ (w : TangentSpace I x),
u' ((fun (x : M) => ⇑(j.toEndomorphism x)) x w) = (fun (x : M') => ⇑(J.toEndomorphism x)) (u x) (u' w))
:
IsPseudoholomorphicAt j J u x
Build pseudoholomorphicity at a point from a manifold derivative satisfying the pointwise Cauchy--Riemann equation.
theorem
TauCeti.isPseudoholomorphicWithinAt_of_hasMFDerivWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
{u' : TangentSpace I x →L[ℝ] TangentSpace I' (u x)}
(hu : HasMFDerivAt[s] u x u')
(hlin :
∀ (w : TangentSpace I x),
u' ((fun (x : M) => ⇑(j.toEndomorphism x)) x w) = (fun (x : M') => ⇑(J.toEndomorphism x)) (u x) (u' w))
:
IsPseudoholomorphicWithinAt j J u s x
Build pseudoholomorphicity within a set from a manifold derivative within that set satisfying the pointwise Cauchy--Riemann equation.
theorem
TauCeti.isPseudoholomorphicAt_iff_isComplexLinearMap
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
:
IsPseudoholomorphicAt j J u x ↔ ∃ (u' : TangentSpace I x →L[ℝ] TangentSpace I' (u x)),
HasMFDerivAt% u x u' ∧ IsComplexLinearMap (j.almostComplexStructureAt x) (J.almostComplexStructureAt (u x)) ↑u'
The Cauchy--Riemann equation of the definition says exactly that the derivative is a complex-linear map from the source tangent space at the point to the target tangent space at the image point.
theorem
TauCeti.isPseudoholomorphicWithinAt_iff_isComplexLinearMap
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
:
IsPseudoholomorphicWithinAt j J u s x ↔ ∃ (u' : TangentSpace I x →L[ℝ] TangentSpace I' (u x)),
HasMFDerivAt[s] u x u' ∧ IsComplexLinearMap (j.almostComplexStructureAt x) (J.almostComplexStructureAt (u x)) ↑u'
The within-set Cauchy--Riemann equation of the definition says exactly that the derivative within the set is complex-linear.
theorem
TauCeti.isPseudoholomorphicOn_iff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
:
Restate setwise pseudoholomorphicity as the pointwise within-set condition.
theorem
TauCeti.isPseudoholomorphic_iff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
:
Restate global pseudoholomorphicity as pointwise pseudoholomorphicity everywhere.
theorem
TauCeti.IsPseudoholomorphicAt.hasMFDerivAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
:
HasMFDerivAt% u x (Classical.choose ⋯)
The continuous-linear manifold derivative witnessing pseudoholomorphicity at a point.
theorem
TauCeti.IsPseudoholomorphicAt.derivative_isComplexLinear
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
:
IsComplexLinearMap (j.almostComplexStructureAt x) (J.almostComplexStructureAt (u x)) ↑(Classical.choose ⋯)
The chosen manifold derivative at a pseudoholomorphic point is complex-linear.
theorem
TauCeti.IsPseudoholomorphicWithinAt.hasMFDerivWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
:
HasMFDerivAt[s] u x (Classical.choose ⋯)
The continuous-linear manifold derivative witnessing pseudoholomorphicity within a set.
theorem
TauCeti.IsPseudoholomorphicWithinAt.derivative_isComplexLinear
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
:
IsComplexLinearMap (j.almostComplexStructureAt x) (J.almostComplexStructureAt (u x)) ↑(Classical.choose ⋯)
The chosen within-set manifold derivative is complex-linear.
Differentiability and continuity #
theorem
TauCeti.IsPseudoholomorphicAt.mdifferentiableAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
:
MDiffAt u x
A map pseudoholomorphic at a point is differentiable there.
theorem
TauCeti.IsPseudoholomorphicWithinAt.mdifferentiableWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
:
MDiffAt[s] u x
A map pseudoholomorphic within a set at a point is differentiable within that set.
theorem
TauCeti.IsPseudoholomorphicAt.continuousAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
:
ContinuousAt u x
A map pseudoholomorphic at a point is continuous there.
theorem
TauCeti.IsPseudoholomorphicWithinAt.continuousWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
:
ContinuousWithinAt u s x
A map pseudoholomorphic within a set at a point is continuous within that set.
theorem
TauCeti.IsPseudoholomorphicOn.mdifferentiableOn
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
(hu : IsPseudoholomorphicOn j J u s)
:
MDiff[s] u
A map pseudoholomorphic on a set is differentiable on it.
theorem
TauCeti.IsPseudoholomorphicOn.continuousOn
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
(hu : IsPseudoholomorphicOn j J u s)
:
ContinuousOn u s
A map pseudoholomorphic on a set is continuous on it.
theorem
TauCeti.IsPseudoholomorphic.mdifferentiable
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
(hu : IsPseudoholomorphic j J u)
:
MDiff u
A pseudoholomorphic map is differentiable.
theorem
TauCeti.IsPseudoholomorphic.continuous
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
(hu : IsPseudoholomorphic j J u)
:
A pseudoholomorphic map is continuous.
The Cauchy--Riemann equation for the canonical derivative #
theorem
TauCeti.IsPseudoholomorphicAt.mfderiv_apply_commute
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
(w : TangentSpace I x)
:
(mfderiv% u x) ((fun (x : M) => ⇑(j.toEndomorphism x)) x w) = (fun (x : M') => ⇑(J.toEndomorphism x)) (u x) ((mfderiv% u x) w)
The manifold derivative of a map pseudoholomorphic at a point intertwines the two almost complex structures: this is the nonlinear Cauchy--Riemann equation.
theorem
TauCeti.IsPseudoholomorphicAt.mfderiv_isComplexLinear
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
:
IsComplexLinearMap (j.almostComplexStructureAt x) (J.almostComplexStructureAt (u x)) ↑(mfderiv% u x)
The manifold derivative of a map pseudoholomorphic at a point is complex-linear.
theorem
TauCeti.isPseudoholomorphicAt_iff_mfderiv
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
:
IsPseudoholomorphicAt j J u x ↔ MDiffAt u x ∧ ∀ (w : TangentSpace I x),
(mfderiv% u x) ((fun (x : M) => ⇑(j.toEndomorphism x)) x w) = (fun (x : M') => ⇑(J.toEndomorphism x)) (u x) ((mfderiv% u x) w)
Pseudoholomorphicity at a point is exactly differentiability together with the Cauchy--Riemann equation for the canonical manifold derivative.
theorem
TauCeti.IsPseudoholomorphicWithinAt.mfderivWithin_apply_commute
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
(hs : UniqueMDiffAt[s] x)
(w : TangentSpace I x)
:
(mfderiv[s] u x) ((fun (x : M) => ⇑(j.toEndomorphism x)) x w) = (fun (x : M') => ⇑(J.toEndomorphism x)) (u x) ((mfderiv[s] u x) w)
The derivative within a set of a map pseudoholomorphic there intertwines the two almost complex structures, provided the set has unique manifold derivatives at the point.
theorem
TauCeti.IsPseudoholomorphicWithinAt.mfderivWithin_isComplexLinear
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
(hs : UniqueMDiffAt[s] x)
:
IsComplexLinearMap (j.almostComplexStructureAt x) (J.almostComplexStructureAt (u x)) ↑(mfderiv[s] u x)
The derivative within a set of a map pseudoholomorphic there is complex-linear, provided the set has unique manifold derivatives at the point.
Relations between the four predicates #
theorem
TauCeti.IsPseudoholomorphicAt.isPseudoholomorphicWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicAt j J u x)
:
IsPseudoholomorphicWithinAt j J u s x
A map pseudoholomorphic at a point is pseudoholomorphic within every set there.
theorem
TauCeti.IsPseudoholomorphicWithinAt.isPseudoholomorphicAt_of_mem_nhds
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u s x)
(hs : s ∈ nhds x)
:
IsPseudoholomorphicAt j J u x
Pseudoholomorphicity within a set that is a neighbourhood of the point upgrades to pseudoholomorphicity at the point.
theorem
TauCeti.IsPseudoholomorphicWithinAt.mono
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s t : Set M}
{x : M}
(hu : IsPseudoholomorphicWithinAt j J u t x)
(hst : s ⊆ t)
:
IsPseudoholomorphicWithinAt j J u s x
Pseudoholomorphicity within a set passes to smaller sets.
theorem
TauCeti.IsPseudoholomorphicOn.isPseudoholomorphicWithinAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
(hu : IsPseudoholomorphicOn j J u s)
(hx : x ∈ s)
:
IsPseudoholomorphicWithinAt j J u s x
A map pseudoholomorphic on a set is pseudoholomorphic within that set at each of its points.
theorem
TauCeti.IsPseudoholomorphic.isPseudoholomorphicAt
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
(hu : IsPseudoholomorphic j J u)
(x : M)
:
IsPseudoholomorphicAt j J u x
A pseudoholomorphic map is pseudoholomorphic at every point.
theorem
TauCeti.IsPseudoholomorphicOn.mono
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s t : Set M}
(hu : IsPseudoholomorphicOn j J u t)
(hst : s ⊆ t)
:
IsPseudoholomorphicOn j J u s
Pseudoholomorphicity on a set passes to smaller sets.
theorem
TauCeti.IsPseudoholomorphic.isPseudoholomorphicOn
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
(hu : IsPseudoholomorphic j J u)
(s : Set M)
:
IsPseudoholomorphicOn j J u s
A pseudoholomorphic map is pseudoholomorphic on every set.
@[simp]
theorem
TauCeti.isPseudoholomorphicWithinAt_univ
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
:
Pseudoholomorphicity within the whole space is pseudoholomorphicity at the point.
@[simp]
theorem
TauCeti.isPseudoholomorphicOn_univ
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
:
Pseudoholomorphicity on the whole space is global pseudoholomorphicity.
The identity, constants, and composition #
@[simp]
theorem
TauCeti.isPseudoholomorphicAt_id
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(j : SmoothAlmostComplexStructure I M)
(x : M)
:
IsPseudoholomorphicAt j j id x
The identity map is pseudoholomorphic at every point, for every smooth almost complex structure.
@[simp]
theorem
TauCeti.isPseudoholomorphicWithinAt_id
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(j : SmoothAlmostComplexStructure I M)
(s : Set M)
(x : M)
:
IsPseudoholomorphicWithinAt j j id s x
The identity map is pseudoholomorphic within every set at every point.
@[simp]
theorem
TauCeti.isPseudoholomorphicOn_id
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(j : SmoothAlmostComplexStructure I M)
(s : Set M)
:
IsPseudoholomorphicOn j j id s
The identity map is pseudoholomorphic on every set.
@[simp]
theorem
TauCeti.isPseudoholomorphic_id
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
(j : SmoothAlmostComplexStructure I M)
:
The identity map is pseudoholomorphic.
@[simp]
theorem
TauCeti.isPseudoholomorphicAt_const
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(c : M')
(x : M)
:
IsPseudoholomorphicAt j J (fun (x : M) => c) x
A constant map is pseudoholomorphic at every point, for arbitrary source and target structures.
@[simp]
theorem
TauCeti.isPseudoholomorphicWithinAt_const
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(c : M')
(s : Set M)
(x : M)
:
IsPseudoholomorphicWithinAt j J (fun (x : M) => c) s x
A constant map is pseudoholomorphic within every set at every point.
@[simp]
theorem
TauCeti.isPseudoholomorphicOn_const
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(c : M')
(s : Set M)
:
IsPseudoholomorphicOn j J (fun (x : M) => c) s
A constant map is pseudoholomorphic on every set.
@[simp]
theorem
TauCeti.isPseudoholomorphic_const
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(j : SmoothAlmostComplexStructure I M)
(J : SmoothAlmostComplexStructure I' M')
(c : M')
:
IsPseudoholomorphic j J fun (x : M) => c
A constant map is pseudoholomorphic.
theorem
TauCeti.IsPseudoholomorphicAt.comp
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{E'' : Type u_7}
{H'' : Type u_8}
{M'' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
[TopologicalSpace H'']
{I'' : ModelWithCorners ℝ E'' H''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[IsManifold I'' (↑⊤) M'']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{K : SmoothAlmostComplexStructure I'' M''}
{u : M → M'}
{v : M' → M''}
{x : M}
(hv : IsPseudoholomorphicAt J K v (u x))
(hu : IsPseudoholomorphicAt j J u x)
:
IsPseudoholomorphicAt j K (v ∘ u) x
The composition of pseudoholomorphic maps is pseudoholomorphic at a point: the chain rule for the nonlinear Cauchy--Riemann equation.
theorem
TauCeti.IsPseudoholomorphicAt.of_comp
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{E'' : Type u_7}
{H'' : Type u_8}
{M'' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
[TopologicalSpace H'']
{I'' : ModelWithCorners ℝ E'' H''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[IsManifold I'' (↑⊤) M'']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{K : SmoothAlmostComplexStructure I'' M''}
{u : M → M'}
{v : M' → M''}
{x : M}
(hvu : IsPseudoholomorphicAt j K (v ∘ u) x)
(hv : IsPseudoholomorphicAt J K v (u x))
(hinj : Function.Injective ⇑(mfderiv% v (u x)))
(hu : MDiffAt u x)
:
IsPseudoholomorphicAt j J u x
A map whose composite with a pseudoholomorphic map of injective differential is pseudoholomorphic is itself pseudoholomorphic: the Cauchy--Riemann equation lifts through an immersion.
theorem
TauCeti.IsPseudoholomorphicWithinAt.comp
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{E'' : Type u_7}
{H'' : Type u_8}
{M'' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
[TopologicalSpace H'']
{I'' : ModelWithCorners ℝ E'' H''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[IsManifold I'' (↑⊤) M'']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{K : SmoothAlmostComplexStructure I'' M''}
{u : M → M'}
{v : M' → M''}
{s : Set M}
{x : M}
{r : Set M'}
(hv : IsPseudoholomorphicWithinAt J K v r (u x))
(hu : IsPseudoholomorphicWithinAt j J u s x)
(hst : Set.MapsTo u s r)
:
IsPseudoholomorphicWithinAt j K (v ∘ u) s x
The composition of pseudoholomorphic maps is pseudoholomorphic within a set at a point.
theorem
TauCeti.IsPseudoholomorphicOn.comp
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{E'' : Type u_7}
{H'' : Type u_8}
{M'' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
[TopologicalSpace H'']
{I'' : ModelWithCorners ℝ E'' H''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[IsManifold I'' (↑⊤) M'']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{K : SmoothAlmostComplexStructure I'' M''}
{u : M → M'}
{v : M' → M''}
{s : Set M}
{r : Set M'}
(hv : IsPseudoholomorphicOn J K v r)
(hu : IsPseudoholomorphicOn j J u s)
(hst : Set.MapsTo u s r)
:
IsPseudoholomorphicOn j K (v ∘ u) s
The composition of pseudoholomorphic maps is pseudoholomorphic on the source set.
theorem
TauCeti.IsPseudoholomorphic.comp
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{E'' : Type u_7}
{H'' : Type u_8}
{M'' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
[TopologicalSpace H'']
{I'' : ModelWithCorners ℝ E'' H''}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[IsManifold I'' (↑⊤) M'']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{K : SmoothAlmostComplexStructure I'' M''}
{u : M → M'}
{v : M' → M''}
(hv : IsPseudoholomorphic J K v)
(hu : IsPseudoholomorphic j J u)
:
IsPseudoholomorphic j K (v ∘ u)
The composition of pseudoholomorphic maps is pseudoholomorphic.
Reversing the structures #
@[simp]
theorem
TauCeti.isPseudoholomorphicWithinAt_neg_neg_iff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
{x : M}
:
Reversing both almost complex structures preserves pseudoholomorphicity within a set: a map is
(j, J)-holomorphic there exactly when it is (-j, -J)-holomorphic.
@[simp]
theorem
TauCeti.isPseudoholomorphicAt_neg_neg_iff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{x : M}
:
Reversing both almost complex structures preserves pseudoholomorphicity: a map is
(j, J)-holomorphic exactly when it is (-j, -J)-holomorphic.
@[simp]
theorem
TauCeti.isPseudoholomorphicOn_neg_neg_iff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
{s : Set M}
:
Reversing both almost complex structures preserves pseudoholomorphicity on a set.
@[simp]
theorem
TauCeti.isPseudoholomorphic_neg_neg_iff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{j : SmoothAlmostComplexStructure I M}
{J : SmoothAlmostComplexStructure I' M'}
{u : M → M'}
:
Reversing both almost complex structures preserves global pseudoholomorphicity.
Curves from the standard complex line #
theorem
TauCeti.isPseudoholomorphicAt_stdComplexLine_iff
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
(J : SmoothAlmostComplexStructure I' M')
(w : ℝ × ℝ → M')
(z : ℝ × ℝ)
:
IsPseudoholomorphicAt (SmoothAlmostComplexStructure.product ℝ) J w z ↔ ∃ (w' : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ)) z →L[ℝ] TangentSpace I' (w z)),
HasMFDerivAt% w z w' ∧ w' stdComplexLineImag = (fun (x : M') => ⇑(J.toEndomorphism x)) (w z) (w' stdComplexLineReal)
A curve from the standard complex line -- that is, ℝ × ℝ with the smooth almost complex
structure SmoothAlmostComplexStructure.product ℝ -- into an almost complex manifold is
pseudoholomorphic at a point exactly when it has a manifold derivative there satisfying the
single coordinate Cauchy--Riemann equation ∂_t w = J(w) ∂_s w. This is the classical form of
the equation for a J-holomorphic curve.
theorem
TauCeti.IsPseudoholomorphicAt.mfderiv_stdComplexLineImag
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{J : SmoothAlmostComplexStructure I' M'}
{w : ℝ × ℝ → M'}
{z : ℝ × ℝ}
(hw : IsPseudoholomorphicAt (SmoothAlmostComplexStructure.product ℝ) J w z)
:
(mfderiv% w z) stdComplexLineImag = (fun (x : M') => ⇑(J.toEndomorphism x)) (w z) ((mfderiv% w z) stdComplexLineReal)
The manifold derivative of a J-holomorphic curve from the standard complex line sends the
imaginary coordinate vector to J applied to the image of the real coordinate vector.
Comparison with the normed-space predicates #
theorem
TauCeti.isPseudoholomorphicAt_iff_isJHolomorphicAt
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(j : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V)
(J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ W) W)
(u : V → W)
(x : V)
:
On model vector spaces, pseudoholomorphicity at a point is the varying-structure predicate for maps between normed spaces, applied to the pointwise almost complex structures on the tangent spaces.
theorem
TauCeti.isPseudoholomorphicWithinAt_iff_isJHolomorphicWithinAt
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(j : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V)
(J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ W) W)
(u : V → W)
(s : Set V)
(x : V)
:
On model vector spaces, pseudoholomorphicity within a set at a point is the varying-structure predicate for maps between normed spaces.
theorem
TauCeti.isPseudoholomorphicOn_iff_isJHolomorphicOn
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(j : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V)
(J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ W) W)
(u : V → W)
(s : Set V)
:
On model vector spaces, pseudoholomorphicity on a set is the varying-structure predicate for maps between normed spaces.
theorem
TauCeti.isPseudoholomorphic_iff_isJHolomorphic
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(j : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V)
(J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ W) W)
(u : V → W)
:
On model vector spaces, pseudoholomorphicity is the varying-structure predicate for maps between normed spaces.
@[simp]
theorem
TauCeti.isPseudoholomorphicAt_constSmooth_iff
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
[FiniteDimensional ℝ V]
[FiniteDimensional ℝ W]
(Jv : AlmostComplexStructure V)
(Jw : AlmostComplexStructure W)
(u : V → W)
(x : V)
:
For the constant smooth structures of two pointwise almost complex structures on model vector spaces, pseudoholomorphicity at a point is the flat, constant-structure predicate. This is the check that the manifold-level Cauchy--Riemann equation restricts to the linear one.
@[simp]
theorem
TauCeti.isPseudoholomorphicWithinAt_constSmooth_iff
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
[FiniteDimensional ℝ V]
[FiniteDimensional ℝ W]
(Jv : AlmostComplexStructure V)
(Jw : AlmostComplexStructure W)
(u : V → W)
(s : Set V)
(x : V)
:
IsPseudoholomorphicWithinAt Jv.constSmooth Jw.constSmooth u s x ↔ IsConstStructureJHolomorphicWithinAt Jv Jw u s x
For the constant smooth structures of two pointwise almost complex structures on model vector spaces, pseudoholomorphicity within a set at a point is the flat, constant-structure predicate.
@[simp]
theorem
TauCeti.isPseudoholomorphicOn_constSmooth_iff
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
[FiniteDimensional ℝ V]
[FiniteDimensional ℝ W]
(Jv : AlmostComplexStructure V)
(Jw : AlmostComplexStructure W)
(u : V → W)
(s : Set V)
:
For the constant smooth structures of two pointwise almost complex structures on model vector spaces, pseudoholomorphicity on a set is the flat, constant-structure predicate.
@[simp]
theorem
TauCeti.isPseudoholomorphic_constSmooth_iff
{V : Type u_10}
{W : Type u_11}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
[FiniteDimensional ℝ V]
[FiniteDimensional ℝ W]
(Jv : AlmostComplexStructure V)
(Jw : AlmostComplexStructure W)
(u : V → W)
:
For the constant smooth structures of two pointwise almost complex structures on model vector spaces, global pseudoholomorphicity is the flat, constant-structure predicate.