Documentation

TauCeti.Geometry.Manifold.VectorBundle.Section.Chart

Charts on regular zero sets of sections over Banach manifolds #

A source chart and the complemented-kernel implicit function theorem give coordinates on regular zeros of a bundle section. The charts are on the actual zero set. Their sources are restricted to the bundle trivialization's base set and the neighbourhood where the implicit coordinate map has invertible derivative. A surjective Fredholm derivative of constant index identifies each kernel with the same finite-dimensional model.

sectionZeroChartedSpace assembles this atlas. Smoothness of transitions and the inclusion are proved in Section.Manifold. The source is modelled on a Banach space without boundary.

References #

The construction uses Mathlib's complemented-kernel implicit function theorem and OpenPartialHomeomorph.subtypeCoord.

source
noncomputable def TauCeti.sectionZeroChartAt {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z : โ†‘{y : M | s y = 0}) :
OpenPartialHomeomorph (โ†‘{y : M | s y = 0}) (Fin n โ†’ ๐•œ)

The preferred chart at a regular Fredholm zero, in source-manifold coordinates. Its source is restricted to the bundle trivialization and the regular implicit-coordinate neighbourhood, and its kernel coordinates are identified with the index model.

Instances For
    source
    @[simp]
    theorem TauCeti.sectionZeroChartAt_source {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z : โ†‘{y : M | s y = 0}) :
    (sectionZeroChartAt hf hFred hsurj hindex z).source = Subtype.val โปยน' ((chartAt X โ†‘z).source โˆฉ interior (b โปยน' (e z).baseSet) โˆฉ โ†‘(chartAt X โ†‘z) โปยน' ((HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) โ‹ฏ โ‹ฏ โ‹ฏ).source โˆฉ โ‹ฏ.implicitCoordSource โ‹ฏ โ‹ฏ))

    A preferred chart's source consists of zeros in the source-chart and bundle trivialization domains, whose coordinates belong to the regular implicit-function source.

    source
    theorem TauCeti.sectionZeroChartAt_apply {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z w : โ†‘{y : M | s y = 0}) :
    โ†‘(sectionZeroChartAt hf hFred hsurj hindex z) w = ((D z).kerModelEquiv โ‹ฏ โ‹ฏ) ((Classical.choose โ‹ฏ) (โ†‘(chartAt X โ†‘z) โ†‘w - โ†‘(chartAt X โ†‘z) โ†‘z))

    The preferred chart reads source-chart displacement through the kernel projection.

    source
    @[simp]
    theorem TauCeti.mem_sectionZeroChartAt_target_iff {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z : โ†‘{y : M | s y = 0}) (k : Fin n โ†’ ๐•œ) :
    k โˆˆ (sectionZeroChartAt hf hFred hsurj hindex z).target โ†” have K := (D z).kerModelEquiv โ‹ฏ โ‹ฏ; have ฮฆ := HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) โ‹ฏ โ‹ฏ โ‹ฏ; (0, K.symm k) โˆˆ ฮฆ.target โˆง โ†‘ฮฆ.symm (0, K.symm k) โˆˆ โ‹ฏ.implicitCoordSource โ‹ฏ โ‹ฏ โˆง โ†‘ฮฆ.symm (0, K.symm k) โˆˆ (chartAt X โ†‘z).target โˆง โ†‘(chartAt X โ†‘z).symm (โ†‘ฮฆ.symm (0, K.symm k)) โˆˆ interior (b โปยน' (e z).baseSet)

    The target is the implicit zero slice whose inverse stays in the regular neighbourhood, the source-chart target, and the bundle-trivialization domain.

    source
    theorem TauCeti.coe_sectionZeroChartAt_symm_apply {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z : โ†‘{y : M | s y = 0}) {k : Fin n โ†’ ๐•œ} (hk : k โˆˆ (sectionZeroChartAt hf hFred hsurj hindex z).target) :
    โ†‘(โ†‘(sectionZeroChartAt hf hFred hsurj hindex z).symm k) = โ†‘(chartAt X โ†‘z).symm (โ†‘(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) โ‹ฏ โ‹ฏ โ‹ฏ).symm (0, ((D z).kerModelEquiv โ‹ฏ โ‹ฏ).symm k))

    On the target, the inverse preferred chart is the inverse ambient source chart applied to the inverse implicit coordinates on the zero slice.

    source
    theorem TauCeti.sectionZeroChartAt_symm_mem_source_and_baseSet_and_implicitCoordSource {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z : โ†‘{y : M | s y = 0}) {k : Fin n โ†’ ๐•œ} (hk : k โˆˆ (sectionZeroChartAt hf hFred hsurj hindex z).target) :
    have y := โ†‘(โ†‘(sectionZeroChartAt hf hFred hsurj hindex z).symm k); y โˆˆ (chartAt X โ†‘z).source โˆง b y โˆˆ (e z).baseSet โˆง โ†‘(chartAt X โ†‘z) y โˆˆ โ‹ฏ.implicitCoordSource โ‹ฏ โ‹ฏ

    The inverse chart remains in the ambient source-chart source, the bundle-trivialization base set, and the regular implicit-function neighbourhood.

    source
    @[simp]
    theorem TauCeti.sectionZeroChartAt_apply_self {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (z : โ†‘{y : M | s y = 0}) :
    โ†‘(sectionZeroChartAt hf hFred hsurj hindex z) z = 0

    A preferred chart is centred at its zero.

    source
    theorem TauCeti.mem_sectionZeroChartAt_source {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (hb : โˆ€ (z : โ†‘{y : M | s y = 0}), ContinuousAt b โ†‘z) (he : โˆ€ (z : โ†‘{y : M | s y = 0}), b โ†‘z โˆˆ (e z).baseSet) (z : โ†‘{y : M | s y = 0}) :
    z โˆˆ (sectionZeroChartAt hf hFred hsurj hindex z).source

    Every zero lies in the source of its preferred chart.

    source
    theorem TauCeti.mem_sectionZeroChartAt_target {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (hb : โˆ€ (z : โ†‘{y : M | s y = 0}), ContinuousAt b โ†‘z) (he : โˆ€ (z : โ†‘{y : M | s y = 0}), b โ†‘z โˆˆ (e z).baseSet) (z : โ†‘{y : M | s y = 0}) :
    0 โˆˆ (sectionZeroChartAt hf hFred hsurj hindex z).target

    The origin belongs to the preferred chart target.

    source
    @[simp]
    theorem TauCeti.sectionZeroChartAt_symm_zero {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (hb : โˆ€ (z : โ†‘{y : M | s y = 0}), ContinuousAt b โ†‘z) (he : โˆ€ (z : โ†‘{y : M | s y = 0}), b โ†‘z โˆˆ (e z).baseSet) (z : โ†‘{y : M | s y = 0}) :
    โ†‘(sectionZeroChartAt hf hFred hsurj hindex z).symm 0 = z

    The inverse chart sends the origin to its zero.

    source
    @[irreducible]
    noncomputable def TauCeti.sectionZeroChartedSpace {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (hb : โˆ€ (z : โ†‘{y : M | s y = 0}), ContinuousAt b โ†‘z) (he : โˆ€ (z : โ†‘{y : M | s y = 0}), b โ†‘z โˆˆ (e z).baseSet) :
    ChartedSpace (Fin n โ†’ ๐•œ) โ†‘{y : M | s y = 0}

    The atlas of preferred implicit-function charts on the actual section zero set.

    Instances For
      source
      @[simp]
      theorem TauCeti.sectionZeroChartedSpace_chartAt {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (hb : โˆ€ (z : โ†‘{y : M | s y = 0}), ContinuousAt b โ†‘z) (he : โˆ€ (z : โ†‘{y : M | s y = 0}), b โ†‘z โˆˆ (e z).baseSet) (z : โ†‘{y : M | s y = 0}) :
      chartAt (Fin n โ†’ ๐•œ) z = sectionZeroChartAt hf hFred hsurj hindex z

      The installed preferred charts are sectionZeroChartAt.

      source
      @[simp]
      theorem TauCeti.sectionZeroChartedSpace_atlas {๐•œ : Type u_1} {X : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {E : B โ†’ Type u_6} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] [NormedAddCommGroup X] [NormedSpace ๐•œ X] [CompleteSpace X] [TopologicalSpace M] [ChartedSpace X M] [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 : M โ†’ B} {s : (y : M) โ†’ E (b y)} {e : โ†‘{y : M | s y = 0} โ†’ Bundle.Trivialization F Bundle.TotalSpace.proj} [โˆ€ (z : โ†‘{y : M | s y = 0}), MemTrivializationAtlas (e z)] {D : โ†‘{y : M | s y = 0} โ†’ X โ†’L[๐•œ] F} {n : โ„•} (hf : โˆ€ (z : โ†‘{y : M | s y = 0}), HasStrictFDerivAt (fun (y : X) => (โ†‘(e z) โŸจb (โ†‘(chartAt X โ†‘z).symm y), s (โ†‘(chartAt X โ†‘z).symm y)โŸฉ).2) (D z) (โ†‘(chartAt X โ†‘z) โ†‘z)) (hFred : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).IsFredholm) (hsurj : โˆ€ (z : โ†‘{y : M | s y = 0}), Function.Surjective โ‡‘(D z)) (hindex : โˆ€ (z : โ†‘{y : M | s y = 0}), (D z).index = โ†‘n) (hb : โˆ€ (z : โ†‘{y : M | s y = 0}), ContinuousAt b โ†‘z) (he : โˆ€ (z : โ†‘{y : M | s y = 0}), b โ†‘z โˆˆ (e z).baseSet) :
      atlas (Fin n โ†’ ๐•œ) โ†‘{y : M | s y = 0} = Set.range (sectionZeroChartAt hf hFred hsurj hindex)

      The installed atlas consists exactly of the preferred charts.