Finite almost complex structures in charts and reconstruction

Let J be a finite-regularity almost complex structure on a smooth manifold M modelled on E. Read in the trivialization of the tangent bundle at x, along the inverse of the extended chart at x, the structure becomes a map E → (E →L[ℝ] E). It squares to -1 on the chart target and equals J x at the chart point. For smooth structures the coordinate field is differentiable there, and its derivative at the chart point anticommutes with J x. More generally, along a chart ψ of M with values in a normed space, J reads as the field dψ ∘ J ∘ dψ⁻¹.

The finite field is C^n on the full extended target, with ordinary pointwise C^n regularity in boundaryless models. ContMDiffAlmostComplexStructure.chartEquiv reconstructs an actual structure on the intrinsic open chart source from a C^n model-endomorphism field on the open target in H. For models with corners that target need not be open in E. Both reconstruction round trips are part of the equivalence; native tangent-frame transitions give coordinate conjugation.

Main declarations

• ContMDiffAlmostComplexStructure.inChart, contDiffOn_inChart: the full finite coordinate field.

• ContMDiffAlmostComplexStructure.chartEquiv: chart-source reconstruction and both round trips.

• ContMDiffAlmostComplexStructure.inChart_extChartAt_eq_conj: derivative conjugation on overlaps.

• ContMDiffAlmostComplexStructure.chartPushforward: the structure read in the coordinates of a chart with values in a normed space; chartPushforward_apply_chartPushforward_apply, mfderiv_comp_toEndomorphism and chartPushforward_eq_pullbackEnd_inChart: it squares to -1, the chart derivative intertwines it with J, and it is a pullback of J read in the extended chart.

• TauCeti.SmoothAlmostComplexStructure.inChart: the almost complex structure read in a chart.

• TauCeti.SmoothAlmostComplexStructure.chartPushforward: the smooth structure pushed forward along a chart with values in a normed space.

• TauCeti.SmoothAlmostComplexStructure.inChart_apply_eq_mfderiv, TauCeti.SmoothAlmostComplexStructure.inChart_extChartAt_apply_eq_mfderiv: it is J conjugated by the derivatives of the chart and of its inverse.

• TauCeti.SmoothAlmostComplexStructure.fderiv_extChartAt_comp_apply_eq_inChart, TauCeti.SmoothAlmostComplexStructure.fderiv_comp_extChartAt_symm_inChart_apply: relations between derivatives of maps into and out of M involving J read in the chart.

• TauCeti.SmoothAlmostComplexStructure.inChart_inChart: it squares to -1 on the chart target.

• TauCeti.SmoothAlmostComplexStructure.inChart_extChartAt_self: it is J x at the chart point.

• TauCeti.SmoothAlmostComplexStructure.fderivWithin_inChart_apply_apply: its derivative at the chart point anticommutes with J x.

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.inChart {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) (z : E) : E →L[ℝ] E

Read a finite-regularity structure through the inverse extended chart and its tangent frame. The formula is total; the square and regularity assertions concern the actual chart target.

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_def {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) (z : E) : J.inChart x z = ContinuousLinearMap.inCoordinates E (TangentSpace I) E (TangentSpace I) x (↑(extChartAt I x).symm z) x (↑(extChartAt I x).symm z) (J.toEndomorphism (↑(extChartAt I x).symm z))

The finite chart field is the native Hom-bundle coordinate expression.

theorem TauCeti.ContMDiffAlmostComplexStructure.contDiffOn_inChart {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) : ContDiffOn ℝ (↑n) (J.inChart x) (extChartAt I x).target

The full coordinate field has the specified finite regularity on the full extended target. For a model with corners this is regularity within that target, not a claim that it is open in E.

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_inChart {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) {z : E} (hz : z ∈ (extChartAt I x).target) (v : E) : (J.inChart x z) ((J.inChart x z) v) = -v

On the actual chart target the model endomorphism squares to minus the identity.

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_extChartAt_self {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.inChart x (↑(extChartAt I x) x) = J.toEndomorphism x

At the chart center the model field agrees with the original fibre endomorphism.

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_apply_eq_mfderiv {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) {z : E} (hz : z ∈ (extChartAt I x).target) (w : E) : (J.inChart x z) w = (mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm z)) ((fun (x : M) => ⇑(J.toEndomorphism x)) (↑(extChartAt I x).symm z) ((mfderiv[Set.range ↑I] ↑(extChartAt I x).symm z) w))

On the chart target, the finite coordinate field is J at the corresponding point, conjugated by the derivatives of the chart and of its inverse.

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.chartPushforward {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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (ψ : OpenPartialHomeomorph M G) (p : G) : G →L[ℝ] G

The structure J pushed forward along a chart ψ of M with values in a normed space G: at p, the endomorphism dψ ∘ J ∘ dψ⁻¹ of G, taken at ψ⁻¹ p and written with the manifold derivatives of ψ and of its inverse. On the target of ψ this is J in the coordinates of ψ.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartPushforward_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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (ψ : OpenPartialHomeomorph M G) (p w : G) : (J.chartPushforward ψ p) w = (mfderiv% ↑ψ (↑ψ.symm p)) ((fun (x : M) => ⇑(J.toEndomorphism x)) (↑ψ.symm p) ((mfderiv% ↑ψ.symm p) w))

Evaluate a pushed-forward structure.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.chartPushforward_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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (h : m ≤ n) (ψ : OpenPartialHomeomorph M G) : (J.ofLE h).chartPushforward ψ = J.chartPushforward ψ

Forgetting regularity does not change the pushed-forward structure.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartPushforward_apply_chartPushforward_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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (ψ : OpenPartialHomeomorph M G) {p : G} (hp : p ∈ ψ.target) (hψ : MDiffAt ↑ψ (↑ψ.symm p)) (hψs : MDiffAt ↑ψ.symm p) (w : G) : (J.chartPushforward ψ p) ((J.chartPushforward ψ p) w) = -w

The pushed-forward structure is an almost complex structure. At a point of the target where the chart and its inverse are differentiable, ψ_* J squares to -1.

theorem TauCeti.ContMDiffAlmostComplexStructure.mfderiv_comp_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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (ψ : OpenPartialHomeomorph M G) {y : M} (hy : y ∈ ψ.source) (hψ : MDiffAt ↑ψ y) (hψs : MDiffAt ↑ψ.symm (↑ψ y)) : mfderiv% ↑ψ y ∘SL J.toEndomorphism y = J.chartPushforward ψ (↑ψ y) ∘SL mfderiv% ↑ψ y

The derivative of a chart intertwines J with the pushed-forward structure.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartPushforward_eq_pullbackEnd_inChart {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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [I.Boundaryless] (ψ : OpenPartialHomeomorph M G) (e : OpenPartialHomeomorph G E) {p : G} (hp : ↑e p ∈ (extChartAt I x).target) (hψ : ↑ψ =ᶠ[nhds (↑ψ.symm p)] ↑e.symm ∘ ↑(extChartAt I x)) (hψs : ↑ψ.symm =ᶠ[nhds p] ↑(extChartAt I x).symm ∘ ↑e) (he : DifferentiableAt ℝ (↑e) p) (hes : DifferentiableAt ℝ (↑e.symm) (↑e p)) : J.chartPushforward ψ p = e.pullbackEnd (J.inChart x) p

Pushforward along a chart through the extended chart. If, near the relevant points, a chart ψ is e⁻¹ ∘ χ and its inverse is χ⁻¹ ∘ e for the extended chart χ at x and an open partial homeomorphism e of normed spaces, then ψ_* J is the pullback by e of J read in χ.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_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) (x : M) (h : m ≤ n) : (J.ofLE h).inChart x = J.inChart x

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_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) (x : M) : (-J).inChart x = -J.inChart x

theorem TauCeti.ContMDiffAlmostComplexStructure.contDiffAt_inChart {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) [I.Boundaryless] {z : E} (hz : z ∈ (extChartAt I x).target) : ContDiffAt ℝ (↑n) (J.inChart x) z

At each point of a boundaryless chart target the coordinate field is an ordinary C^n map.

theorem TauCeti.ContMDiffAlmostComplexStructure.inChart_extChartAt_eq_conj {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) {y : M} (hy : y ∈ (chartAt H x).source) {x' : M} (hy' : y ∈ (chartAt H x').source) : J.inChart x' (↑(extChartAt I x') y) = tangentCoordChange I x x' y ∘SL J.inChart x (↑(extChartAt I x) y) ∘SL tangentCoordChange I x' x y

Chart-coordinate fields are conjugated by the actual derivative of the chart transition. tangentCoordChange is the native derivative within range I of the extended transition map.

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.chartEquiv {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 : ℕ∞} (x : M) : ContMDiffAlmostComplexStructure I n ↥{ carrier := (chartAt H x).source, is_open' := ⋯ } ≃ { A : ContMDiffMap I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↥{ carrier := (chartAt H x).target, is_open' := ⋯ }) (E →L[ℝ] E) ↑n // ∀ (z : ↥{ carrier := (chartAt H x).target, is_open' := ⋯ }) (v : E), (A z) ((A z) v) = -v }

Exact reconstruction on an intrinsic open chart source from finite-regularity endomorphism fields on its open target in H. For models with corners the target need not be open in E.

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.ofChart {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 : ℕ∞} (x : M) (A : E → E →L[ℝ] E) (hA : ContDiffOn ℝ (↑n) A (extChartAt I x).target) (hAA : ∀ z ∈ (extChartAt I x).target, ∀ (v : E), (A z) ((A z) v) = -v) : ContMDiffAlmostComplexStructure I n ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }

Reconstruct on the intrinsic chart source directly from a normed-space field on the extended target. Its finite regularity and square identity are required only on that target.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.chartEquiv_ofChart {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 : ℕ∞} (x : M) (A : E → E →L[ℝ] E) (hA : ContDiffOn ℝ (↑n) A (extChartAt I x).target) (hAA : ∀ z ∈ (extChartAt I x).target, ∀ (v : E), (A z) ((A z) v) = -v) (z : ↥{ carrier := (chartAt H x).target, is_open' := ⋯ }) : ↑((chartEquiv x) (ofChart x A hA hAA)) z = A (↑I ↑z)

Reading the reconstructed chart structure recovers the prescribed normed-space field.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartEquiv_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 : ℕ∞} (x : M) (Jc : ContMDiffAlmostComplexStructure I n ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }) (y : ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }) : ↑((chartEquiv x) Jc) ⟨↑(chartAt H x) ↑y, ⋯⟩ = (trivializationAt E (TangentSpace I) ⟨x, ⋯⟩).almostComplexCoordinates Jc y

The chart equivalence evaluates the coordinate field at the forward chart value.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartEquiv_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] {n : ℕ∞} (x : M) (A : { A : ContMDiffMap I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↥{ carrier := (chartAt H x).target, is_open' := ⋯ }) (E →L[ℝ] E) ↑n // ∀ (z : ↥{ carrier := (chartAt H x).target, is_open' := ⋯ }) (v : E), (A z) ((A z) v) = -v }) (y : ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }) (v : TangentSpace I y) : (fun (x_1 : ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }) => ⇑(((chartEquiv x).symm A).toEndomorphism x_1)) y v = (Bundle.Trivialization.symmL ℝ (trivializationAt E (TangentSpace I) ⟨x, ⋯⟩) y) ((↑A ⟨↑(chartAt H x) ↑y, ⋯⟩) ((Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt E (TangentSpace I) ⟨x, ⋯⟩) y) v))

The inverse chart equivalence is inverse tangent-frame conjugation of the given field.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartEquiv_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 : ℕ∞} (x : M) (Jc : ContMDiffAlmostComplexStructure I n ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }) (h : m ≤ n) : ⇑↑((chartEquiv x) (Jc.ofLE h)) = ⇑↑((chartEquiv x) Jc)

The chart-coordinate equivalence preserves the underlying field when regularity is lowered.

theorem TauCeti.ContMDiffAlmostComplexStructure.chartEquiv_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 : ℕ∞} (x : M) (Jc : ContMDiffAlmostComplexStructure I n ↥{ carrier := (chartAt H x).source, is_open' := ⋯ }) : ⇑↑((chartEquiv x) (-Jc)) = fun (z : ↥{ carrier := (chartAt H x).target, is_open' := ⋯ }) => -↑((chartEquiv x) Jc) z

Negating a structure negates its chart-coordinate field.

noncomputable def TauCeti.SmoothAlmostComplexStructure.inChart {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) (z : E) : E →L[ℝ] E

The almost complex structure read in the trivialization of the tangent bundle at x, along the inverse of the extended chart at x.

theorem TauCeti.SmoothAlmostComplexStructure.inChart_def {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) (z : E) : J.inChart x z = ContinuousLinearMap.inCoordinates E (TangentSpace I) E (TangentSpace I) x (↑(extChartAt I x).symm z) x (↑(extChartAt I x).symm z) (J.toEndomorphism (↑(extChartAt I x).symm z))

The defining formula of inChart: J at (extChartAt I x).symm z, written in the coordinates of the trivialization of the tangent bundle at x.

@[simp]

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

Reading a smooth structure in a chart agrees with every finite-regularity specialization.

noncomputable def TauCeti.SmoothAlmostComplexStructure.chartPushforward {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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (ψ : OpenPartialHomeomorph M G) (p : G) : G →L[ℝ] G

The smooth structure J pushed forward along a chart ψ of M with values in a normed space G: at p, the endomorphism dψ ∘ J ∘ dψ⁻¹ of G, as in ContMDiffAlmostComplexStructure.chartPushforward.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.toContMDiff_chartPushforward {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) {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] (n : ℕ∞) (ψ : OpenPartialHomeomorph M G) : (J.toContMDiff n).chartPushforward ψ = J.chartPushforward ψ

Pushing forward a smooth structure agrees with every finite-regularity specialization.

theorem TauCeti.SmoothAlmostComplexStructure.contDiffOn_inChart {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) : ContDiffOn ℝ (↑⊤) (J.inChart x) (extChartAt I x).target

The smooth coordinate field is smooth on its full chart target.

theorem TauCeti.SmoothAlmostComplexStructure.inChart_extChartAt_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) {y : M} (hy : y ∈ (extChartAt I x).source) (u : E) : (J.inChart x (↑(extChartAt I x) y)) u = (↑(trivializationAt E (TangentSpace I) x) ⟨y, (fun (x : M) => ⇑(J.toEndomorphism x)) y ((trivializationAt E (TangentSpace I) x).symm y u)⟩).2

At the image of a point y of the chart at x, the almost complex structure read in the chart is J y in the coordinates of the trivialization of the tangent bundle at x.

theorem TauCeti.SmoothAlmostComplexStructure.inChart_apply_eq_mfderiv {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) {z : E} (hz : z ∈ (extChartAt I x).target) (w : E) : (J.inChart x z) w = (mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm z)) ((fun (x : M) => ⇑(J.toEndomorphism x)) (↑(extChartAt I x).symm z) ((mfderiv[Set.range ↑I] ↑(extChartAt I x).symm z) w))

On the chart target, the almost complex structure read in the chart is J at the corresponding point, conjugated by the derivatives of the chart and of its inverse.

theorem TauCeti.SmoothAlmostComplexStructure.inChart_extChartAt_apply_eq_mfderiv {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) {y : M} (hy : y ∈ (extChartAt I x).source) (w : E) : (J.inChart x (↑(extChartAt I x) y)) w = (mfderiv% ↑(extChartAt I x) y) ((fun (x : M) => ⇑(J.toEndomorphism x)) y ((mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)) w))

At the image of a point y of the chart at x, the almost complex structure read in the chart is J y, conjugated by the derivatives of the chart at y and of its inverse.

theorem TauCeti.SmoothAlmostComplexStructure.fderiv_extChartAt_comp_apply_eq_inChart {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) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {u : F → M} {w : F} (hu : MDiffAt u w) (hw : u w ∈ (extChartAt I x).source) {a b : F} (h : (mfderiv% u w) a = (fun (x : M) => ⇑(J.toEndomorphism x)) (u w) ((mfderiv% u w) b)) : (fderiv ℝ (↑(extChartAt I x) ∘ u) w) a = (J.inChart x ((↑(extChartAt I x) ∘ u) w)) ((fderiv ℝ (↑(extChartAt I x) ∘ u) w) b)

Read in the extended chart φ at x, a relation du(a) = J du(b) between derivatives at w of a map u from a normed space becomes d(φ ∘ u)(a) = J_φ d(φ ∘ u)(b), for the structure J_φ = J.inChart x read in the chart.

theorem TauCeti.SmoothAlmostComplexStructure.fderiv_comp_extChartAt_symm_inChart_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) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : M → F} {z : E} (hz : z ∈ (extChartAt I x).target) (hf : DifferentiableAt ℝ (f ∘ ↑(extChartAt I x).symm) z) (w : E) : (fderiv ℝ (f ∘ ↑(extChartAt I x).symm) z) ((J.inChart x z) w) = (d% f (↑(extChartAt I x).symm z)) ((fun (x : M) => ⇑(J.toEndomorphism x)) (↑(extChartAt I x).symm z) ((mfderiv[Set.range ↑I] ↑(extChartAt I x).symm z) w))

On the chart target, the derivative of the coordinate expression f ∘ φ⁻¹ of a map f into a normed space, applied after the structure J.inChart x read in the chart φ at x, is the derivative of f applied after J.

theorem TauCeti.SmoothAlmostComplexStructure.inChart_inChart {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) {z : E} (hz : z ∈ (extChartAt I x).target) (w : E) : (J.inChart x z) ((J.inChart x z) w) = -w

In the chart, the almost complex structure still squares to -1.

theorem TauCeti.SmoothAlmostComplexStructure.inChart_extChartAt_self {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.inChart x (↑(extChartAt I x) x) = J.toEndomorphism x

At the chart point, the almost complex structure read in the chart is J x.

theorem TauCeti.SmoothAlmostComplexStructure.differentiableWithinAt_inChart {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) : DifferentiableWithinAt ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)

The almost complex structure read in the chart at x is differentiable at the chart point.

theorem TauCeti.SmoothAlmostComplexStructure.fderivWithin_inChart_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 w : E) : ((fderivWithin ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)) v) ((J.inChart x (↑(extChartAt I x) x)) w) = -(J.inChart x (↑(extChartAt I x) x)) (((fderivWithin ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)) v) w)

Differentiating J² = -1 in the chart at x: the derivative of the almost complex structure read in the chart anticommutes with its value at the chart point.