Smooth almost complex structures on manifolds

This file lifts the pointwise linear algebra of TauCeti.AlmostComplexStructure to smooth manifolds. A smooth almost complex structure is a smooth section of the endomorphism bundle of the tangent bundle whose square is fiberwise minus the identity. Its value at each point is a pointwise almost complex structure on that tangent space.

The smoothness is part of the structure itself, while relations to a symplectic form are not fields of it. Tameness and compatibility with a smooth two-form are TauCeti.SmoothTwoForm.Tames and TauCeti.SmoothTwoForm.Compatible in TauCeti.Geometry.Symplectic.Manifold.TwoForm. For a fiberwise nondegenerate form, TauCeti.SmoothTwoForm.IsNondegenerate.tames_iff and TauCeti.SmoothTwoForm.IsNondegenerate.compatible_iff reduce them to the pointwise TauCeti.SymplecticForm.Tames and TauCeti.SymplecticForm.Compatible for the tangent-fiber structures produced by almostComplexStructureAt. Manifold-valued J-holomorphic maps (TauCeti.Geometry.Symplectic.Manifold.JHolomorphic) are stated with this definition.

Main declarations

• TauCeti.SmoothAlmostComplexStructure: a smooth tangent-bundle endomorphism squaring to -1.
• TauCeti.SmoothAlmostComplexStructure.almostComplexStructureAt: the pointwise almost complex structure on a tangent space, with model-space complex-linearity bridge TauCeti.SmoothAlmostComplexStructure.isComplexLinearMap_almostComplexStructureAt_model_iff.
• TauCeti.SmoothAlmostComplexStructure.contMDiff_apply: applying the structure to a C^n vector field along a C^n map gives a C^n vector field along that map.
• TauCeti.SmoothAlmostComplexStructure.mdifferentiableAt_apply: the pointwise differentiable counterpart.
• TauCeti.SmoothAlmostComplexStructure.neg: the negative of a smooth almost complex structure.
• TauCeti.SmoothAlmostComplexStructure.const: a continuous endomorphism of a real normed space squaring to -1 gives the constant smooth almost complex structure on that model manifold.
• TauCeti.SmoothAlmostComplexStructure.contDiff_toEndomorphism: on a self-modelled normed space, the endomorphism section is C^∞ in the normed-space sense.
• TauCeti.AlmostComplexStructure.constSmooth: a pointwise almost complex structure on a finite-dimensional real normed space gives the constant smooth almost complex structure on that model manifold.
• TauCeti.SmoothAlmostComplexStructure.product: the standard smooth almost complex structure on V × V, sending (v, w) to (-w, v).
• TauCeti.SmoothAlmostComplexStructure.ofTangentCoordChangeISMul: multiplication by i on the tangent spaces of a manifold modelled on a complex normed space, as a smooth almost complex structure, when the tangent coordinate changes commute with multiplication by i. The almost complex structures of a complex manifold and of a Riemann surface with boundary are built from it.

The definition follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.2.

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

A smooth almost complex structure on a manifold is a smooth tangent-bundle endomorphism whose square is fiberwise minus the identity.

The endomorphism is bundled as a smooth section of End(TM). Tameness, compatibility with a symplectic form, and integrability are deliberately not fields of this structure.

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

  The underlying smooth section of the tangent endomorphism bundle.

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

  The defining identity J² = -1 on every tangent fiber.

theorem TauCeti.SmoothAlmostComplexStructure.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] : Function.Injective toEndomorphism

The underlying smooth endomorphism section determines a smooth almost complex structure.

@[instance_reducible]

instance TauCeti.SmoothAlmostComplexStructure.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] : CoeFun (SmoothAlmostComplexStructure I M) fun (x : SmoothAlmostComplexStructure I M) => (x : M) → TangentSpace I x → TangentSpace I x

A smooth almost complex structure is applied as J x v, evaluating its endomorphism of the tangent space at x on the tangent vector v.

def TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) (x : M) : AlmostComplexStructure (TangentSpace I x)

The value of a smooth almost complex structure at a point, as a pointwise AlmostComplexStructure on that tangent space.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) (x : M) : (J.almostComplexStructureAt x).toLinearMap = ↑(J.toEndomorphism x)

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) (x : M) (v : TangentSpace I x) : (J.almostComplexStructureAt x).toLinearMap v = (fun (x : M) => ⇑(J.toEndomorphism x)) x v

Evaluating the pointwise almost complex structure agrees with evaluating the smooth one.

theorem TauCeti.SmoothAlmostComplexStructure.isComplexLinearMap_almostComplexStructureAt_model_iff {V : Type u_4} {W : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J₁ : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V) (J₂ : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ W) W) (v : V) (w : W) (L : V →ₗ[ℝ] W) : IsComplexLinearMap (J₁.almostComplexStructureAt v) (J₂.almostComplexStructureAt w) L ↔ ∀ (u : V), L ((J₁.toEndomorphism v) u) = (J₂.toEndomorphism w) (L u)

On self-modelled normed spaces, IsComplexLinearMap between almostComplexStructureAt values is pointwise intertwining of toEndomorphism on the model spaces (bridging TangentSpace 𝓘(ℝ, V) x and V, where rw cannot match .toLinearMap at implicit transparency).

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑(J.toEndomorphism x)) x ((fun (x : M) => ⇑(J.toEndomorphism x)) x v) = -v

Applying a smooth almost complex structure twice gives the negative tangent vector.

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) (x : M) : Function.Injective ((fun (x : M) => ⇑(J.toEndomorphism x)) x)

A smooth almost complex structure is fiberwise injective.

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) (x : M) : Function.Surjective ((fun (x : M) => ⇑(J.toEndomorphism x)) x)

A smooth almost complex structure is fiberwise surjective.

theorem TauCeti.SmoothAlmostComplexStructure.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] {J K : SmoothAlmostComplexStructure I 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

Two smooth almost complex structures agreeing on every tangent vector are equal.

theorem TauCeti.SmoothAlmostComplexStructure.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] {J K : SmoothAlmostComplexStructure I 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

theorem TauCeti.SmoothAlmostComplexStructure.ext_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] {J K : SmoothAlmostComplexStructure I M} (h : ∀ (x : M), J.almostComplexStructureAt x = K.almostComplexStructureAt x) : J = K

Two smooth almost complex structures with the same pointwise almost complex structures are equal.

theorem TauCeti.SmoothAlmostComplexStructure.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] {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] {n : WithTop ℕ∞} [ENat.LEInfty n] (J : SmoothAlmostComplexStructure I M) {b : N → M} {V : (y : N) → TangentSpace I (b y)} (hV : ContMDiff I' I.tangent n fun (y : N) => ⟨b y, V y⟩) : ContMDiff I' I.tangent n fun (y : N) => ⟨b y, (fun (x : M) => ⇑(J.toEndomorphism x)) (b y) (V y)⟩

Applying a smooth almost complex structure along a C^n map b to a C^n vector field along b gives a C^n vector field along b. Taking b = id this says that J preserves C^n vector fields on M.

theorem TauCeti.SmoothAlmostComplexStructure.mdifferentiableAt_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] {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 : SmoothAlmostComplexStructure I M) {b : N → M} {y₀ : N} {V : (y : N) → TangentSpace I (b y)} (hV : (MDiffAt fun (y : N) => ⟨b y, V y⟩) y₀) : (MDiffAt fun (y : N) => ⟨b y, (fun (x : M) => ⇑(J.toEndomorphism x)) (b y) (V y)⟩) y₀

Applying a smooth almost complex structure to a vector field along a map b, differentiable at y₀ as a map into the tangent bundle, gives a vector field along b differentiable at y₀. Taking b = id this says that J preserves vector fields differentiable at a point.

theorem TauCeti.SmoothAlmostComplexStructure.contMDiffAt_toEndomorphism_of_eventuallyEq {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} {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] {n : WithTop ℕ∞} [ENat.LEInfty n] {J' : N → SmoothAlmostComplexStructure I M} {b : N → M} {y₀ : N} (hb : ContMDiffAt I' I n b y₀) (hJ' : ∀ᶠ (y : N) in nhds y₀, J' y = J) : ContMDiffAt I' (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E))) n (fun (y : N) => ⟨b y, (J' y).toEndomorphism (b y)⟩) y₀

A family of smooth almost complex structures which equals a fixed J near y₀, read along a map b which is C^n at y₀, is C^n at y₀ as a section of the tangent endomorphism bundle along b.

noncomputable def TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) : SmoothAlmostComplexStructure I M

Negating a smooth almost complex structure gives another smooth almost complex structure.

@[instance_reducible]

noncomputable instance TauCeti.SmoothAlmostComplexStructure.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] : Neg (SmoothAlmostComplexStructure I M)

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) : (-J).toEndomorphism = -J.toEndomorphism

theorem TauCeti.SmoothAlmostComplexStructure.neg_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) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑((-J).toEndomorphism x)) x v = -(fun (x : M) => ⇑(J.toEndomorphism x)) x v

Evaluating a negated smooth almost complex structure negates its value.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.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] (J : SmoothAlmostComplexStructure I M) : - -J = J

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.neg_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] (J : SmoothAlmostComplexStructure I M) (x : M) : (-J).almostComplexStructureAt x = -J.almostComplexStructureAt x

The pointwise structure of a negated smooth almost complex structure is the negation of the pointwise structure.

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

A continuous endomorphism of a normed space squaring to -1 defines a constant smooth almost complex structure on the corresponding model manifold.

@[simp]

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

The endomorphism section of a constant smooth almost complex structure has its defining value in every fiber.

theorem TauCeti.SmoothAlmostComplexStructure.const_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (Jc : V →L[ℝ] V) (hJc : ∀ (v : V), Jc (Jc v) = -v) (x v : V) : (fun (x : V) => ⇑((const Jc hJc).toEndomorphism x)) x v = Jc v

Evaluating a constant smooth almost complex structure applies its defining endomorphism.

theorem TauCeti.SmoothAlmostComplexStructure.contDiff_toEndomorphism {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V) : ContDiff ℝ ↑⊤ fun (x : V) => J.toEndomorphism x

On a self-modelled normed space, the endomorphism field of a SmoothAlmostComplexStructure is smooth in the normed-space sense.

noncomputable def TauCeti.AlmostComplexStructure.constSmooth {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (J : AlmostComplexStructure V) : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V

A pointwise almost complex structure on a finite-dimensional normed vector space defines a constant smooth almost complex structure on the corresponding model manifold.

@[simp]

theorem TauCeti.AlmostComplexStructure.constSmooth_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (J : AlmostComplexStructure V) (x v : V) : (fun (x : V) => ⇑(J.constSmooth.toEndomorphism x)) x v = J.toLinearMap v

@[simp]

theorem TauCeti.AlmostComplexStructure.fromTangentSpace_constSmooth_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (J : AlmostComplexStructure V) (x : V) (v : TangentSpace (modelWithCornersSelf ℝ V) x) : (NormedSpace.fromTangentSpace x) ((fun (x : V) => ⇑(J.constSmooth.toEndomorphism x)) x v) = J.toLinearMap ((NormedSpace.fromTangentSpace x) v)

Under the canonical identification of a self-model tangent fiber with the model space, evaluating a constant smooth almost complex structure is evaluating its defining linear map.

@[simp]

theorem TauCeti.AlmostComplexStructure.constSmooth_almostComplexStructureAt {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (J : AlmostComplexStructure V) (x : V) : J.constSmooth.almostComplexStructureAt x = J

noncomputable def TauCeti.SmoothAlmostComplexStructure.product (V : Type u_4) [NormedAddCommGroup V] [NormedSpace ℝ V] : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (V × V)) (V × V)

The standard smooth almost complex structure on V × V, sending (v, w) to (-w, v).

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.product_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (x v : V × V) : (fun (x : V × V) => ⇑((product V).toEndomorphism x)) x v = (-v.2, v.1)

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.product_almostComplexStructureAt {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × V) : (product V).almostComplexStructureAt x = AlmostComplexStructure.product V

Multiplication by i on a manifold modelled on a complex normed space

noncomputable def TauCeti.SmoothAlmostComplexStructure.ofTangentCoordChangeISMul {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (N : Type u_6) [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' (↑⊤) N] (h : ∀ {x y z : N}, z ∈ (chartAt H' x).source ∩ (chartAt H' y).source → ∀ (v : E'), (tangentCoordChange I' x y z) (Complex.I • v) = Complex.I • (tangentCoordChange I' x y z) v) : SmoothAlmostComplexStructure I' N

Multiplication by i on the tangent spaces of a manifold N modelled on a complex normed space E', as a smooth almost complex structure, when the tangent coordinate changes of N commute with multiplication by i.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.ofTangentCoordChangeISMul_apply {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' (↑⊤) N] (h : ∀ {x y z : N}, z ∈ (chartAt H' x).source ∩ (chartAt H' y).source → ∀ (v : E'), (tangentCoordChange I' x y z) (Complex.I • v) = Complex.I • (tangentCoordChange I' x y z) v) (x : N) (v : E') : (fun (x : N) => ⇑((ofTangentCoordChangeISMul I' N ⋯).toEndomorphism x)) x v = Complex.I • v

The almost complex structure ofTangentCoordChangeISMul is multiplication by i on every tangent space.

theorem TauCeti.SmoothAlmostComplexStructure.toEndomorphism_ofTangentCoordChangeISMul {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' (↑⊤) N] (h : ∀ {x y z : N}, z ∈ (chartAt H' x).source ∩ (chartAt H' y).source → ∀ (v : E'), (tangentCoordChange I' x y z) (Complex.I • v) = Complex.I • (tangentCoordChange I' x y z) v) (x : N) : (ofTangentCoordChangeISMul I' N ⋯).toEndomorphism x = Complex.I • ContinuousLinearMap.id ℝ E'

The almost complex structure ofTangentCoordChangeISMul is multiplication by i on every tangent space, as an endomorphism.

theorem TauCeti.SmoothAlmostComplexStructure.inTangentCoordinates_ofTangentCoordChangeISMul {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' (↑⊤) N] (h : ∀ {x y z : N}, z ∈ (chartAt H' x).source ∩ (chartAt H' y).source → ∀ (v : E'), (tangentCoordChange I' x y z) (Complex.I • v) = Complex.I • (tangentCoordChange I' x y z) v) {x₀ x : N} (hx : x ∈ (chartAt H' x₀).source) : inTangentCoordinates I' I' id id (fun (x : N) => (ofTangentCoordChangeISMul I' N ⋯).toEndomorphism x) x₀ x = Complex.I • ContinuousLinearMap.id ℝ E'

In the tangent coordinates of the chart at any point x₀, the almost complex structure ofTangentCoordChangeISMul is multiplication by i on the whole chart domain.