Transporting constant-structure J-holomorphic maps along linear coordinate changes

This file records that the local constant-structure J-holomorphic predicate is invariant under continuous real-linear changes of source and target coordinates. If f : V → W is constant-structure J-holomorphic and eV : V ≃L[ℝ] V', eW : W ≃L[ℝ] W', then the transported map v' ↦ eW (f (eV.symm v')) is constant-structure J-holomorphic for the transported almost complex structures.

These are the chart-change lemmas needed before the analytic Heegaard Floer roadmap upgrades the normed-vector-space Cauchy--Riemann equation to tangent charts on almost complex manifolds. The almost complex structures themselves are transported by the linear-algebra API in TauCeti.Geometry.Symplectic.Transport; this file adds the matching map-level calculus.

Main declarations

• TauCeti.IsConstStructureJHolomorphicAt.transport: pointwise transport of constant-structure J-holomorphicity.
• TauCeti.IsConstStructureJHolomorphicWithinAt.transport: within-set transport along a source coordinate change whose inverse maps the transported source set back into the original source set.
• TauCeti.IsConstStructureJHolomorphicOn.transport and TauCeti.IsConstStructureJHolomorphic.transport: setwise and global transport.
• TauCeti.isConstStructureJHolomorphicAt_transport_iff, TauCeti.isConstStructureJHolomorphicWithinAt_transport_iff, TauCeti.isConstStructureJHolomorphicOn_transport_iff, and TauCeti.isConstStructureJHolomorphic_transport_iff: transport equivalences, obtained by applying the forward statement in both directions.

The convention follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1: constant-structure J-holomorphicity is the Cauchy--Riemann equation df ∘ J = J' ∘ df, and coordinate changes conjugate both J and df.

theorem TauCeti.IsConstStructureJHolomorphicAt.transport {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : IsConstStructureJHolomorphicAt (J.transport ↑eV) (J'.transport ↑eW) (fun (y : V') => eW (f (eV.symm y))) (eV x)

Transport a pointwise constant-structure J-holomorphic map along continuous real-linear equivalences of the source and target coordinates.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.transport {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} {t : Set V'} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : Set.MapsTo (fun (y : V') => eV.symm y) t s → IsConstStructureJHolomorphicWithinAt (J.transport ↑eV) (J'.transport ↑eW) (fun (y : V') => eW (f (eV.symm y))) t (eV x)

Transport a within-set constant-structure J-holomorphic map along continuous real-linear equivalences of the source and target coordinates, for any target-domain set whose points map back into the original source set.

theorem TauCeti.IsConstStructureJHolomorphicOn.transport {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {t : Set V'} (hf : IsConstStructureJHolomorphicOn J J' f s) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : Set.MapsTo (fun (y : V') => eV.symm y) t s → IsConstStructureJHolomorphicOn (J.transport ↑eV) (J'.transport ↑eW) (fun (y : V') => eW (f (eV.symm y))) t

Transport a setwise constant-structure J-holomorphic map along continuous real-linear equivalences of the source and target coordinates, for any target-domain set whose points map back into the original source set.

theorem TauCeti.IsConstStructureJHolomorphic.transport {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : IsConstStructureJHolomorphic (J.transport ↑eV) (J'.transport ↑eW) fun (y : V') => eW (f (eV.symm y))

Transport a globally constant-structure J-holomorphic map along continuous real-linear equivalences of the source and target coordinates.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicAt_transport_iff {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} (f : V → W) (x : V) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : IsConstStructureJHolomorphicAt (J.transport ↑eV) (J'.transport ↑eW) (fun (y : V') => eW (f (eV.symm y))) (eV x) ↔ IsConstStructureJHolomorphicAt J J' f x

Pointwise constant-structure J-holomorphicity is invariant under continuous real-linear coordinate changes.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicWithinAt_transport_iff {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} (f : V → W) (s : Set V) (x : V) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : IsConstStructureJHolomorphicWithinAt (J.transport ↑eV) (J'.transport ↑eW) (fun (y : V') => eW (f (eV.symm y))) (⇑eV '' s) (eV x) ↔ IsConstStructureJHolomorphicWithinAt J J' f s x

Within-set constant-structure J-holomorphicity is invariant under continuous real-linear coordinate changes, with the source set sent to its image.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicOn_transport_iff {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} (f : V → W) (s : Set V) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : IsConstStructureJHolomorphicOn (J.transport ↑eV) (J'.transport ↑eW) (fun (y : V') => eW (f (eV.symm y))) (⇑eV '' s) ↔ IsConstStructureJHolomorphicOn J J' f s

Setwise constant-structure J-holomorphicity is invariant under continuous real-linear coordinate changes, with the source set sent to its image.

@[simp]

theorem TauCeti.isConstStructureJHolomorphic_transport_iff {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedAddCommGroup W'] [NormedSpace ℝ W'] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} (f : V → W) (eV : V ≃L[ℝ] V') (eW : W ≃L[ℝ] W') : (IsConstStructureJHolomorphic (J.transport ↑eV) (J'.transport ↑eW) fun (y : V') => eW (f (eV.symm y))) ↔ IsConstStructureJHolomorphic J J' f

Global constant-structure J-holomorphicity is invariant under continuous real-linear coordinate changes.