The parameter projection of a universal linearization

A transversality argument in Floer theory never perturbs a single equation; it perturbs a whole family. One writes the equation as f x l = 0 for x in a Banach space E of maps and l in a Banach space Λ of parameters -- almost complex structures, Hamiltonians, metrics -- and studies the universal zero set {(x, l) | f x l = 0} rather than any one fibre. Linearizing at a solution turns that geometric picture into a purely linear one: the total derivative is a continuous linear map E × Λ →L[𝕜] F, its restriction D₁ to E × 0 is the linearization of the single equation at the fixed parameter, its restriction D₂ to 0 × Λ records how the equation moves with the parameter, the kernel of the total derivative is the tangent space to the universal zero set when the nonlinear hypotheses make that zero set a manifold (and is its candidate tangent space in general), and the projection to Λ of that kernel is the linearization of "forget the solution, remember the parameter".

This file analyses that projection. Writing the total derivative as a coproduct D₁.coprod D₂ : E × Λ →L[𝕜] F, which by ContinuousLinearMap.coprod_comp_inl_inr is no loss of generality, ContinuousLinearMap.parameterProj D₁ D₂ is the restriction of Prod.snd to (D₁.coprod D₂).ker, and the two theorems that transversality arguments run on are:

• the projection is surjective exactly when D₁ is, provided the total linearization is surjective -- so a parameter is a regular value of the projection exactly when the equation it indexes is regular;
• when E and Λ are Banach spaces the projection is Fredholm whenever D₁ is Fredholm; if the total linearization is surjective it has the same index as D₁ -- so the parametrized problem carries the same expected dimension count as the unparametrized one.

Together these are the linear engine of the parametric transversality theorem (McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3). A further step can feed the projection to the Sard--Smale theorem of TauCeti.Analysis.Fredholm.SardSmale; besides a smooth chart on the universal zero set, its residual-set conclusion requires real scalars, second countability of the domain, and the stated C^k threshold. At a regular parameter, TauCeti.Analysis.Fredholm.LevelSet.Basic supplies a chart modelled on a finite-dimensional space whose dimension is the index of D₁. This file supplies only the linear half of that chain.

The exact sequence

Everything below is read off one four-term exact sequence of 𝕜-modules,

0 → ker D₁ → ker (D₁.coprod D₂) → Λ → F ⧸ range D₁,

whose maps are x ↦ (x, 0) (ContinuousLinearMap.kerCoprodHom), the parameter projection, and the map induced by D₂ (ContinuousLinearMap.parameterToCoker). Its exactness at ker (D₁.coprod D₂) and at Λ is ContinuousLinearMap.exact_kerCoprodHom_parameterProj and ContinuousLinearMap.exact_parameterProj_parameterToCoker; both hold with no hypothesis at all.

Exactness at ker (D₁.coprod D₂) says that the kernel of the projection is ker D₁: a point of the universal zero set over a fixed parameter is a solution of the equation that parameter indexes. Exactness at Λ says that the range of the projection consists of the parameter directions whose infinitesimal effect D₂ l on the equation is already achievable by moving the solution.

Surjectivity of the total linearization says exactly that range D₁ ⊔ range D₂ = ⊤, that is, that the last map above is onto (ContinuousLinearMap.parameterToCoker_surjective_iff_coprod_surjective). Extending the sequence by → 0 on the right then identifies the cokernel of the projection with the cokernel of D₁ (ContinuousLinearMap.quotientRangeParameterProjEquiv), and the surjectivity criterion is the degenerate case of that identification.

The exact sequence, its algebraic identifications, and the finrank identities hold over any ring, with continuous addition in F; the finite-dimensionality statements hold over division rings without any norm. The index statement also holds over any ring and needs neither completeness nor the Fredholm property, because ContinuousLinearMap.index is a difference of two Module.finranks and the sequence matches both of them.

The Fredholm statement additionally assumes that D₁ is Fredholm and that E and Λ are Banach spaces; F need only have continuous addition and closed points. Its closed range is the preimage of the closed range of D₁, its kernel inherits a continuous projection from that of D₁, and the Banach open mapping theorem gives strictness. No completeness of the scalar field is required.

Main declarations

• ContinuousLinearMap.parameterProj: the projection to the parameter space of the kernel of a total linearization D₁.coprod D₂.
• ContinuousLinearMap.exact_kerCoprodHom_parameterProj and ContinuousLinearMap.exact_parameterProj_parameterToCoker: the exact sequence above.
• ContinuousLinearMap.kerEquivKerParameterProj: the kernel of the projection is ker D₁.
• ContinuousLinearMap.range_parameterProj: its range is the preimage of range D₁ under D₂.
• ContinuousLinearMap.parameterToCoker_surjective_iff_coprod_surjective: the total linearization is onto exactly when the parameter directions span the cokernel of D₁.
• ContinuousLinearMap.quotientRangeParameterProjEquiv: for a surjective total linearization, the cokernel of the projection is the cokernel of D₁.
• ContinuousLinearMap.parameterProj_surjective_iff: for a surjective total linearization, the projection is surjective exactly when D₁ is.
• ContinuousLinearMap.index_parameterProj: for a surjective total linearization, the projection has the same index as D₁.
• ContinuousLinearMap.isFredholm_parameterProj: when E and Λ are Banach spaces, if D₁ is Fredholm then the projection is Fredholm.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix A.3.

def ContinuousLinearMap.parameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : ↥(↑(D₁.coprod D₂)).ker →L[𝕜] Λ

The parameter projection of the total linearization D₁.coprod D₂ : E × Λ →L[𝕜] F: the restriction to its kernel of the projection E × Λ →L[𝕜] Λ.

The kernel of the total linearization is the candidate tangent space to the universal zero set of a parametrized equation; under the nonlinear hypotheses making that zero set a manifold, it is its tangent space. This map is then the linearization of the projection of that zero set to the space of parameters. Every continuous linear map out of E × Λ is of the form D₁.coprod D₂, by ContinuousLinearMap.coprod_comp_inl_inr, so the coproduct source is no restriction.

Equations

• D₁.parameterProj D₂ = (ContinuousLinearMap.snd 𝕜 E Λ).domRestrict (↑(D₁.coprod D₂)).ker

@[simp]

theorem ContinuousLinearMap.parameterProj_apply {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (v : ↥(↑(D₁.coprod D₂)).ker) : (D₁.parameterProj D₂) v = (↑v).2

The parameter projection reads off the parameter component of a candidate tangent vector.

Exactness at the candidate tangent space: the kernel of the projection

def ContinuousLinearMap.kerCoprodHom {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : ↥(↑D₁).ker →L[𝕜] ↥(↑(D₁.coprod D₂)).ker

The embedding x ↦ (x, 0) of ker D₁ into the kernel of the total linearization: the formal tangent directions to the universal zero set along which the parameter does not move.

Equations

• D₁.kerCoprodHom D₂ = (ContinuousLinearMap.inl 𝕜 E Λ).restrict ⋯

@[simp]

theorem ContinuousLinearMap.kerCoprodHom_apply {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (x : ↥(↑D₁).ker) : ↑((D₁.kerCoprodHom D₂) x) = (↑x, 0)

The embedding sends x to the pair (x, 0).

theorem ContinuousLinearMap.kerCoprodHom_injective {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : Function.Injective ⇑(D₁.kerCoprodHom D₂)

The embedding x ↦ (x, 0) is injective, which is exactness of the sequence at ker D₁.

@[simp]

theorem ContinuousLinearMap.range_kerCoprodHom {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : (↑(D₁.kerCoprodHom D₂)).range = (↑(D₁.parameterProj D₂)).ker

The formal tangent directions along which the parameter does not move are exactly the solutions of the linearized equation at the fixed parameter.

theorem ContinuousLinearMap.exact_kerCoprodHom_parameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : Function.Exact ⇑(D₁.kerCoprodHom D₂) ⇑(D₁.parameterProj D₂)

Exactness of 0 → ker D₁ → ker (D₁.coprod D₂) → Λ at the middle term.

def ContinuousLinearMap.kerEquivKerParameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : ↥(↑D₁).ker ≃L[𝕜] ↥(↑(D₁.parameterProj D₂)).ker

The continuous linear identification of ker D₁ with the kernel of the projection.

Equations

• D₁.kerEquivKerParameterProj D₂ = ContinuousLinearEquiv.equivOfInverse (ContinuousLinearMap.kerCoprodHomToKer✝ D₁ D₂) (ContinuousLinearMap.kerParameterProjInverse✝ D₁ D₂) ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.kerEquivKerParameterProj_apply {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (x : ↥(↑D₁).ker) : ↑↑((D₁.kerEquivKerParameterProj D₂) x) = (↑x, 0)

The identification of ker D₁ with the kernel of the projection is x ↦ (x, 0).

@[simp]

theorem ContinuousLinearMap.kerEquivKerParameterProj_symm_apply {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (v : ↥(↑(D₁.parameterProj D₂)).ker) : ↑((D₁.kerEquivKerParameterProj D₂).symm v) = (↑↑v).1

The inverse identification takes the first component of a vector in the projection kernel.

Exactness at the parameter space: the range of the projection

@[simp]

theorem ContinuousLinearMap.range_parameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : (↑(D₁.parameterProj D₂)).range = Submodule.comap (↑D₂) (↑D₁).range

The range of the parameter projection is the set of parameter directions whose infinitesimal effect D₂ l on the equation can already be undone by moving the solution.

No hypothesis on D₁ or on the total linearization is needed.

noncomputable def ContinuousLinearMap.parameterToCoker {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : Λ →ₗ[𝕜] F ⧸ (↑D₁).range

The map Λ → F ⧸ range D₁ induced by D₂: it measures how far the infinitesimal effect of a parameter direction is from being achievable by moving the solution.

Equations

• D₁.parameterToCoker D₂ = (↑D₁).range.mkQ ∘ₗ ↑D₂

@[simp]

theorem ContinuousLinearMap.parameterToCoker_apply {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (l : Λ) : (D₁.parameterToCoker D₂) l = (↑D₁).range.mkQ (D₂ l)

The induced map sends a parameter direction to the class of its infinitesimal effect.

@[simp]

theorem ContinuousLinearMap.ker_parameterToCoker {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : (D₁.parameterToCoker D₂).ker = (↑(D₁.parameterProj D₂)).range

The kernel of the map induced by D₂ is the range of the parameter projection: this is ContinuousLinearMap.range_parameterProj read in the quotient.

theorem ContinuousLinearMap.exact_parameterProj_parameterToCoker {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : Function.Exact ⇑(D₁.parameterProj D₂) ⇑(D₁.parameterToCoker D₂)

Exactness of ker (D₁.coprod D₂) → Λ → F ⧸ range D₁ at the middle term.

theorem ContinuousLinearMap.parameterToCoker_surjective_iff_coprod_surjective {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : Function.Surjective ⇑(D₁.parameterToCoker D₂) ↔ Function.Surjective ⇑(D₁.coprod D₂)

The total linearization is surjective exactly when the parameter directions span the cokernel of D₁.

This is the criterion transversality arguments verify in practice: one exhibits enough perturbations of the equation to cover every obstruction to solving the linearized equation.

The cokernel of the projection

noncomputable def ContinuousLinearMap.quotientRangeParameterProjEquivRange {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : (Λ ⧸ (↑(D₁.parameterProj D₂)).range) ≃ₗ[𝕜] ↥(D₁.parameterToCoker D₂).range

The cokernel of the parameter projection is the range of the map from parameters into the cokernel of D₁.

Equations

• D₁.quotientRangeParameterProjEquivRange D₂ = ((↑(D₁.parameterProj D₂)).range.quotEquivOfEq (D₁.parameterToCoker D₂).ker ⋯).trans (D₁.parameterToCoker D₂).quotKerEquivRange

@[simp]

theorem ContinuousLinearMap.quotientRangeParameterProjEquivRange_mk {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (l : Λ) : ↑((D₁.quotientRangeParameterProjEquivRange D₂) (Submodule.Quotient.mk l)) = (↑D₁).range.mkQ (D₂ l)

The range equivalence sends the class of l to the image of l in the cokernel.

noncomputable def ContinuousLinearMap.quotientRangeParameterProjEquiv {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD : Function.Surjective ⇑(D₁.coprod D₂)) : (Λ ⧸ (↑(D₁.parameterProj D₂)).range) ≃ₗ[𝕜] F ⧸ (↑D₁).range

For a surjective total linearization, the cokernel of the parameter projection is the cokernel of D₁, identified by the map induced by D₂.

ContinuousLinearMap.ker_parameterToCoker identifies the kernel of the map from parameters to the cokernel with range (parameterProj D₁ D₂), making the descended map on the quotient injective. Surjectivity of the total linearization is what makes that descended map onto.

Equations

• D₁.quotientRangeParameterProjEquiv D₂ hD = ((↑(D₁.parameterProj D₂)).range.quotEquivOfEq (D₁.parameterToCoker D₂).ker ⋯).trans ((D₁.parameterToCoker D₂).quotKerEquivOfSurjective ⋯)

@[simp]

theorem ContinuousLinearMap.quotientRangeParameterProjEquiv_mk {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD : Function.Surjective ⇑(D₁.coprod D₂)) (l : Λ) : (D₁.quotientRangeParameterProjEquiv D₂ hD) (Submodule.Quotient.mk l) = Submodule.Quotient.mk (D₂ l)

The cokernel equivalence sends the class of l to the class of D₂ l.

theorem ContinuousLinearMap.range_parameterProj_eq_top_of_range_eq_top {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD₁ : (↑D₁).range = ⊤) : (↑(D₁.parameterProj D₂)).range = ⊤

If D₁ is onto, then so is the parameter projection, with no hypothesis on the total linearization.

theorem ContinuousLinearMap.parameterProj_surjective_of_surjective {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD₁ : Function.Surjective ⇑D₁) : Function.Surjective ⇑(D₁.parameterProj D₂)

The Function.Surjective form of ContinuousLinearMap.range_parameterProj_eq_top_of_range_eq_top.

theorem ContinuousLinearMap.range_parameterProj_eq_top_iff {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD : (↑(D₁.coprod D₂)).range = ⊤) : (↑(D₁.parameterProj D₂)).range = ⊤ ↔ (↑D₁).range = ⊤

Assuming the total linearization is surjective, the parameter projection is onto exactly when D₁ is. In the nonlinear application, this says that a parameter is a regular value of the projection from the universal zero set precisely when the equation it indexes is regular.

theorem ContinuousLinearMap.parameterProj_surjective_iff {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD : Function.Surjective ⇑(D₁.coprod D₂)) : Function.Surjective ⇑(D₁.parameterProj D₂) ↔ Function.Surjective ⇑D₁

The Function.Surjective form of ContinuousLinearMap.range_parameterProj_eq_top_iff.

The dimensions of the kernel and cokernel

@[simp]

theorem ContinuousLinearMap.finrank_ker_parameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) : Module.finrank 𝕜 ↥(↑(D₁.parameterProj D₂)).ker = Module.finrank 𝕜 ↥(↑D₁).ker

The kernel of the parameter projection has the same dimension as the kernel of D₁.

theorem ContinuousLinearMap.finrank_quotient_range_parameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD : Function.Surjective ⇑(D₁.coprod D₂)) : Module.finrank 𝕜 (Λ ⧸ (↑(D₁.parameterProj D₂)).range) = Module.finrank 𝕜 (F ⧸ (↑D₁).range)

For a surjective total linearization, the cokernel of the parameter projection has the same dimension as the cokernel of D₁.

theorem ContinuousLinearMap.index_parameterProj {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD : Function.Surjective ⇑(D₁.coprod D₂)) : (D₁.parameterProj D₂).index = D₁.index

The parameter projection of a surjective total linearization has the same index as D₁.

Under the hypotheses needed to apply TauCeti.Analysis.Fredholm.LevelSet.Basic, this equality gives the dimension of the finite-dimensional model space for a regular fibre.

Neither operator is assumed Fredholm: both sides are differences of Module.finranks, and the exact sequence matches the four dimensions in pairs, junk values included.

theorem ContinuousLinearMap.finiteDimensional_ker_parameterProj {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) [FiniteDimensional 𝕜 ↥(↑D₁).ker] : FiniteDimensional 𝕜 ↥(↑(D₁.parameterProj D₂)).ker

The kernel of the parameter projection is finite dimensional as soon as that of D₁ is.

theorem ContinuousLinearMap.finiteDimensional_quotient_range_parameterProj {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup Λ] [Module 𝕜 Λ] [TopologicalSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) [FiniteDimensional 𝕜 (F ⧸ (↑D₁).range)] : FiniteDimensional 𝕜 (Λ ⧸ (↑(D₁.parameterProj D₂)).range)

The cokernel of the parameter projection is finite dimensional as soon as that of D₁ is; surjectivity of the total linearization is not needed.

theorem ContinuousLinearMap.isFredholm_parameterProj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup Λ] [NormedSpace 𝕜 Λ] [CompleteSpace Λ] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [T1Space F] (D₁ : E →L[𝕜] F) (D₂ : Λ →L[𝕜] F) (hD₁ : D₁.IsFredholm) : (D₁.parameterProj D₂).IsFredholm

The parameter projection is Fredholm as soon as D₁ is, when E and Λ are Banach spaces and F has continuous addition and closed points. When the total linearization is surjective, ContinuousLinearMap.index_parameterProj also identifies their indices.

Applying Sard--Smale in the nonlinear setting is a further step requiring a suitable smooth chart, real scalars, second countability, and the theorem's C^k threshold.