Finite almost complex structures in a tangent trivialization

Reading a native finite-regularity almost complex structure in an atlas trivialization gives a field of model endomorphisms of the same order. When the trivialization covers the base, the construction is reversible. Both directions use the existing Hom-bundle trivialization and its native section-regularity equivalence.

The ambient manifold is smooth, as required by the canonical carrier; the field order includes zero and infinity. No finite-dimensionality or completeness assumption is required.

noncomputable def Bundle.Trivialization.almostComplexCoordinates {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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) (x : M) : E →L[ℝ] E

Read an almost complex structure in a specified tangent-bundle trivialization.

theorem Bundle.Trivialization.almostComplexCoordinates_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) (x : M) (v : E) : (e.almostComplexCoordinates J x) v = (continuousLinearMapAt ℝ e x) ((fun (x : M) => ⇑(J.toEndomorphism x)) x ((symmL ℝ e x) v))

The coordinate field evaluates by conjugating through the chosen tangent frame.

theorem Bundle.Trivialization.contMDiffOn_almostComplexCoordinates {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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) : ContMDiffOn I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↑n) (e.almostComplexCoordinates J) e.baseSet

The coordinate field retains the specified finite order on the full trivialization domain.

theorem Bundle.Trivialization.almostComplexCoordinates_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) {x : M} (hx : x ∈ e.baseSet) (v : E) : (e.almostComplexCoordinates J x) ((e.almostComplexCoordinates J x) v) = -v

Coordinates preserve the square identity at every point of the trivialization domain.

@[simp]

theorem Bundle.Trivialization.almostComplexCoordinates_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) (h : m ≤ n) : e.almostComplexCoordinates (J.ofLE h) = e.almostComplexCoordinates J

@[simp]

theorem Bundle.Trivialization.almostComplexCoordinates_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) : e.almostComplexCoordinates (-J) = -e.almostComplexCoordinates J

noncomputable def Bundle.Trivialization.almostComplexStructure {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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (he : e.baseSet = Set.univ) (A : M → E →L[ℝ] E) (hA : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↑n) A) (hAA : ∀ (x : M) (v : E), (A x) ((A x) v) = -v) : TauCeti.ContMDiffAlmostComplexStructure I n M

Construct a native almost complex structure from a finite-regularity coordinate field in a tangent trivialization covering the whole base.

theorem Bundle.Trivialization.almostComplexStructure_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (he : e.baseSet = Set.univ) (A : M → E →L[ℝ] E) (hA : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↑n) A) (hAA : ∀ (x : M) (v : E), (A x) ((A x) v) = -v) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑((e.almostComplexStructure he A hA hAA).toEndomorphism x)) x v = (symmL ℝ e x) ((A x) ((continuousLinearMapAt ℝ e x) v))

Reconstruction evaluates by the inverse coordinate conjugation.

@[simp]

theorem Bundle.Trivialization.almostComplexCoordinates_almostComplexStructure {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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (he : e.baseSet = Set.univ) (A : M → E →L[ℝ] E) (hA : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↑n) A) (hAA : ∀ (x : M) (v : E), (A x) ((A x) v) = -v) : e.almostComplexCoordinates (e.almostComplexStructure he A hA hAA) = A

Reading a reconstructed structure recovers the entire coordinate field.

@[simp]

theorem Bundle.Trivialization.almostComplexStructure_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (he : e.baseSet = Set.univ) (A : M → E →L[ℝ] E) (hA : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↑n) A) (hAA : ∀ (x : M) (v : E), (A x) ((A x) v) = -v) (h : m ≤ n) : (e.almostComplexStructure he A hA hAA).ofLE h = e.almostComplexStructure he A ⋯ hAA

Reconstruction commutes with forgetting regularity.

theorem Bundle.Trivialization.almostComplexStructure_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (he : e.baseSet = Set.univ) (A : M → E →L[ℝ] E) (hA : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E)) (↑n) A) (hAA : ∀ (x : M) (v : E), (A x) ((A x) v) = -v) : e.almostComplexStructure he (-A) ⋯ ⋯ = -e.almostComplexStructure he A hA hAA

Reconstruction commutes with negating the coordinate field.

theorem Bundle.Trivialization.almostComplexCoordinates_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] (e' : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e'] (J : TauCeti.ContMDiffAlmostComplexStructure I n M) {x : M} (hx : x ∈ e.baseSet) (hx' : x ∈ e'.baseSet) : e'.almostComplexCoordinates J x = ↑(coordChangeL ℝ e e' x) ∘SL e.almostComplexCoordinates J x ∘SL ↑(coordChangeL ℝ e' e x)

Coordinate readings in two tangent frames are conjugate by the native frame transition. The hypotheses are precisely membership in the two frame domains.

noncomputable def Bundle.Trivialization.almostComplexEquiv {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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] {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] (he : e.baseSet = Set.univ) (h : Diffeomorph I I' M N ↑n) : TauCeti.ContMDiffAlmostComplexStructure I n M ≃ { A : ContMDiffMap I' (modelWithCornersSelf ℝ (E →L[ℝ] E)) N (E →L[ℝ] E) ↑n // ∀ (x : N) (v : E), (A x) ((A x) v) = -v }

In a globally covering tangent frame and any Cⁿ base coordinates, native structures correspond exactly to finite-regularity endomorphism fields squaring to minus the identity.

theorem Bundle.Trivialization.almostComplexEquiv_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] {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] (he : e.baseSet = Set.univ) (h : Diffeomorph I I' M N ↑n) (J : TauCeti.ContMDiffAlmostComplexStructure I n M) (y : N) : ↑((e.almostComplexEquiv he h) J) y = e.almostComplexCoordinates J (h.symm y)

The coordinate equivalence reads the field at the inverse base coordinate.

theorem Bundle.Trivialization.almostComplexEquiv_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 : ℕ∞} (e : Trivialization E TotalSpace.proj) [MemTrivializationAtlas e] {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] (he : e.baseSet = Set.univ) (h : Diffeomorph I I' M N ↑n) (A : { A : ContMDiffMap I' (modelWithCornersSelf ℝ (E →L[ℝ] E)) N (E →L[ℝ] E) ↑n // ∀ (x : N) (v : E), (A x) ((A x) v) = -v }) (x : M) (v : TangentSpace I x) : (fun (x : M) => ⇑(((e.almostComplexEquiv he h).symm A).toEndomorphism x)) x v = (symmL ℝ e x) ((↑A (h x)) ((continuousLinearMapAt ℝ e x) v))

The inverse equivalence conjugates through the tangent frame at the forward base coordinate.