Parametric transversality for Fredholm bundle sections

Let M be a Banach manifold, Λ a Banach space of parameters, and s a section along a map b : M × Λ → B to the base of a vector bundle. A parameter l is regular when the section s (·, l) of the restricted bundle is regular: its intrinsic linearization is surjective at every one of its zeros. If the linearization of s in the M direction is Fredholm and the total linearization is surjective at every zero, the regular parameters form a residual set, hence a dense set for Banach Λ. For such a parameter the zeros of s (·, l) then form a C^n manifold whose dimension is the Fredholm index. This is the abstract transversality package used to show that moduli spaces cut out by a generic perturbation are manifolds.

If the slice linearizations have negative index at all zeros, regularity is equivalent to absence of zeros. Thus zero-free parameters form a residual, dense set: a negative expected dimension means an empty moduli space. The index need not be constant, and its sign is required only at actual zeros.

Smoothness of the section is required only at zeros, and all hypotheses are stated for the intrinsic linearizations. The manifold structure on the zeros also uses a smooth bundle. The finite differentiability threshold is Smale's, n > max (index, 0) for the index of the linearization in the M direction. No norm on the individual bundle fibers is needed.

The proof reads the section in a source chart and a bundle trivialization at each zero, applies the local parametric theorem for Banach-space equations to that coordinate expression, and takes a countable cover of the actual section zero set. Zeros of a coordinate expression outside its chart or trivialization are never treated as section zeros. Away from the centre of the chart, the coordinate derivative in the M direction is the intrinsic one followed by the derivative of the inverse chart, so non-regular section zeros give non-regular coordinate zeros.

Main results

• TauCeti.isMeagre_setOf_not_isRegularSectionParameter: the non-regular parameters are meagre.
• TauCeti.dense_setOf_isRegularSectionParameter: regular parameters are dense.
• TauCeti.eventually_residual_exists_isManifold_sectionZero: for a residual set of parameters, the zeros form a C^n manifold of dimension the index, with a C^n immersion whose tangent spaces are the kernels.
• TauCeti.isRegularSectionParameter_iff_forall_ne_zero_of_index_neg: with negative slice indices at zeros, regularity is equivalent to absence of zeros.
• TauCeti.mem_residual_setOf_forall_section_ne_zero_of_index_neg and TauCeti.dense_setOf_forall_section_ne_zero_of_index_neg: zero-free parameters form a residual, dense set when the slice indices at zeros are negative.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3 (Theorem A.3.6 and its proof).
• S. Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965), 861--866.

The local analytic input is TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_not_surjective_levelSetParameterMap.

def TauCeti.IsRegularSectionParameter (X : Type u_1) {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] (b : M × Λ → B) (s : (z : M × Λ) → E (b z)) (l : Λ) : Prop

A parameter l is regular for a section along b : M × Λ → B when the section s (·, l) along b (·, l) has surjective intrinsic linearization at each of its zeros. Regularity of the total linearization is a separate condition.

theorem TauCeti.isRegularSectionParameter_iff {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} {l : Λ} : IsRegularSectionParameter X b s l ↔ ∀ (x : M), s (x, l) = 0 → Function.Surjective ⇑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, l)) (fun (y : M) => s (y, l)) x)

Characterization of a regular parameter by the linearizations at its zeros.

theorem TauCeti.isRegularSectionParameter_iff_forall_ne_zero_of_index_neg {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} {l : Λ} (hindex : ∀ (x : M), s (x, l) = 0 → (↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, l)) (fun (y : M) => s (y, l)) x)).index < 0) : IsRegularSectionParameter X b s l ↔ ∀ (x : M), s (x, l) ≠ 0

When every zero of a parameter slice has negative index, the parameter is regular if and only if that slice has no zeros. This implication needs no smoothness or Fredholm assumption: surjectivity alone forces the algebraic index to be nonnegative.

@[simp]

theorem TauCeti.isRegularSectionParameter_trivial {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace B] (b : M × Λ → B) (f : M × Λ → F) (l : Λ) : IsRegularSectionParameter X b f l ↔ ∀ (x : M), f (x, l) = 0 → Function.Surjective ⇑((d% fun (y : M) => f (y, l)) x)

In a trivial bundle, a parameter is regular exactly when the fiber-valued equation f (·, l) = 0 has surjective manifold derivative at each of its solutions.

theorem TauCeti.isMeagre_setOf_not_isRegularSectionParameter {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6} {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB] [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F] [IsManifold (modelWithCornersSelf ℝ X) 1 M] [SecondCountableTopology ↑{z : M × Λ | s z = 0}] {n : WithTop ℕ∞} (hcont : ∀ (z : M × Λ), s z = 0 → ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) (I.prod (modelWithCornersSelf ℝ F)) n (fun (w : M × Λ) => ⟨b w, s w⟩) z) (hFred : ∀ (z : M × Λ), s z = 0 → (sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1).IsFredholm) (htotal : ∀ (z : M × Λ), s z = 0 → Function.Surjective ⇑(sectionLinearization ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z)) (hn : ∀ (z : M × Λ), s z = 0 → ↑((↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index.toNat + 1) ≤ n) : IsMeagre {l : Λ | ¬IsRegularSectionParameter X b s l}

Parametric transversality for bundle sections. Non-regular parameters are meagre when the total linearization is surjective and the linearization in the M direction is Fredholm at every zero. Second countability is needed only for the actual universal zero set.

At each zero the section must be C^k for Smale's threshold k > max (i, 0), where i is the index of the slice linearization.

theorem TauCeti.mem_residual_setOf_isRegularSectionParameter {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6} {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB] [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F] [IsManifold (modelWithCornersSelf ℝ X) 1 M] [SecondCountableTopology ↑{z : M × Λ | s z = 0}] {n : WithTop ℕ∞} (hcont : ∀ (z : M × Λ), s z = 0 → ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) (I.prod (modelWithCornersSelf ℝ F)) n (fun (w : M × Λ) => ⟨b w, s w⟩) z) (hFred : ∀ (z : M × Λ), s z = 0 → (sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1).IsFredholm) (htotal : ∀ (z : M × Λ), s z = 0 → Function.Surjective ⇑(sectionLinearization ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z)) (hn : ∀ (z : M × Λ), s z = 0 → ↑((↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index.toNat + 1) ≤ n) : {l : Λ | IsRegularSectionParameter X b s l} ∈ residual Λ

Regular parameters of a universal Fredholm bundle section form a residual set.

theorem TauCeti.dense_setOf_isRegularSectionParameter {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6} {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB] [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F] [IsManifold (modelWithCornersSelf ℝ X) 1 M] [SecondCountableTopology ↑{z : M × Λ | s z = 0}] {n : WithTop ℕ∞} (hcont : ∀ (z : M × Λ), s z = 0 → ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) (I.prod (modelWithCornersSelf ℝ F)) n (fun (w : M × Λ) => ⟨b w, s w⟩) z) (hFred : ∀ (z : M × Λ), s z = 0 → (sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1).IsFredholm) (htotal : ∀ (z : M × Λ), s z = 0 → Function.Surjective ⇑(sectionLinearization ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z)) (hn : ∀ (z : M × Λ), s z = 0 → ↑((↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index.toNat + 1) ≤ n) : Dense {l : Λ | IsRegularSectionParameter X b s l}

Regular parameters of a universal Fredholm bundle section are dense in the Banach parameter space.

theorem TauCeti.eventually_residual_exists_isManifold_sectionZero {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6} {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB] [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F] [SecondCountableTopology ↑{z : M × Λ | s z = 0}] {n : WithTop ℕ∞} (hcont : ∀ (z : M × Λ), s z = 0 → ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) (I.prod (modelWithCornersSelf ℝ F)) n (fun (w : M × Λ) => ⟨b w, s w⟩) z) (hFred : ∀ (z : M × Λ), s z = 0 → (sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1).IsFredholm) (htotal : ∀ (z : M × Λ), s z = 0 → Function.Surjective ⇑(sectionLinearization ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z)) (hn : ∀ (z : M × Λ), s z = 0 → ↑((↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index.toNat + 1) ≤ n) {d : ℕ} [IsManifold (modelWithCornersSelf ℝ X) n M] [ContMDiffVectorBundle n F E I] (hn0 : n ≠ 0) (hindex : ∀ (z : M × Λ), s z = 0 → (↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index = ↑d) : ∀ᶠ (l : Λ) in residual Λ, ∃ (cs : ChartedSpace (Fin d → ℝ) ↑{x : M | s (x, l) = 0}), IsManifold (modelWithCornersSelf ℝ (Fin d → ℝ)) n ↑{x : M | s (x, l) = 0} ∧ Manifold.IsImmersionOfComplement F (modelWithCornersSelf ℝ (Fin d → ℝ)) (modelWithCornersSelf ℝ X) n Subtype.val ∧ ∀ (z : ↑{x : M | s (x, l) = 0}), (↑(mfderiv% Subtype.val z)).range = (↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, l)) (fun (y : M) => s (y, l)) ↑z)).ker

Generic regular zeros. For a residual set of parameters l, the zeros of s (·, l) form a C^n manifold of dimension the index d, with a C^n immersion into M whose tangent spaces are the kernels of the linearizations in the M direction.

theorem TauCeti.mem_residual_setOf_forall_section_ne_zero_of_index_neg {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6} {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB] [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F] [IsManifold (modelWithCornersSelf ℝ X) 1 M] [SecondCountableTopology ↑{z : M × Λ | s z = 0}] {n : WithTop ℕ∞} (hcont : ∀ (z : M × Λ), s z = 0 → ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) (I.prod (modelWithCornersSelf ℝ F)) n (fun (w : M × Λ) => ⟨b w, s w⟩) z) (hFred : ∀ (z : M × Λ), s z = 0 → (sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1).IsFredholm) (htotal : ∀ (z : M × Λ), s z = 0 → Function.Surjective ⇑(sectionLinearization ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z)) (hn0 : n ≠ 0) (hindex : ∀ (z : M × Λ), s z = 0 → (↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index < 0) : {l : Λ | ∀ (x : M), s (x, l) ≠ 0} ∈ residual Λ

Generic absence of negative-index zeros. If the slice linearization is Fredholm of negative index at each zero and the total section is transverse to zero, zero-free parameters form a residual set. Second countability is needed only for the universal zero set.

The section only needs to be C¹: Smale's regularity threshold k > max (index, 0) is 1 in negative index.

theorem TauCeti.dense_setOf_forall_section_ne_zero_of_index_neg {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6} {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M] [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB] [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)] [(a : B) → AddCommGroup (E a)] [(a : B) → Module ℝ (E a)] [FiberBundle F E] [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F] [IsManifold (modelWithCornersSelf ℝ X) 1 M] [SecondCountableTopology ↑{z : M × Λ | s z = 0}] {n : WithTop ℕ∞} (hcont : ∀ (z : M × Λ), s z = 0 → ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) (I.prod (modelWithCornersSelf ℝ F)) n (fun (w : M × Λ) => ⟨b w, s w⟩) z) (hFred : ∀ (z : M × Λ), s z = 0 → (sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1).IsFredholm) (htotal : ∀ (z : M × Λ), s z = 0 → Function.Surjective ⇑(sectionLinearization ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z)) (hn0 : n ≠ 0) (hindex : ∀ (z : M × Λ), s z = 0 → (↑(sectionLinearization (modelWithCornersSelf ℝ X) (fun (y : M) => b (y, z.2)) (fun (y : M) => s (y, z.2)) z.1)).index < 0) : Dense {l : Λ | ∀ (x : M), s (x, l) ≠ 0}

Zero-free parameters of a transverse universal section with negative slice indices are dense in the Banach parameter space. In particular they occur arbitrarily near any prescribed parameter, without a constant-index assumption. The section only needs to be C¹.