J-holomorphic maps for varying almost complex structures

This file defines J-holomorphic maps between real normed spaces equipped with point-dependent almost complex structures. At x, the Cauchy--Riemann equation is dfₓ ∘ J(x) = J'(f(x)) ∘ dfₓ; in particular, the target structure is evaluated at the image point. This is the local-coordinate model for J-holomorphic curves in Lane F2.1 of the analytic Heegaard Floer roadmap.

The almost complex structures remain unbundled functions. No regularity is imposed on them by the definition: continuity or smoothness belongs among the separate hypotheses of analytic results that need it. The existing constant-structure API is recovered by specializing both functions to constants.

Main declarations

• TauCeti.IsJHolomorphicAt: J-holomorphicity at a point for varying structures.
• TauCeti.IsJHolomorphicWithinAt: the corresponding within-set predicate.
• TauCeti.IsJHolomorphicOn and TauCeti.IsJHolomorphic: setwise and global predicates.
• TauCeti.IsJHolomorphicAt.comp: composition of J-holomorphic maps.

The within-set predicate carries the same two structural lemmas as the constant-structure one: IsJHolomorphicWithinAt.mono shrinks the set and isJHolomorphicWithinAt_univ identifies the Set.univ case with IsJHolomorphicAt. IsJHolomorphicOn.mono and isJHolomorphicOn_univ follow from them pointwise.

The convention follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1.

def TauCeti.IsJHolomorphicAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (x : U) : Prop

A map is J-holomorphic at a point when it has a Fréchet derivative there which intertwines the source structure at that point with the target structure at the image point.

Equations

• TauCeti.IsJHolomorphicAt J J' f x = TauCeti.IsConstStructureJHolomorphicAt (J x) (J' (f x)) f x

def TauCeti.IsJHolomorphicWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (s : Set U) (x : U) : Prop

A map is J-holomorphic within a set at a point when its derivative within the set intertwines the structures at that point and its image.

Equations

• TauCeti.IsJHolomorphicWithinAt J J' f s x = TauCeti.IsConstStructureJHolomorphicWithinAt (J x) (J' (f x)) f s x

def TauCeti.IsJHolomorphicOn {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (s : Set U) : Prop

A map is J-holomorphic on a set when it is J-holomorphic within that set at every point of the set.

Equations

• TauCeti.IsJHolomorphicOn J J' f s = ∀ x ∈ s, TauCeti.IsJHolomorphicWithinAt J J' f s x

def TauCeti.IsJHolomorphic {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) : Prop

A map is globally J-holomorphic when it is J-holomorphic at every point.

Equations

• TauCeti.IsJHolomorphic J J' f = ∀ (x : U), TauCeti.IsJHolomorphicAt J J' f x

theorem TauCeti.isJHolomorphicAt_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (x : U) : IsJHolomorphicAt J J' f x ↔ ∃ (f' : U →L[ℝ] V), HasFDerivAt f f' x ∧ IsComplexLinearMap (J x) (J' (f x)) ↑f'

Restate pointwise J-holomorphicity as the existence of a complex-linear derivative.

theorem TauCeti.isJHolomorphicWithinAt_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (s : Set U) (x : U) : IsJHolomorphicWithinAt J J' f s x ↔ ∃ (f' : U →L[ℝ] V), HasFDerivWithinAt f f' s x ∧ IsComplexLinearMap (J x) (J' (f x)) ↑f'

Restate within-set J-holomorphicity as the existence of a complex-linear derivative within the set.

theorem TauCeti.isJHolomorphicOn_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (s : Set U) : IsJHolomorphicOn J J' f s ↔ ∀ x ∈ s, IsJHolomorphicWithinAt J J' f s x

Restate setwise J-holomorphicity as the pointwise within-set condition.

theorem TauCeti.isJHolomorphic_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) : IsJHolomorphic J J' f ↔ ∀ (x : U), IsJHolomorphicAt J J' f x

Restate global J-holomorphicity as pointwise J-holomorphicity everywhere.

theorem TauCeti.isJHolomorphicAt_of_hasFDerivAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x : U} {f' : U →L[ℝ] V} (hf : HasFDerivAt f f' x) (hlin : IsComplexLinearMap (J x) (J' (f x)) ↑f') : IsJHolomorphicAt J J' f x

Build pointwise J-holomorphicity from a complex-linear Fréchet derivative.

theorem TauCeti.isJHolomorphicWithinAt_of_hasFDerivWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} {f' : U →L[ℝ] V} (hf : HasFDerivWithinAt f f' s x) (hlin : IsComplexLinearMap (J x) (J' (f x)) ↑f') : IsJHolomorphicWithinAt J J' f s x

Build within-set J-holomorphicity from a complex-linear derivative within the set.

theorem TauCeti.IsJHolomorphicAt.hasFDerivAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x : U} (hf : IsJHolomorphicAt J J' f x) : HasFDerivAt f (Classical.choose ⋯) x

The continuous-linear derivative witnessing J-holomorphicity at a point.

theorem TauCeti.IsJHolomorphicAt.derivative_isComplexLinear {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x : U} (hf : IsJHolomorphicAt J J' f x) : IsComplexLinearMap (J x) (J' (f x)) ↑(Classical.choose ⋯)

The chosen derivative at a J-holomorphic point is complex-linear.

theorem TauCeti.IsJHolomorphicAt.differentiableAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x : U} (hf : IsJHolomorphicAt J J' f x) : DifferentiableAt ℝ f x

A J-holomorphic map at a point is differentiable there.

theorem TauCeti.IsJHolomorphicWithinAt.hasFDerivWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f s x) : HasFDerivWithinAt f (Classical.choose ⋯) s x

The continuous-linear derivative witnessing within-set J-holomorphicity.

theorem TauCeti.IsJHolomorphicWithinAt.differentiableWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f s x) : DifferentiableWithinAt ℝ f s x

A map J-holomorphic within a set at a point is differentiable within that set.

theorem TauCeti.IsJHolomorphicAt.continuousAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x : U} (hf : IsJHolomorphicAt J J' f x) : ContinuousAt f x

A J-holomorphic map at a point is continuous there.

theorem TauCeti.IsJHolomorphicWithinAt.continuousWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f s x) : ContinuousWithinAt f s x

A map J-holomorphic within a set at a point is continuous within that set.

theorem TauCeti.IsJHolomorphicAt.fderiv_isComplexLinear {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x : U} (hf : IsJHolomorphicAt J J' f x) : IsComplexLinearMap (J x) (J' (f x)) ↑(fderiv ℝ f x)

The Fréchet derivative of a J-holomorphic map is complex-linear.

theorem TauCeti.IsJHolomorphicAt.fderiv_apply_commute {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {x v : U} (hf : IsJHolomorphicAt J J' f x) : (fderiv ℝ f x) ((J x).toLinearMap v) = (J' (f x)).toLinearMap ((fderiv ℝ f x) v)

The Fréchet derivative of a J-holomorphic map commutes with the structures.

theorem TauCeti.IsJHolomorphicAt.isJHolomorphicWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicAt J J' f x) : IsJHolomorphicWithinAt J J' f s x

Pointwise J-holomorphicity implies J-holomorphicity within any set.

theorem TauCeti.IsJHolomorphicWithinAt.derivative_isComplexLinear {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f s x) : IsComplexLinearMap (J x) (J' (f x)) ↑(Classical.choose ⋯)

The chosen within-set derivative is complex-linear.

theorem TauCeti.IsJHolomorphicWithinAt.fderivWithin_isComplexLinear {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f s x) (hs : UniqueDiffWithinAt ℝ s x) : IsComplexLinearMap (J x) (J' (f x)) ↑(fderivWithin ℝ f s x)

The within-set Fréchet derivative is complex-linear when derivatives are unique.

theorem TauCeti.IsJHolomorphicWithinAt.fderivWithin_apply_commute {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x v : U} (hf : IsJHolomorphicWithinAt J J' f s x) (hs : UniqueDiffWithinAt ℝ s x) : (fderivWithin ℝ f s x) ((J x).toLinearMap v) = (J' (f x)).toLinearMap ((fderivWithin ℝ f s x) v)

The within-set Fréchet derivative commutes with the structures.

theorem TauCeti.IsJHolomorphicWithinAt.isJHolomorphicAt_of_mem_nhds {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f s x) (hs : s ∈ nhds x) : IsJHolomorphicAt J J' f x

Within-set J-holomorphicity on a neighborhood implies pointwise J-holomorphicity.

theorem TauCeti.IsJHolomorphicWithinAt.mono {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s t : Set U} {x : U} (hf : IsJHolomorphicWithinAt J J' f t x) (hst : s ⊆ t) : IsJHolomorphicWithinAt J J' f s x

Restrict the domain set of a within-set J-holomorphic map.

@[simp]

theorem TauCeti.isJHolomorphicWithinAt_univ {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) (x : U) : IsJHolomorphicWithinAt J J' f Set.univ x ↔ IsJHolomorphicAt J J' f x

Within the whole space, J-holomorphicity is the same as pointwise J-holomorphicity.

theorem TauCeti.IsJHolomorphicOn.isJHolomorphicWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} (hf : IsJHolomorphicOn J J' f s) {x : U} (hx : x ∈ s) : IsJHolomorphicWithinAt J J' f s x

A setwise J-holomorphic map is J-holomorphic within the set at each member.

theorem TauCeti.IsJHolomorphicOn.mono {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s t : Set U} (hf : IsJHolomorphicOn J J' f t) (hst : s ⊆ t) : IsJHolomorphicOn J J' f s

Restrict the domain set of a setwise J-holomorphic map.

theorem TauCeti.IsJHolomorphicOn.differentiableOn {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} (hf : IsJHolomorphicOn J J' f s) : DifferentiableOn ℝ f s

A setwise J-holomorphic map is differentiable on its domain.

theorem TauCeti.IsJHolomorphicOn.continuousOn {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} {s : Set U} (hf : IsJHolomorphicOn J J' f s) : ContinuousOn f s

A setwise J-holomorphic map is continuous on its domain.

theorem TauCeti.IsJHolomorphic.isJHolomorphicOn {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} (hf : IsJHolomorphic J J' f) (s : Set U) : IsJHolomorphicOn J J' f s

A globally J-holomorphic map is J-holomorphic on every set.

theorem TauCeti.IsJHolomorphic.differentiable {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} (hf : IsJHolomorphic J J' f) : Differentiable ℝ f

A globally J-holomorphic map is differentiable.

theorem TauCeti.IsJHolomorphic.continuous {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {f : U → V} (hf : IsJHolomorphic J J' f) : Continuous f

A globally J-holomorphic map is continuous.

@[simp]

theorem TauCeti.isJHolomorphicOn_univ {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (f : U → V) : IsJHolomorphicOn J J' f Set.univ ↔ IsJHolomorphic J J' f

J-holomorphicity on the whole space is equivalent to global J-holomorphicity.

@[simp]

theorem TauCeti.isJHolomorphicAt_constStructure_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure U) (J' : AlmostComplexStructure V) (f : U → V) (x : U) : IsJHolomorphicAt (fun (x : U) => J) (fun (x : V) => J') f x ↔ IsConstStructureJHolomorphicAt J J' f x

For constant structure functions, varying-structure pointwise J-holomorphicity is exactly the existing constant-structure predicate.

@[simp]

theorem TauCeti.isJHolomorphicWithinAt_constStructure_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure U) (J' : AlmostComplexStructure V) (f : U → V) (s : Set U) (x : U) : IsJHolomorphicWithinAt (fun (x : U) => J) (fun (x : V) => J') f s x ↔ IsConstStructureJHolomorphicWithinAt J J' f s x

For constant structure functions, varying-structure within-set J-holomorphicity is exactly the existing constant-structure predicate.

@[simp]

theorem TauCeti.isJHolomorphicOn_constStructure_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure U) (J' : AlmostComplexStructure V) (f : U → V) (s : Set U) : IsJHolomorphicOn (fun (x : U) => J) (fun (x : V) => J') f s ↔ IsConstStructureJHolomorphicOn J J' f s

For constant structure functions, setwise J-holomorphicity is exactly the existing constant-structure predicate.

@[simp]

theorem TauCeti.isJHolomorphic_constStructure_iff {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure U) (J' : AlmostComplexStructure V) (f : U → V) : IsJHolomorphic (fun (x : U) => J) (fun (x : V) => J') f ↔ IsConstStructureJHolomorphic J J' f

For constant structure functions, global J-holomorphicity is exactly the existing constant-structure predicate.

@[simp]

theorem TauCeti.isJHolomorphicAt_id {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (J : U → AlmostComplexStructure U) (x : U) : IsJHolomorphicAt J J id x

The identity map is J-holomorphic at every point for every varying almost complex structure.

@[simp]

theorem TauCeti.isJHolomorphicAt_const {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (c : V) (x : U) : IsJHolomorphicAt J J' (fun (x : U) => c) x

A constant map is J-holomorphic at every point for arbitrary source and target structures.

@[simp]

theorem TauCeti.isJHolomorphicWithinAt_id {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (J : U → AlmostComplexStructure U) (s : Set U) (x : U) : IsJHolomorphicWithinAt J J id s x

The identity map is J-holomorphic within every set at every point.

@[simp]

theorem TauCeti.isJHolomorphicWithinAt_const {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (c : V) (s : Set U) (x : U) : IsJHolomorphicWithinAt J J' (fun (x : U) => c) s x

A constant map is J-holomorphic within every set at every point.

@[simp]

theorem TauCeti.isJHolomorphicOn_id {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (J : U → AlmostComplexStructure U) (s : Set U) : IsJHolomorphicOn J J id s

The identity map is J-holomorphic on every set.

@[simp]

theorem TauCeti.isJHolomorphicOn_const {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (c : V) (s : Set U) : IsJHolomorphicOn J J' (fun (x : U) => c) s

A constant map is J-holomorphic on every set.

@[simp]

theorem TauCeti.isJHolomorphic_id {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (J : U → AlmostComplexStructure U) : IsJHolomorphic J J id

The identity map is J-holomorphic for every varying almost complex structure.

@[simp]

theorem TauCeti.isJHolomorphic_const {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : U → AlmostComplexStructure U) (J' : V → AlmostComplexStructure V) (c : V) : IsJHolomorphic J J' fun (x : U) => c

A constant map is J-holomorphic for arbitrary source and target structures.

theorem TauCeti.IsJHolomorphicAt.comp {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {J'' : W → AlmostComplexStructure W} {f : U → V} {g : V → W} {x : U} (hg : IsJHolomorphicAt J' J'' g (f x)) (hf : IsJHolomorphicAt J J' f x) : IsJHolomorphicAt J J'' (g ∘ f) x

The composition of two J-holomorphic maps is J-holomorphic at a point.

theorem TauCeti.IsJHolomorphicWithinAt.comp {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {J'' : W → AlmostComplexStructure W} {f : U → V} {g : V → W} {s : Set U} {t : Set V} {x : U} (hg : IsJHolomorphicWithinAt J' J'' g t (f x)) (hf : IsJHolomorphicWithinAt J J' f s x) (hst : Set.MapsTo f s t) : IsJHolomorphicWithinAt J J'' (g ∘ f) s x

The composition of two within-set J-holomorphic maps is J-holomorphic within the source set.

theorem TauCeti.IsJHolomorphicOn.comp {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {J'' : W → AlmostComplexStructure W} {f : U → V} {g : V → W} {s : Set U} {t : Set V} (hg : IsJHolomorphicOn J' J'' g t) (hf : IsJHolomorphicOn J J' f s) (hst : Set.MapsTo f s t) : IsJHolomorphicOn J J'' (g ∘ f) s

The composition of two setwise J-holomorphic maps is J-holomorphic on the source set.

theorem TauCeti.IsJHolomorphic.comp {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : U → AlmostComplexStructure U} {J' : V → AlmostComplexStructure V} {J'' : W → AlmostComplexStructure W} {f : U → V} {g : V → W} (hg : IsJHolomorphic J' J'' g) (hf : IsJHolomorphic J J' f) : IsJHolomorphic J J'' (g ∘ f)

The composition of two globally J-holomorphic maps is globally J-holomorphic.