Documentation

TauCeti.Geometry.Manifold.VectorBundle.Section.ZeroChart

Local charts for regular zeros of bundle sections #

A section along a map from a Banach space has, near a regular zero, a zero set parametrized by the kernel of its coordinate derivative. The chart is on the actual zero set of the section, not on the globally extended coordinate equation: outside a bundle trivialization's base set, that equation can have spurious zeros. We restrict the implicit-function chart to the interior of the preimage of the base set before taking its zero slice.

sectionZeroChart provides this local homeomorphism, with its source, target, coordinate formula and normalization. Its inverse, included into the parameter space, is smooth at the origin and has derivative the inclusion of the kernel. For a surjective Fredholm derivative, exists_sectionZeroChartModel gives a chart modelled on Fin n โ†’ ๐•œ, where n is the index, and identifies its tangent image with the kernel of the intrinsic section linearization.

The atlas on regular zero sets over Banach manifolds is constructed in Section.Chart; smooth compatibility is proved in Section.Manifold.

References #

The construction uses Mathlib's complemented-kernel implicit function theorem and OpenPartialHomeomorph.subtypeCoord, as in TauCeti.levelSetChart.

source
noncomputable def TauCeti.sectionZeroChart {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
OpenPartialHomeomorph โ†‘{y : X | s y = 0} โ†ฅ(โ†‘T).ker

The implicit-function chart of a section's actual zero set, restricted to the neighbourhood where the chosen bundle trivialization is valid. The coordinates are the projection onto the kernel of the coordinate derivative, applied to displacement from the base point.

Instances For
    source
    @[simp]
    theorem TauCeti.sectionZeroChart_source {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    (sectionZeroChart hf hT hker hz).source = Subtype.val โปยน' ((HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T hf hT hker).source โˆฉ interior (b โปยน' e.baseSet))

    The source consists of zeros in the implicit-function source and in the interior of the preimage of the bundle trivialization's base set.

    source
    @[simp]
    theorem TauCeti.sectionZeroChart_target {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    (sectionZeroChart hf hT hker hz).target = (fun (k : โ†ฅ(โ†‘T).ker) => (0, k)) โปยน' ((HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T hf hT hker).restrOpen (interior (b โปยน' e.baseSet)) โ‹ฏ).target

    The target is the zero slice of the implicit-function target, restricted to points whose inverse remains in the trivialization's base set.

    source
    theorem TauCeti.sectionZeroChart_apply {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) (y : โ†‘{y : X | s y = 0}) :
    โ†‘(sectionZeroChart hf hT hker hz) y = (Classical.choose hker) (โ†‘y - x)

    The section-zero chart reads displacement through the chosen projection onto the kernel.

    source
    theorem TauCeti.coe_sectionZeroChart_symm_apply {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) {k : โ†ฅ(โ†‘T).ker} (hk : k โˆˆ (sectionZeroChart hf hT hker hz).target) :
    โ†‘(โ†‘(sectionZeroChart hf hT hker hz).symm k) = โ†‘(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T hf hT hker).symm (0, k)

    On the target, the inverse chart is the ambient implicit function on the zero slice.

    source
    @[simp]
    theorem TauCeti.sectionZeroChart_apply_self {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    โ†‘(sectionZeroChart hf hT hker hz) โŸจx, hzโŸฉ = 0

    The chart is centred at the regular zero.

    source
    theorem TauCeti.mem_sectionZeroChart_source {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hb : ContinuousAt b x) (he : b x โˆˆ e.baseSet) (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    โŸจx, hzโŸฉ โˆˆ (sectionZeroChart hf hT hker hz).source

    Continuity of the base map at the zero ensures that the zero lies in the chart source.

    source
    theorem TauCeti.mem_sectionZeroChart_target {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hb : ContinuousAt b x) (he : b x โˆˆ e.baseSet) (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    0 โˆˆ (sectionZeroChart hf hT hker hz).target

    The origin belongs to the target of a section-zero chart at a zero in its base set.

    source
    @[simp]
    theorem TauCeti.sectionZeroChart_symm_zero {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hb : ContinuousAt b x) (he : b x โˆˆ e.baseSet) (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    โ†‘(sectionZeroChart hf hT hker hz).symm 0 = โŸจx, hzโŸฉ

    The inverse sends the chart origin back to the section's zero.

    source
    theorem TauCeti.contDiffAt_coe_sectionZeroChart_symm {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} {m : WithTop โ„•โˆž} (hb : ContinuousAt b x) (he : b x โˆˆ e.baseSet) (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) (hs : ContDiffAt ๐•œ m (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) x) :
    ContDiffAt ๐•œ m (fun (k : โ†ฅ(โ†‘T).ker) => โ†‘(โ†‘(sectionZeroChart hf hT hker hz).symm k)) 0

    The inverse chart, included in the parameter space, is as smooth at the origin as the section's fiber coordinates are at its zero.

    source
    theorem TauCeti.hasStrictFDerivAt_coe_sectionZeroChart_symm {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} (hb : ContinuousAt b x) (he : b x โˆˆ e.baseSet) (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) :
    HasStrictFDerivAt (fun (k : โ†ฅ(โ†‘T).ker) => โ†‘(โ†‘(sectionZeroChart hf hT hker hz).symm k)) (โ†‘T).ker.subtypeL 0

    The tangent parametrization at the origin is the canonical inclusion of the kernel of the section's coordinate derivative.

    source
    theorem TauCeti.contDiffAt_coe_sectionZeroChart_symm_of_mem {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} {m : WithTop โ„•โˆž} (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hT : (โ†‘T).range = โŠค) (hker : (โ†‘T).ker.ClosedComplemented) (hz : s x = 0) {k : โ†ฅ(โ†‘T).ker} (hk : k โˆˆ (sectionZeroChart hf hT hker hz).target) (hmem : โ†‘(โ†‘(sectionZeroChart hf hT hker hz).symm k) โˆˆ hf.implicitCoordSource hT hker) (hs : ContDiffAt ๐•œ m (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) โ†‘(โ†‘(sectionZeroChart hf hT hker hz).symm k)) :
    ContDiffAt ๐•œ m (fun (j : โ†ฅ(โ†‘T).ker) => โ†‘(โ†‘(sectionZeroChart hf hT hker hz).symm j)) k

    Away from the origin, the inverse section-zero chart is smooth wherever its image lies in the neighbourhood on which the implicit coordinate derivative remains invertible.

    source
    theorem TauCeti.exists_sectionZeroChartModel {๐•œ : Type u_1} {X : Type u_2} {B : Type u_3} {F : Type u_4} {E : B โ†’ Type u_5} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace 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 : X โ†’ B} {s : (y : X) โ†’ E (b y)} {x : X} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : X โ†’L[๐•œ] F} [CompleteSpace ๐•œ] {m : WithTop โ„•โˆž} {n : โ„•} (hb : ContinuousAt b x) (he : b x โˆˆ e.baseSet) (hf : HasStrictFDerivAt (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) T x) (hFred : T.IsFredholm) (hsurj : Function.Surjective โ‡‘(sectionLinearization (modelWithCornersSelf ๐•œ X) b s x)) (hindex : T.index = โ†‘n) (hz : s x = 0) (hs : ContDiffAt ๐•œ m (fun (y : X) => (โ†‘e โŸจb y, s yโŸฉ).2) x) :
    โˆƒ (ฯ‡ : OpenPartialHomeomorph (โ†‘{y : X | s y = 0}) (Fin n โ†’ ๐•œ)), โŸจx, hzโŸฉ โˆˆ ฯ‡.source โˆง โ†‘ฯ‡ โŸจx, hzโŸฉ = 0 โˆง ContDiffAt ๐•œ m (fun (k : Fin n โ†’ ๐•œ) => โ†‘(โ†‘ฯ‡.symm k)) 0 โˆง Function.Injective โ‡‘(fderiv ๐•œ (fun (k : Fin n โ†’ ๐•œ) => โ†‘(โ†‘ฯ‡.symm k)) 0) โˆง (โ†‘(fderiv ๐•œ (fun (k : Fin n โ†’ ๐•œ) => โ†‘(โ†‘ฯ‡.symm k)) 0)).range = (โ†‘(sectionLinearization (modelWithCornersSelf ๐•œ X) b s x)).ker

    A regular zero of a Fredholm section has a local parametrization of dimension the index. The parametrization is as smooth at its origin as the section's coordinates, and its derivative is injective with image exactly the kernel of the intrinsic section linearization.

    The base map may in particular be a manifold chart inverse, so the statement also applies to local parameter expressions of sections over Banach manifolds.