Finite-regularity block almost complex structures

On P × M, combine a Cⁿ almost complex structure on P with a jointly Cⁿ family of almost complex structures on T_x M, allowed to depend on both p and x. The result acts diagonally under the canonical product tangent identification. In particular, for P = ℝ × ℝ with its standard structure, it sends (a, b, v) to (-b, a, J_(s,t,x) v). The order n : ℕ∞ includes continuous structures and the smooth endpoint. The vertical regularity is that of an endomorphism section along P × M → M; it does not assert an almost complex structure on the full product tangent bundle. familySlice restricts it to a native structure on M at each parameter. The block construction combines it with the chosen horizontal structure. This permits time-dependent vertical structures in suspensions without requiring the monodromy to preserve one fixed almost complex structure.

The native finite construction has evaluation, square, downgrade, negation and ordinary-product APIs, and preserves joint parameter dependence without derivative loss. The existing smooth construction specializes this one at infinite order. The evaluation formula splits the quadratic form into horizontal and vertical terms. Compatible vertical families therefore give a compatible block structure for the product two-form. When the vertical family also depends smoothly on a parameter, so does the block structure (TauCeti.SmoothAlmostComplexStructure.contMDiff_prodFamily_family). Equivariance under a product map reduces to equivariance of its two blocks; for a translation and a monodromy map this is precisely the vertical seam equation.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, second edition, Section 2.2 (compatible almost complex structures).
• M. Hutchings and M. Sullivan, The periodic Floer homology of a Dehn twist, Algebraic & Geometric Topology 5 (2005), 301–354 (block structures on suspensions).

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) : ContMDiffAlmostComplexStructure (I.prod I') n (P × M)

The Cⁿ block structure on P × M with horizontal block J and a jointly Cⁿ vertical family K_(p,x). The vertical block may depend on both coordinates.

theorem TauCeti.ContMDiffAlmostComplexStructure.contMDiff_prodFamily_family {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) {EΛ : Type u_7} {HΛ : Type u_8} {Λ : Type u_9} [NormedAddCommGroup EΛ] [NormedSpace ℝ EΛ] [TopologicalSpace HΛ] {IΛ : ModelWithCorners ℝ EΛ HΛ} [TopologicalSpace Λ] [ChartedSpace HΛ Λ] {K : Λ → (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)} (hK : ContMDiff (IΛ.prod (I.prod I')) (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (r : Λ × P × M) => ⟨r.2.2, LinearMap.toContinuousLinearMap (K r.1 r.2).toLinearMap⟩) : ContMDiff (IΛ.prod (I.prod I')) ((I.prod I').prod (modelWithCornersSelf ℝ (E × F →L[ℝ] E × F))) ↑n fun (r : Λ × P × M) => ⟨r.2, (J.prodFamily (K r.1) ⋯).toEndomorphism r.2⟩

A jointly Cⁿ vertical family gives a jointly Cⁿ block family as a tangent-endomorphism section along Λ × (P × M) → P × M. No derivatives are lost, including at n = 0.

theorem TauCeti.ContMDiffAlmostComplexStructure.prodFamily_apply {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (p : P × M) (v : TangentSpace (I.prod I') p) : (fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) p v = (Manifold.tangentSpaceProdEquiv p).symm ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 ((Manifold.tangentSpaceProdEquiv p) v).1, (K p).toLinearMap ((Manifold.tangentSpaceProdEquiv p) v).2)

A block structure acts separately on the two components of a product tangent vector.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.prodFamily_toEndomorphism_apply {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (p : P × M) : (J.prodFamily K hK).toEndomorphism p = (J.toEndomorphism p.1).prodMap (LinearMap.toContinuousLinearMap (K p).toLinearMap)

The endomorphism of the block structure is the continuous linear block map.

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.familySlice {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (p : P) : ContMDiffAlmostComplexStructure I' n M

A domain-dependent structure over P restricts at each parameter to a native Cⁿ structure on M. Its joint regularity is along P × M → M, not on the full tangent bundle of P × M.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.familySlice_toEndomorphism_apply {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (p : P) (x : M) : (familySlice K hK p).toEndomorphism x = LinearMap.toContinuousLinearMap (K (p, x)).toLinearMap

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.familySlice_ofLE {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {m : ℕ∞} (hmn : m ≤ n) (p : P) : (familySlice K hK p).ofLE hmn = familySlice K ⋯ p

Forgetting regularity commutes with slicing a domain-dependent family.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.prodFamily_ofLE {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {m : ℕ∞} (hmn : m ≤ n) : (J.prodFamily K hK).ofLE hmn = (J.ofLE hmn).prodFamily K ⋯

Forgetting regularity commutes with the block construction.

theorem TauCeti.ContMDiffAlmostComplexStructure.contMDiff_neg_family {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (-K p).toLinearMap⟩

Negation preserves joint regularity for a domain-dependent almost complex structure.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.familySlice_neg {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (p : P) : familySlice (fun (q : P × M) => -K q) ⋯ p = -familySlice K hK p

Negation commutes with restricting a domain-dependent family at a parameter.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.prodFamily_neg {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) : (-J).prodFamily (fun (p : P × M) => -K p) ⋯ = -J.prodFamily K hK

Negating both blocks negates the block structure.

noncomputable def TauCeti.ContMDiffAlmostComplexStructure.prod {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (L : ContMDiffAlmostComplexStructure I' n M) : ContMDiffAlmostComplexStructure (I.prod I') n (P × M)

The ordinary product is the domain-independent vertical special case.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.prod_apply {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (L : ContMDiffAlmostComplexStructure I' n M) (p : P × M) (v : TangentSpace (I.prod I') p) : (fun (x : P × M) => ⇑((J.prod L).toEndomorphism x)) p v = (Manifold.tangentSpaceProdEquiv p).symm ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 ((Manifold.tangentSpaceProdEquiv p) v).1, (fun (x : M) => ⇑(L.toEndomorphism x)) p.2 ((Manifold.tangentSpaceProdEquiv p) v).2)

The ordinary product acts componentwise under the canonical tangent identification.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.prod_ofLE {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (L : ContMDiffAlmostComplexStructure I' n M) {m : ℕ∞} (hmn : m ≤ n) : (J.prod L).ofLE hmn = (J.ofLE hmn).prod (L.ofLE hmn)

Forgetting regularity commutes with the ordinary product.

@[simp]

theorem TauCeti.ContMDiffAlmostComplexStructure.prod_neg {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (L : ContMDiffAlmostComplexStructure I' n M) : (-J).prod (-L) = -J.prod L

Negating both factors negates the ordinary product.

theorem TauCeti.ContMDiffAlmostComplexStructure.eval₂_prod_prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (σ : SmoothTwoForm I P) (τ : SmoothTwoForm I' M) (p : P × M) (v : TangentSpace (I.prod I') p) : SmoothBundleForm.eval₂ (σ.prod τ) p v ((fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) p v) = SmoothBundleForm.eval₂ σ p.1 ((Manifold.tangentSpaceProdEquiv p) v).1 ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 ((Manifold.tangentSpaceProdEquiv p) v).1) + SmoothBundleForm.eval₂ τ p.2 ((Manifold.tangentSpaceProdEquiv p) v).2 ((K p).toLinearMap ((Manifold.tangentSpaceProdEquiv p) v).2)

The quadratic form of a product two-form and a block almost complex structure is the sum of its horizontal and vertical quadratic forms.

theorem TauCeti.ContMDiffAlmostComplexStructure.mfderiv_prodMap_prodFamily_iff {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] {n : ℕ∞} (J : ContMDiffAlmostComplexStructure I n P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑n fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {f : P → P} {g : M → M} (p : P × M) (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) : (∀ (v : TangentSpace (I.prod I') p), (mfderiv% (Prod.map f g) p) ((fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) p v) = (fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) (f p.1, g p.2) ((mfderiv% (Prod.map f g) p) v)) ↔ (∀ (u : TangentSpace I p.1), (mfderiv% f p.1) ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 u) = (fun (x : P) => ⇑(J.toEndomorphism x)) (f p.1) ((mfderiv% f p.1) u)) ∧ ∀ (w : TangentSpace I' p.2), (mfderiv% g p.2) ((K p).toLinearMap w) = (K (f p.1, g p.2)).toLinearMap ((mfderiv% g p.2) w)

A product map intertwines the block structure at a point precisely when its horizontal differential intertwines J and its vertical differential intertwines the corresponding members of K. In a suspension the second condition is the seam equation.

noncomputable def TauCeti.SmoothAlmostComplexStructure.prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) : SmoothAlmostComplexStructure (I.prod I') (P × M)

The smooth block structure, obtained from the native finite-regularity construction at infinite order. The vertical block may depend jointly on the domain and target point.

theorem TauCeti.SmoothAlmostComplexStructure.contMDiff_prodFamily_family {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) {EΛ : Type u_7} {HΛ : Type u_8} {Λ : Type u_9} [NormedAddCommGroup EΛ] [NormedSpace ℝ EΛ] [TopologicalSpace HΛ] {IΛ : ModelWithCorners ℝ EΛ HΛ} [TopologicalSpace Λ] [ChartedSpace HΛ Λ] {K : Λ → (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)} (hK : ContMDiff (IΛ.prod (I.prod I')) (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (r : Λ × P × M) => ⟨r.2.2, LinearMap.toContinuousLinearMap (K r.1 r.2).toLinearMap⟩) : ContMDiff (IΛ.prod (I.prod I')) ((I.prod I').prod (modelWithCornersSelf ℝ (E × F →L[ℝ] E × F))) ↑⊤ fun (r : Λ × P × M) => ⟨r.2, (J.prodFamily (K r.1) ⋯).toEndomorphism r.2⟩

Jointly smooth vertical families give jointly smooth block structures.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.prodFamily_apply {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (p : P × M) (v : TangentSpace (I.prod I') p) : (fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) p v = (Manifold.tangentSpaceProdEquiv p).symm ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 ((Manifold.tangentSpaceProdEquiv p) v).1, (K p).toLinearMap ((Manifold.tangentSpaceProdEquiv p) v).2)

A smooth block structure acts separately on the two tangent components.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.prodFamily_toContMDiff {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (n : ℕ∞) : (J.prodFamily K hK).toContMDiff n = (J.toContMDiff n).prodFamily K ⋯

Viewing the smooth block construction at finite regularity gives the native finite block construction. This includes the infinite-order equivalence with the smooth carrier.

theorem TauCeti.SmoothAlmostComplexStructure.eval₂_prod_prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (σ : SmoothTwoForm I P) (τ : SmoothTwoForm I' M) (p : P × M) (v : TangentSpace (I.prod I') p) : SmoothBundleForm.eval₂ (σ.prod τ) p v ((fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) p v) = SmoothBundleForm.eval₂ σ p.1 ((Manifold.tangentSpaceProdEquiv p) v).1 ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 ((Manifold.tangentSpaceProdEquiv p) v).1) + SmoothBundleForm.eval₂ τ p.2 ((Manifold.tangentSpaceProdEquiv p) v).2 ((K p).toLinearMap ((Manifold.tangentSpaceProdEquiv p) v).2)

The quadratic form of a product two-form and a block almost complex structure is the sum of its horizontal and vertical quadratic forms.

theorem TauCeti.SmoothAlmostComplexStructure.tames_prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {σ : SmoothTwoForm I P} {τ : SmoothTwoForm I' M} (hσ : σ.Tames J) (hτ : ∀ (p : P × M) (v : TangentSpace I' p.2), v ≠ 0 → 0 < SmoothBundleForm.eval₂ τ p.2 v ((K p).toLinearMap v)) : (σ.prod τ).Tames (J.prodFamily K hK)

If each block is tamed by its factor two-form, the block structure is tamed by the product form.

theorem TauCeti.SmoothAlmostComplexStructure.invariant_prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {σ : SmoothTwoForm I P} {τ : SmoothTwoForm I' M} (hσ : σ.Invariant J) (hτ : ∀ (p : P × M) (v w : TangentSpace I' p.2), SmoothBundleForm.eval₂ τ p.2 ((K p).toLinearMap v) ((K p).toLinearMap w) = SmoothBundleForm.eval₂ τ p.2 v w) : (σ.prod τ).Invariant (J.prodFamily K hK)

Invariance of each block gives invariance of the product form.

theorem TauCeti.SmoothAlmostComplexStructure.compatible_prodFamily {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {σ : SmoothTwoForm I P} {τ : SmoothTwoForm I' M} (hσ : σ.Compatible J) (hτ : τ.IsNondegenerate) (hcompat : ∀ (p : P × M), (hτ.symplecticFormAt p.2).Compatible (K p)) : (σ.prod τ).Compatible (J.prodFamily K hK)

Compatible vertical families and a compatible horizontal block give a block structure compatible with the product two-form.

theorem TauCeti.SmoothAlmostComplexStructure.mfderiv_prodMap_prodFamily_iff {E : Type u_1} {H : Type u_2} {P : Type u_3} {F : Type u_4} {H' : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (J : SmoothAlmostComplexStructure I P) (K : (p : P × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff (I.prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : P × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) {f : P → P} {g : M → M} (p : P × M) (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) : (∀ (v : TangentSpace (I.prod I') p), (mfderiv% (Prod.map f g) p) ((fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) p v) = (fun (x : P × M) => ⇑((J.prodFamily K hK).toEndomorphism x)) (f p.1, g p.2) ((mfderiv% (Prod.map f g) p) v)) ↔ (∀ (u : TangentSpace I p.1), (mfderiv% f p.1) ((fun (x : P) => ⇑(J.toEndomorphism x)) p.1 u) = (fun (x : P) => ⇑(J.toEndomorphism x)) (f p.1) ((mfderiv% f p.1) u)) ∧ ∀ (w : TangentSpace I' p.2), (mfderiv% g p.2) ((K p).toLinearMap w) = (K (f p.1, g p.2)).toLinearMap ((mfderiv% g p.2) w)

A product map intertwines the block structure at a point precisely when its horizontal differential intertwines J and its vertical differential intertwines the corresponding members of K. In a suspension the second condition is the seam equation.

theorem TauCeti.SmoothAlmostComplexStructure.eval₂_prod_prodFamily_standard {F : Type u_1} {H' : Type u_2} {M : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (K : (p : (ℝ × ℝ) × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff ((modelWithCornersSelf ℝ (ℝ × ℝ)).prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : (ℝ × ℝ) × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (τ : SmoothTwoForm I' M) (p : (ℝ × ℝ) × M) (v : TangentSpace ((modelWithCornersSelf ℝ (ℝ × ℝ)).prod I') p) : SmoothBundleForm.eval₂ (stdSymplecticForm.constSmooth.prod τ) p v ((fun (x : (ℝ × ℝ) × M) => ⇑(((AlmostComplexStructure.product ℝ).constSmooth.prodFamily K hK).toEndomorphism x)) p v) = ((NormedSpace.fromTangentSpace p.1) ((Manifold.tangentSpaceProdEquiv p) v).1).1 ^ 2 + ((NormedSpace.fromTangentSpace p.1) ((Manifold.tangentSpaceProdEquiv p) v).1).2 ^ 2 + SmoothBundleForm.eval₂ τ p.2 ((Manifold.tangentSpaceProdEquiv p) v).2 ((K p).toLinearMap ((Manifold.tangentSpaceProdEquiv p) v).2)

For the standard horizontal block J∂s = ∂t, J∂t = -∂s, the quadratic form of ds ∧ dt + τ is a² + b² + τ(v, K v). The vertical family is arbitrary and may depend on both time coordinates.

theorem TauCeti.SmoothAlmostComplexStructure.mfderiv_translation_prodFamily_iff {F : Type u_1} {H' : Type u_2} {M : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H'] {I' : ModelWithCorners ℝ F H'} [TopologicalSpace M] [ChartedSpace H' M] [IsManifold I' (↑⊤) M] (K : (p : (ℝ × ℝ) × M) → AlmostComplexStructure (TangentSpace I' p.2)) (hK : ContMDiff ((modelWithCornersSelf ℝ (ℝ × ℝ)).prod I') (I'.prod (modelWithCornersSelf ℝ (F →L[ℝ] F))) ↑⊤ fun (p : (ℝ × ℝ) × M) => ⟨p.2, LinearMap.toContinuousLinearMap (K p).toLinearMap⟩) (c : ℝ × ℝ) (g : Diffeomorph I' I' M M ↑⊤) (p : (ℝ × ℝ) × M) : (∀ (v : TangentSpace ((modelWithCornersSelf ℝ (ℝ × ℝ)).prod I') p), (mfderiv% (Prod.map (fun (q : ℝ × ℝ) => q + c) ⇑g) p) ((fun (x : (ℝ × ℝ) × M) => ⇑(((AlmostComplexStructure.product ℝ).constSmooth.prodFamily K hK).toEndomorphism x)) p v) = (fun (x : (ℝ × ℝ) × M) => ⇑(((AlmostComplexStructure.product ℝ).constSmooth.prodFamily K hK).toEndomorphism x)) (p.1 + c, g p.2) ((mfderiv% (Prod.map (fun (q : ℝ × ℝ) => q + c) ⇑g) p) v)) ↔ ∀ (w : TangentSpace I' p.2), (mfderiv% ⇑g p.2) ((K p).toLinearMap w) = (K (p.1 + c, g p.2)).toLinearMap ((mfderiv% ⇑g p.2) w)

Under a translation of the time plane and a fibre diffeomorphism g, the standard block structure is invariant exactly when its vertical family obeys the seam equation. Taking c = (0, 1) and g = φ.symm gives the mapping-torus deck generator; taking c = (1, 0) and g = Diffeomorph.refl I' M ∞ gives the other time-circle generator.