Almost complex structures of finite regularity

TauCeti.ContMDiffAlmostComplexStructure I n M is a Cⁿ section of the tangent endomorphism bundle whose square is minus the identity in every fibre. The regularity parameter n : ℕ∞ includes continuous structures and the smooth endpoint.

TauCeti.ContMDiffAlmostComplexStructure.smoothEquiv identifies the infinite-regularity carrier with the existing SmoothAlmostComplexStructure. Forgetting regularity preserves the underlying section and commutes with evaluation. Applying a structure to a vector field along a map preserves every regularity order at most that of the structure.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, second edition, Section 2.2 (almost complex structures) and Appendix B (finite regularity).

structure TauCeti.ContMDiffAlmostComplexStructure {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (n : ℕ∞) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] : Type (max u_1 u_4)

A Cⁿ tangent endomorphism whose square is minus the identity in every fibre. The ambient manifold is smooth; the structure need only have regularity n.

• toEndomorphism : ContMDiffSection I (E →L[ℝ] E) ↑n fun (x : M) => TangentSpace I x →L[ℝ] TangentSpace I x

  The underlying endomorphism section with its specified regularity.

• square_neg (x : M) : self.toEndomorphism x ∘SL self.toEndomorphism x = -ContinuousLinearMap.id ℝ (TangentSpace I x)

  The defining identity holds at every point, not just on a chosen open set.

theorem TauCeti.ContMDiffAlmostComplexStructure.toEndomorphism_injective {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] {n : ℕ∞} : Function.Injective toEndomorphism

The endomorphism section determines the almost complex structure.

@[instance_reducible]

instance TauCeti.ContMDiffAlmostComplexStructure.instCoeFunForallForallTangentSpaceReal {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] {n : ℕ∞} : CoeFun (ContMDiffAlmostComplexStructure I n M) fun (x : ContMDiffAlmostComplexStructure I n M) => (x : M) → TangentSpace I x → TangentSpace I x

Evaluate the structure at a point and then at a tangent vector.

def TauCeti.ContMDiffAlmostComplexStructure.almostComplexStructureAt {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (x : M) : AlmostComplexStructure (TangentSpace I x)

The underlying real-linear almost complex structure on a tangent fibre.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.almostComplexStructureAt_toLinearMap {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (x : M) : (J.almostComplexStructureAt x).toLinearMap = ↑(J.toEndomorphism x)

theorem TauCeti.ContMDiffAlmostComplexStructure.almostComplexStructureAt_apply {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (x : M) (v : TangentSpace I x) : (J.almostComplexStructureAt x).toLinearMap v = (fun (x : M) => ⇑(J.toEndomorphism x)) x v

Evaluating the fibrewise structure agrees with evaluating the bundled section.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.apply_apply {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑(J.toEndomorphism x)) x ((fun (x : M) => ⇑(J.toEndomorphism x)) x v) = -v

Applying the structure twice negates a tangent vector.

theorem TauCeti.ContMDiffAlmostComplexStructure.injective {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (x : M) : Function.Injective ((fun (x : M) => ⇑(J.toEndomorphism x)) x)

Each fibrewise endomorphism is injective.

theorem TauCeti.ContMDiffAlmostComplexStructure.surjective {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (x : M) : Function.Surjective ((fun (x : M) => ⇑(J.toEndomorphism x)) x)

Each fibrewise endomorphism is surjective.

theorem TauCeti.ContMDiffAlmostComplexStructure.ext {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] {n : ℕ∞} {J K : ContMDiffAlmostComplexStructure I n M} (h : ∀ (x : M) (v : TangentSpace I x), (fun (x : M) => ⇑(J.toEndomorphism x)) x v = (fun (x : M) => ⇑(K.toEndomorphism x)) x v) : J = K

Equality is detected on tangent vectors.

theorem TauCeti.ContMDiffAlmostComplexStructure.ext_iff {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] {n : ℕ∞} {J K : ContMDiffAlmostComplexStructure I n M} : J = K ↔ ∀ (x : M) (v : TangentSpace I x), (fun (x : M) => ⇑(J.toEndomorphism x)) x v = (fun (x : M) => ⇑(K.toEndomorphism x)) x v

def TauCeti.ContMDiffAlmostComplexStructure.ofLE {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] {n m : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (h : m ≤ n) : ContMDiffAlmostComplexStructure I m M

Forget higher regularity without changing any fibrewise endomorphism.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.ofLE_toEndomorphism_apply {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] {n m : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (h : m ≤ n) (x : M) : (J.ofLE h).toEndomorphism x = J.toEndomorphism x

theorem TauCeti.ContMDiffAlmostComplexStructure.ofLE_apply {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] {n m : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (h : m ≤ n) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑((J.ofLE h).toEndomorphism x)) x v = (fun (x : M) => ⇑(J.toEndomorphism x)) x v

Forgetting regularity leaves the action on tangent vectors unchanged.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.ofLE_refl {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) : J.ofLE ⋯ = J

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.ofLE_ofLE {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] {n m l : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (h : m ≤ n) (h' : l ≤ m) : (J.ofLE h).ofLE h' = J.ofLE ⋯

theorem TauCeti.ContMDiffAlmostComplexStructure.ofLE_injective {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] {n m : ℕ∞} (h : m ≤ n) : Function.Injective fun (J : ContMDiffAlmostComplexStructure I n M) => J.ofLE h

Regularity forgetting is injective because it retains the entire section.

def TauCeti.ContMDiffAlmostComplexStructure.toSmooth {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 : ContMDiffAlmostComplexStructure I ⊤ M) : SmoothAlmostComplexStructure I M

At infinite regularity, retain the existing smooth almost complex structure carrier.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.toSmooth_toEndomorphism {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 : ContMDiffAlmostComplexStructure I ⊤ M) : J.toSmooth.toEndomorphism = J.toEndomorphism

theorem TauCeti.ContMDiffAlmostComplexStructure.toSmooth_apply {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 : ContMDiffAlmostComplexStructure I ⊤ M) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑(J.toSmooth.toEndomorphism x)) x v = (fun (x : M) => ⇑(J.toEndomorphism x)) x v

Smooth conversion preserves the action on tangent vectors.

def TauCeti.SmoothAlmostComplexStructure.toContMDiff {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) (n : ℕ∞) : ContMDiffAlmostComplexStructure I n M

View a smooth structure at any specified regularity.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.toContMDiff_toEndomorphism_apply {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) (n : ℕ∞) (x : M) : (J.toContMDiff n).toEndomorphism x = J.toEndomorphism x

theorem TauCeti.SmoothAlmostComplexStructure.toContMDiff_apply {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) (n : ℕ∞) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑((J.toContMDiff n).toEndomorphism x)) x v = (fun (x : M) => ⇑(J.toEndomorphism x)) x v

Changing the regularity of a smooth structure leaves its pointwise action unchanged.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.toContMDiff_ofLE {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) {m n : ℕ∞} (h : m ≤ n) : (J.toContMDiff n).ofLE h = J.toContMDiff m

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.toContMDiff_toSmooth {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) : (J.toContMDiff ⊤).toSmooth = J

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.toSmooth_toContMDiff {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 : ContMDiffAlmostComplexStructure I ⊤ M) : J.toSmooth.toContMDiff ⊤ = J

def TauCeti.ContMDiffAlmostComplexStructure.smoothEquiv {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] : ContMDiffAlmostComplexStructure I ⊤ M ≃ SmoothAlmostComplexStructure I M

The infinite-regularity carrier is equivalent to the native smooth carrier.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.smoothEquiv_apply {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 : ContMDiffAlmostComplexStructure I ⊤ M) : smoothEquiv J = J.toSmooth

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.smoothEquiv_symm_apply {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) : smoothEquiv.symm J = J.toContMDiff ⊤

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.neg {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) : ContMDiffAlmostComplexStructure I n M

Negation preserves the specified regularity and the square identity.

@[instance_reducible]

noncomputable instance TauCeti.ContMDiffAlmostComplexStructure.instNeg {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] {n : ℕ∞} : Neg (ContMDiffAlmostComplexStructure I n M)

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.neg_toEndomorphism {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) : (-J).toEndomorphism = -J.toEndomorphism

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.neg_neg {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] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) : - -J = J

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.ofLE_neg {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] {n m : ℕ∞} (J : ContMDiffAlmostComplexStructure I n M) (h : m ≤ n) : (-J).ofLE h = -J.ofLE h

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.const {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ∞) (Jc : V →L[ℝ] V) (hJc : ∀ (v : V), Jc (Jc v) = -v) : ContMDiffAlmostComplexStructure (modelWithCornersSelf ℝ V) n V

A continuous linear complex structure defines a constant structure at every regularity.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.const_toEndomorphism_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ∞) (Jc : V →L[ℝ] V) (hJc : ∀ (v : V), Jc (Jc v) = -v) (x : V) : (const n Jc hJc).toEndomorphism x = Jc

def TauCeti.ContMDiffAlmostComplexStructure.ofModel {n : ℕ∞} {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : V → V →L[ℝ] V) (hA : ContDiff ℝ (↑n) A) (hAA : ∀ (x v : V), (A x) ((A x) v) = -v) : ContMDiffAlmostComplexStructure (modelWithCornersSelf ℝ V) n V

A Cⁿ field of continuous linear maps squaring to minus the identity defines a Cⁿ almost complex structure on the model manifold. The field may depend on the base point.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.ofModel_toEndomorphism_apply {n : ℕ∞} {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : V → V →L[ℝ] V) (hA : ContDiff ℝ (↑n) A) (hAA : ∀ (x v : V), (A x) ((A x) v) = -v) (x : V) : (ofModel A hA hAA).toEndomorphism x = A x

theorem TauCeti.ContMDiffAlmostComplexStructure.contDiff_toEndomorphism {n : ℕ∞} {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : ContMDiffAlmostComplexStructure (modelWithCornersSelf ℝ V) n V) : ContDiff ℝ (↑n) (have this := fun (x : V) => J.toEndomorphism x; this)

On a model manifold, the endomorphism field of a Cⁿ structure is a Cⁿ map of normed spaces. This is the converse to ofModel.

theorem TauCeti.ContMDiffAlmostComplexStructure.contMDiff_apply {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] {n m : ℕ∞} {E' : Type u_4} {H' : Type u_5} {N : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] (J : ContMDiffAlmostComplexStructure I n M) (hmn : m ≤ n) {b : N → M} (hb : ContMDiff I' I (↑m) b) {V : (y : N) → TangentSpace I (b y)} (hV : ContMDiff I' I.tangent ↑m fun (y : N) => ⟨b y, V y⟩) : ContMDiff I' I.tangent ↑m fun (y : N) => ⟨b y, (fun (x : M) => ⇑(J.toEndomorphism x)) (b y) (V y)⟩

Applying a Cⁿ structure to a Cᵐ vector field along a Cᵐ map preserves regularity whenever m ≤ n. This includes m = 0.