Documentation

TauCeti.Geometry.Manifold.VectorBundle.Section.Linearization

Linearization of a section at a zero #

At a zero of a differentiable section, differentiating its fiber coordinates and transporting back to the fiber gives a linear map from the tangent space of the source to the fiber, independent of the trivialization. Away from a zero, the derivative of the transition function contributes an additional term, so no such independence is asserted.

We work with a section along a map from a manifold M to the base of the bundle. This includes sections over Banach manifolds, and sections over Banach spaces with their canonical manifold structure π“˜(π•œ, X), for which mvfderiv_eq_fderiv recovers the FrΓ©chet derivative. The coordinate-change formula shows that Fredholmness, the index, and regularity (surjectivity) at zeros can be checked in any bundle trivialization, and the chain rule sectionLinearization_comp passes between a manifold source and its source charts.

The convention is that of McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3. The calculation uses Mathlib's bundle coordinate changes and the zero-value derivative rule TauCeti.mvfderiv_eq_comp_of_eventuallyEq_clm_apply.

source
noncomputable def TauCeti.sectionLinearization {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] (IM : ModelWithCorners π•œ EM HM) [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)) (x : M) :
TangentSpace IM x β†’L[π•œ] E (b x)

Differentiate a section along b in the preferred trivialization at b x, then transport the derivative back to that fiber. At a zero of a differentiable section this is independent of the trivialization, as expressed by sectionLinearization_eq_symmL_comp.

As with mfderiv, this expression is defined even where differentiability fails.

Instances For
    source
    theorem TauCeti.sectionLinearization_def {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} :
    sectionLinearization IM b s x = Bundle.Trivialization.symmL π•œ (trivializationAt F E (b x)) (b x) ∘SL (d% fun (y : M) => (↑(trivializationAt F E (b x)) ⟨b y, s y⟩).2) x

    The defining expression for the linearization in the preferred trivialization.

    source
    theorem TauCeti.index_sectionLinearization_of_finiteDimensional {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} [FiniteDimensional π•œ EM] [FiniteDimensional π•œ F] :
    (↑(sectionLinearization IM b s x)).index = ↑(Module.finrank π•œ EM) - ↑(Module.finrank π•œ F)

    For finite-dimensional source and model fiber, the intrinsic section linearization has index equal to the source dimension minus the fiber dimension, even away from zeros and without differentiability assumptions.

    source
    @[simp]
    theorem TauCeti.sectionLinearization_zero {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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} {x : M} (hb : ContinuousAt b x) :
    sectionLinearization IM b (fun (y : M) => 0) x = 0

    The zero section along a continuous map has zero linearization.

    source
    theorem TauCeti.mvfderiv_section_coordChange_of_eq_zero {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (he' : b x ∈ e'.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    (d% fun (y : M) => (↑e' ⟨b y, s y⟩).2) x = ↑(Bundle.Trivialization.coordChangeL π•œ e e' (b x)) ∘SL (d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x

    At a zero of a section along a continuous map, its coordinate derivatives in two bundle trivializations differ by postcomposition with the fiber coordinate change.

    source
    theorem TauCeti.sectionLinearization_eq_symmL_comp {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    sectionLinearization IM b s x = Bundle.Trivialization.symmL π•œ e (b x) ∘SL (d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x

    At a zero, the linearization can be computed in any bundle trivialization whose fiber coordinates are differentiable at the point.

    source
    @[simp]
    theorem TauCeti.continuousLinearMapAt_comp_sectionLinearization {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    Bundle.Trivialization.continuousLinearMapAt π•œ e (b x) ∘SL sectionLinearization IM b s x = (d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x

    Reading the intrinsic linearization in a trivialization recovers the derivative of the section's fiber coordinates.

    source
    theorem TauCeti.surjective_sectionLinearization_iff {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    Function.Surjective ⇑(sectionLinearization IM b s x) ↔ Function.Surjective ⇑((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x)

    A zero is regular for the intrinsic linearization exactly when its coordinate derivative is surjective.

    source
    theorem TauCeti.ker_sectionLinearization {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    (↑(sectionLinearization IM b s x)).ker = (↑((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x)).ker

    At a zero, the intrinsic linearization has the same kernel as the derivative of any differentiable fiber-coordinate expression.

    source
    theorem TauCeti.range_subtypeL_comp_eq_ker_sectionLinearization {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {T : TangentSpace IM x β†’L[π•œ] F} {G : Type u_8} [AddCommGroup G] [Module π•œ G] [TopologicalSpace G] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hf : HasMFDerivAt% (fun (y : M) => (↑e ⟨b y, s y⟩).2) x T) (hz : s x = 0) (K : β†₯(↑T).ker ≃L[π•œ] G) :
    (↑((↑T).ker.subtypeL ∘SL ↑K.symm)).range = (↑(sectionLinearization IM b s x)).ker

    At a zero, the kernel inclusion composed with the inverse of a kernel-model equivalence has range equal to the kernel of the intrinsic section linearization.

    source
    theorem TauCeti.index_sectionLinearization {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    (↑(sectionLinearization IM b s x)).index = (↑((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x)).index

    At a zero, the intrinsic linearization and any differentiable fiber-coordinate expression have the same Fredholm index.

    source
    theorem TauCeti.isFredholm_sectionLinearization_iff {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    (sectionLinearization IM b s x).IsFredholm ↔ ((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x).IsFredholm

    A section's intrinsic linearization at a zero is Fredholm exactly when its derivative in any differentiable fiber-coordinate expression is Fredholm.

    source
    theorem TauCeti.index_mvfderiv_section_coordChange_of_eq_zero {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (he' : b x ∈ e'.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    (↑((d% fun (y : M) => (↑e' ⟨b y, s y⟩).2) x)).index = (↑((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x)).index

    The Fredholm index of a section's coordinate derivative at a zero is independent of the bundle trivialization. No Fredholm hypothesis is needed for this equality of indices.

    source
    theorem TauCeti.isFredholm_mvfderiv_section_coordChange_iff_of_eq_zero {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (he' : b x ∈ e'.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    ((d% fun (y : M) => (↑e' ⟨b y, s y⟩).2) x).IsFredholm ↔ ((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x).IsFredholm

    Fredholmness of a section's coordinate derivative at a zero is independent of the bundle trivialization.

    source
    theorem TauCeti.surjective_mvfderiv_section_coordChange_iff_of_eq_zero {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {x : M} {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] (hb : ContinuousAt b x) (he : b x ∈ e.baseSet) (he' : b x ∈ e'.baseSet) (hs : (MDiffAt fun (y : M) => (↑e ⟨b y, s y⟩).2) x) (hzero : s x = 0) :
    Function.Surjective ⇑((d% fun (y : M) => (↑e' ⟨b y, s y⟩).2) x) ↔ Function.Surjective ⇑((d% fun (y : M) => (↑e ⟨b y, s y⟩).2) x)

    Surjectivity of a section's coordinate derivative at a zero is independent of the bundle trivialization, so regular zeros can be tested in any fiber coordinates.

    source
    @[simp]
    theorem TauCeti.sectionLinearization_trivial {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM M] [NormedAddCommGroup F] [NormedSpace π•œ F] [TopologicalSpace B] (b : M β†’ B) (f : M β†’ F) (x : M) :
    sectionLinearization IM b f x = d% f x

    In a trivial bundle, the linearization of a section along any map is just the vector-valued manifold derivative of its fiber component.

    source
    theorem TauCeti.sectionLinearization_comp {π•œ : Type u_1} {EM : Type u_2} {HM : Type u_3} {M : Type u_4} {B : Type u_5} {F : Type u_6} {E : B β†’ Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup EM] [NormedSpace π•œ EM] [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} [TopologicalSpace M] [ChartedSpace HM 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 : (y : M) β†’ E (b y)} {EN : Type u_8} {HN : Type u_9} {N : Type u_10} [NormedAddCommGroup EN] [NormedSpace π•œ EN] [TopologicalSpace HN] {IN : ModelWithCorners π•œ EN HN} [TopologicalSpace N] [ChartedSpace HN N] {g : N β†’ M} {y : N} (hg : MDiffAt g y) (hs : (MDiffAt fun (z : M) => (↑(trivializationAt F E (b (g y))) ⟨b z, s z⟩).2) (g y)) :
    sectionLinearization IN (b ∘ g) (fun (z : N) => s (g z)) y = sectionLinearization IM b s (g y) ∘SL mfderiv% g y

    Pulling a section back along a differentiable map precomposes its intrinsic linearization with the differential of that map. This is the chain rule used to pass between a manifold source and a source chart.