Fibres and linear charts of pullback bundles

The fibres of f *ᵖ E inherit their additive group, topological module, normed and inner product structures and their scalar towers from E (f x). Mathlib supplies the additive monoid and module structures. The topological group structures let fibrewise linear equivalences between pullbacks, such as the pullback x ↦ e (f x) of a family of fibrewise linear equivalences e, induce maps of total spaces with continuous inverses. The normed instances allow the orthonormal frame bundle of a pullback to use exactly the original fibre metrics, with no transport or renorming. A pulled-back linear trivialization also induces the original fibre equivalence at the image point (Bundle.Trivialization.linearEquivAt_pullback and Bundle.Trivialization.continuousLinearEquivAt_pullback). Hom coordinates between pullbacks by two different base maps agree with the original source and target coordinates (ContinuousLinearMap.inCoordinates_pullback_of_mem).

@[instance_reducible]

instance Bundle.Pullback.instAddCommGroup {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) [(b : B) → AddCommGroup (E b)] (x : B') : AddCommGroup ((f *ᵖ E) x)

A pullback fibre carries the additive group structure of the original fibre.

instance Bundle.Pullback.instIsTopologicalAddGroup {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) [(b : B) → AddCommGroup (E b)] [(b : B) → TopologicalSpace (E b)] [∀ (b : B), IsTopologicalAddGroup (E b)] (x : B') : IsTopologicalAddGroup ((f *ᵖ E) x)

Addition and negation on a pullback fibre are continuous when they are on the original fibre.

instance Bundle.Pullback.instContinuousSMul {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) {R : Type u_4} [Semiring R] [TopologicalSpace R] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module R (E b)] [(b : B) → TopologicalSpace (E b)] [∀ (b : B), ContinuousSMul R (E b)] (x : B') : ContinuousSMul R ((f *ᵖ E) x)

Scalar multiplication on a pullback fibre is continuous when it is on the original fibre.

instance Bundle.Pullback.instIsScalarTower {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) {R : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [SMul R S] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module R (E b)] [(b : B) → Module S (E b)] [∀ (b : B), IsScalarTower R S (E b)] (x : B') : IsScalarTower R S ((f *ᵖ E) x)

Scalar multiplications on a pullback fibre form a tower when they do on the original fibre, for instance the real and complex scalar multiplications of a complex vector bundle.

@[instance_reducible]

instance Bundle.Pullback.instNormedAddCommGroup {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) [(b : B) → NormedAddCommGroup (E b)] (x : B') : NormedAddCommGroup ((f *ᵖ E) x)

A pullback fibre carries the normed additive group structure of the original fibre.

@[instance_reducible]

instance Bundle.Pullback.instNormedSpace {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) {𝕜 : Type u_4} [NormedField 𝕜] [(b : B) → NormedAddCommGroup (E b)] [(b : B) → NormedSpace 𝕜 (E b)] (x : B') : NormedSpace 𝕜 ((f *ᵖ E) x)

Scalar multiplication on a normed pullback fibre has the original norm bound.

@[instance_reducible]

instance Bundle.Pullback.instInnerProductSpace {B : Type u_1} {B' : Type u_2} {E : B → Type u_3} (f : B' → B) {𝕜 : Type u_4} [RCLike 𝕜] [(b : B) → NormedAddCommGroup (E b)] [(b : B) → InnerProductSpace 𝕜 (E b)] (x : B') : InnerProductSpace 𝕜 ((f *ᵖ E) x)

The inner product on a pullback fibre is the original fibre inner product.

@[simp]

theorem Bundle.Trivialization.linearEquivAt_pullback {𝕜 : Type u_1} {B : Type u_2} {B' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [TopologicalSpace B] [TopologicalSpace B'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] {K : Type u_6} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (f : K) (b : B') (hb : b ∈ (e.pullback f).baseSet) : linearEquivAt 𝕜 (e.pullback f) b hb = linearEquivAt 𝕜 e (f b) ⋯

A pulled-back linear chart gives the original fibre equivalence at the image point.

@[simp]

theorem Bundle.Trivialization.continuousLinearEquivAt_pullback {𝕜 : Type u_1} {B : Type u_2} {B' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [TopologicalSpace B] [TopologicalSpace B'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_5} [(b : B) → AddCommGroup (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (TotalSpace F V)] [FiberBundle F V] {K : Type u_6} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (f : K) (x : B') (hx : x ∈ (e.pullback f).baseSet) : continuousLinearEquivAt 𝕜 (e.pullback f) x hx = continuousLinearEquivAt 𝕜 e (f x) ⋯

A pulled-back continuous linear fibre chart is the original chart at the image point.

instance Bundle.Trivialization.memTrivializationAtlas_pullback {B : Type u_1} {B' : Type u_2} {F : Type u_3} {V : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace F] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [∀ (x : B), Nonempty (V x)] [FiberBundle F V] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] (f : C(B', B)) : MemTrivializationAtlas (e.pullback f)

Pulling back an atlas trivialization gives an atlas trivialization of the native pullback bundle.

theorem ContinuousLinearMap.inCoordinates_pullback_of_mem {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} {X : Type u_4} {F : Type u_5} {G : Type u_6} {K : Type u_7} {L : Type u_8} [NontriviallyNormedField 𝕜] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace X] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {V : B → Type u_9} {W : C → Type u_10} [(b : B) → AddCommGroup (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [(c : C) → AddCommGroup (W c)] [(c : C) → Module 𝕜 (W c)] [(c : C) → TopologicalSpace (W c)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] [TopologicalSpace (Bundle.TotalSpace G W)] [FiberBundle G W] [VectorBundle 𝕜 G W] [FunLike K X B] [ContinuousMapClass K X B] [FunLike L X C] [ContinuousMapClass L X C] (f : K) (g : L) (x₀ x : X) (A : V (f x) →L[𝕜] W (g x)) (hV : f x ∈ (trivializationAt F V (f x₀)).baseSet) (hW : g x ∈ (trivializationAt G W (g x₀)).baseSet) : inCoordinates F (⇑f *ᵖ V) G (⇑g *ᵖ W) x₀ x x₀ x A = inCoordinates F V G W (f x₀) (f x) (g x₀) (g x) A

The hom-bundle coordinates between two pullbacks are the original source and target coordinates at their image points, on the common chart domain.