Block almost complex structures in a product trivialization

In a smooth product trivialization B × V over a base B carrying a constant complex structure i, a smooth almost complex structure J makes the projection Prod.fst : B × V → B pseudoholomorphic precisely when J has the lower-triangular block form

J(p)(a, v) = (i a, α(p) a + j(p) v)

(TauCeti.ComplexStructureFamily.blockEndomorphism i α j p), where at each point p : B × V the fibre block j(p) is an almost complex structure on V and the connection block α(p) is (i, j(p))-complex-antilinear, α(p)(i a) + j(p)(α(p) a) = 0.

This file builds both directions of that correspondence on arbitrary real normed spaces B and V (without finite-dimensionality assumptions):

• blockEndomorphism_comp_self_eq_neg_id_iff characterizes when blockEndomorphism i α j p squares to -1 in terms of i² = -1, j(p)² = -1, and α(p)(i a) + j(p)(α(p) a) = 0 (equivalently IsComplexAntilinear, TauCeti.isComplexAntilinear_iff_apply_add_apply_eq_zero);
• blockAlmostComplexStructure bundles smooth α and j satisfying these identities into a SmoothAlmostComplexStructure 𝓘(ℝ, B × V) (B × V) whose projection Prod.fst is pseudoholomorphic (isPseudoholomorphic_fst_blockAlmostComplexStructure);
• conversely, connectionBlock and fiberBlock extract smooth blocks from any J : SmoothAlmostComplexStructure 𝓘(ℝ, B × V) (B × V), and isPseudoholomorphicAt_fst_iff_toEndomorphism_eq_blockEndomorphism proves that Prod.fst is pseudoholomorphic at p if and only if J equals blockEndomorphism i (connectionBlock J) (fiberBlock J) at p.

For the manifold-level diagonal (α = 0) product family on P × M, see TauCeti.SmoothAlmostComplexStructure.prodFamily.

Main declarations

• TauCeti.ComplexStructureFamily.blockEndomorphism_comp_self_eq_neg_id_iff: block square -1 criterion.
• TauCeti.ComplexStructureFamily.blockAlmostComplexStructure: smooth almost complex structure associated to (i, α, j).
• TauCeti.ComplexStructureFamily.connectionBlock, TauCeti.ComplexStructureFamily.fiberBlock: the off-diagonal and vertical blocks of an almost complex structure on B × V.
• TauCeti.ComplexStructureFamily.isPseudoholomorphicAt_fst_iff_toEndomorphism_eq_blockEndomorphism and ComplexStructureFamily.isPseudoholomorphic_fst_iff_toEndomorphism_eq_blockEndomorphism: characterization of block structures via pseudoholomorphy of Prod.fst.

References

• J. W. Robbin and D. A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699, Section 8.9.
• J. W. Robbin and D. A. Salamon, Corrigendum to A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 9 (2007), 901–905.

Algebraic structure and regularity of blockEndomorphism

theorem TauCeti.ComplexStructureFamily.blockEndomorphism_comp_self_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p w : B × V) : (blockEndomorphism i α j p) ((blockEndomorphism i α j p) w) = (i (i w.1), (α p) (i w.1) + (j p) ((α p) w.1) + (j p) ((j p) w.2))

Applying blockEndomorphism i α j p twice yields (i (i w.1), α p (i w.1) + j p (α p w.1) + j p (j p w.2)).

theorem TauCeti.ComplexStructureFamily.blockEndomorphism_comp_self_eq_neg_id_iff {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) : blockEndomorphism i α j p ∘SL blockEndomorphism i α j p = -ContinuousLinearMap.id ℝ (B × V) ↔ (∀ (a : B), i (i a) = -a) ∧ (∀ (v : V), (j p) ((j p) v) = -v) ∧ ∀ (a : B), (α p) (i a) + (j p) ((α p) a) = 0

The block endomorphism [[i, 0], [α, j]] at p squares to -1 if and only if i² = -1, j(p)² = -1, and α(p)(i a) + j(p)(α(p) a) = 0 for all a.

theorem TauCeti.ComplexStructureFamily.contDiffWithinAt_blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} {s : Set (B × V)} {p : B × V} (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hα : ContDiffWithinAt ℝ n α s p) (hj : ContDiffWithinAt ℝ n j s p) : ContDiffWithinAt ℝ n (blockEndomorphism i α j) s p

theorem TauCeti.ComplexStructureFamily.contDiffAt_blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} {p : B × V} (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hα : ContDiffAt ℝ n α p) (hj : ContDiffAt ℝ n j p) : ContDiffAt ℝ n (blockEndomorphism i α j) p

theorem TauCeti.ComplexStructureFamily.contDiff_blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hα : ContDiff ℝ n α) (hj : ContDiff ℝ n j) : ContDiff ℝ n (blockEndomorphism i α j)

Smooth block almost complex structures and projection characterization

def TauCeti.ComplexStructureFamily.blockAlmostComplexStructure {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (hα : ContDiff ℝ (↑⊤) α) (hj : ContDiff ℝ (↑⊤) j) (hi : ∀ (a : B), i (i a) = -a) (hj_sq : ∀ (p : B × V) (v : V), (j p) ((j p) v) = -v) (hαj : ∀ (p : B × V) (a : B), (α p) (i a) + (j p) ((α p) a) = 0) : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)

Construct a SmoothAlmostComplexStructure on B × V from a constant base complex structure i, a smooth connection block α, and a smooth fibre almost complex structure family j satisfying α(p)(i a) + j(p)(α(p) a) = 0.

@[simp]

theorem TauCeti.ComplexStructureFamily.blockAlmostComplexStructure_toEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (hα : ContDiff ℝ (↑⊤) α) (hj : ContDiff ℝ (↑⊤) j) (hi : ∀ (a : B), i (i a) = -a) (hj_sq : ∀ (p : B × V) (v : V), (j p) ((j p) v) = -v) (hαj : ∀ (p : B × V) (a : B), (α p) (i a) + (j p) ((α p) a) = 0) (p : B × V) : (blockAlmostComplexStructure i α j hα hj hi hj_sq hαj).toEndomorphism p = blockEndomorphism i α j p

theorem TauCeti.ComplexStructureFamily.blockAlmostComplexStructure_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (hα : ContDiff ℝ (↑⊤) α) (hj : ContDiff ℝ (↑⊤) j) (hi : ∀ (a : B), i (i a) = -a) (hj_sq : ∀ (p : B × V) (v : V), (j p) ((j p) v) = -v) (hαj : ∀ (p : B × V) (a : B), (α p) (i a) + (j p) ((α p) a) = 0) (p w : B × V) : (fun (x : B × V) => ⇑((blockAlmostComplexStructure i α j hα hj hi hj_sq hαj).toEndomorphism x)) p w = (i w.1, (α p) w.1 + (j p) w.2)

theorem TauCeti.ComplexStructureFamily.isPseudoholomorphic_fst_blockAlmostComplexStructure {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (hα : ContDiff ℝ (↑⊤) α) (hj : ContDiff ℝ (↑⊤) j) (hi : ∀ (a : B), i (i a) = -a) (hj_sq : ∀ (p : B × V) (v : V), (j p) ((j p) v) = -v) (hαj : ∀ (p : B × V) (a : B), (α p) (i a) + (j p) ((α p) a) = 0) : IsPseudoholomorphic (blockAlmostComplexStructure i α j hα hj hi hj_sq hαj) (SmoothAlmostComplexStructure.const i hi) Prod.fst

For a smooth block almost complex structure, the base projection Prod.fst : B × V → B is pseudoholomorphic.

noncomputable def TauCeti.ComplexStructureFamily.connectionBlock {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (p : B × V) : B →L[ℝ] V

The off-diagonal connection block a ↦ (J(p)(a, 0)).2 of a smooth almost complex structure on B × V.

noncomputable def TauCeti.ComplexStructureFamily.fiberBlock {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (p : B × V) : V →L[ℝ] V

The vertical fibre block v ↦ (J(p)(0, v)).2 of a smooth almost complex structure on B × V.

@[simp]

theorem TauCeti.ComplexStructureFamily.connectionBlock_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (p : B × V) (a : B) : (connectionBlock J p) a = ((fun (x : B × V) => ⇑(J.toEndomorphism x)) p (a, 0)).2

@[simp]

theorem TauCeti.ComplexStructureFamily.fiberBlock_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (p : B × V) (v : V) : (fiberBlock J p) v = ((fun (x : B × V) => ⇑(J.toEndomorphism x)) p (0, v)).2

@[simp]

theorem TauCeti.ComplexStructureFamily.connectionBlock_blockAlmostComplexStructure {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (hα : ContDiff ℝ (↑⊤) α) (hj : ContDiff ℝ (↑⊤) j) (hi : ∀ (a : B), i (i a) = -a) (hj_sq : ∀ (p : B × V) (v : V), (j p) ((j p) v) = -v) (hαj : ∀ (p : B × V) (a : B), (α p) (i a) + (j p) ((α p) a) = 0) : connectionBlock (blockAlmostComplexStructure i α j hα hj hi hj_sq hαj) = α

@[simp]

theorem TauCeti.ComplexStructureFamily.fiberBlock_blockAlmostComplexStructure {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (hα : ContDiff ℝ (↑⊤) α) (hj : ContDiff ℝ (↑⊤) j) (hi : ∀ (a : B), i (i a) = -a) (hj_sq : ∀ (p : B × V) (v : V), (j p) ((j p) v) = -v) (hαj : ∀ (p : B × V) (a : B), (α p) (i a) + (j p) ((α p) a) = 0) : fiberBlock (blockAlmostComplexStructure i α j hα hj hi hj_sq hαj) = j

theorem TauCeti.ComplexStructureFamily.contDiff_connectionBlock {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) : ContDiff ℝ (↑⊤) (connectionBlock J)

theorem TauCeti.ComplexStructureFamily.contDiff_fiberBlock {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) : ContDiff ℝ (↑⊤) (fiberBlock J)

theorem TauCeti.ComplexStructureFamily.isPseudoholomorphicAt_fst_iff {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (hi : ∀ (a : B), i (i a) = -a) (p : B × V) : IsPseudoholomorphicAt J (SmoothAlmostComplexStructure.const i hi) Prod.fst p ↔ ∀ (w : B × V), ((fun (x : B × V) => ⇑(J.toEndomorphism x)) p w).1 = i w.1

The projection Prod.fst : B × V → B is pseudoholomorphic at p from J to the constant structure i if and only if (J p w).1 = i w.1 for every w.

theorem TauCeti.ComplexStructureFamily.isPseudoholomorphicAt_fst_iff_toEndomorphism_eq_blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (hi : ∀ (a : B), i (i a) = -a) (p : B × V) : IsPseudoholomorphicAt J (SmoothAlmostComplexStructure.const i hi) Prod.fst p ↔ J.toEndomorphism p = blockEndomorphism i (connectionBlock J) (fiberBlock J) p

A smooth almost complex structure J on B × V agrees at p with blockEndomorphism i (connectionBlock J) (fiberBlock J) p if and only if Prod.fst is pseudoholomorphic at p.

theorem TauCeti.ComplexStructureFamily.fiberBlock_apply_apply_and_connectionBlock_anticommute {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (hi : ∀ (a : B), i (i a) = -a) {p : B × V} (hp : IsPseudoholomorphicAt J (SmoothAlmostComplexStructure.const i hi) Prod.fst p) : (∀ (v : V), (fiberBlock J p) ((fiberBlock J p) v) = -v) ∧ ∀ (a : B), (connectionBlock J p) (i a) + (fiberBlock J p) ((connectionBlock J p) a) = 0

When Prod.fst is pseudoholomorphic at p, the extracted blocks satisfy j(p)² = -1 and α(p)(i a) + j(p)(α(p) a) = 0.

theorem TauCeti.ComplexStructureFamily.isPseudoholomorphic_fst_iff_toEndomorphism_eq_blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (hi : ∀ (a : B), i (i a) = -a) : IsPseudoholomorphic J (SmoothAlmostComplexStructure.const i hi) Prod.fst ↔ ∀ (p : B × V), J.toEndomorphism p = blockEndomorphism i (connectionBlock J) (fiberBlock J) p

Global characterization: Prod.fst : B × V → B is pseudoholomorphic if and only if J is the block almost complex structure built from i, connectionBlock J, and fiberBlock J.

theorem TauCeti.ComplexStructureFamily.eq_blockAlmostComplexStructure_of_isPseudoholomorphic_fst {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (hi : ∀ (a : B), i (i a) = -a) (hJ : IsPseudoholomorphic J (SmoothAlmostComplexStructure.const i hi) Prod.fst) : J = blockAlmostComplexStructure i (connectionBlock J) (fiberBlock J) ⋯ ⋯ hi ⋯ ⋯

Reconstructing J as blockAlmostComplexStructure when Prod.fst is pseudoholomorphic.