Pullbacks of fibre bundles

Four facts about Mathlib's pullback bundle f *ᵖ E, whose fibre over x is the fibre of E over f x, needed to pull back bundles with extra structure on their fibres or on their atlas.

• The fibres of f *ᵖ E carry the actions of a monoid on the fibres of E (Bundle.Pullback.instMulAction), as Mathlib already does for module structures. This is what makes the pullback of a principal bundle again carry a right action on its fibres.
• The coordinate change between the pullbacks e.pullback f and e'.pullback f of two trivializations, over a point x with f x in the base set of e, is the coordinate change between e and e' over f x (Bundle.Trivialization.coordChange_pullback). This transfers regularity of the coordinate changes of E to those of f *ᵖ E.
• The canonical lift Bundle.Pullback.lift f : TotalSpace F (f *ᵖ E) → TotalSpace F E has range (π F E) ⁻¹' Set.range f and inherits injectivity, inducingness, and topological (or open / closed) embedding properties from f (Bundle.Pullback.isEmbedding_lift).
• A map into the total space of f *ᵖ E is continuous exactly when its projection and its lift to the total space of E are (Bundle.Pullback.continuous_iff).

@[instance_reducible]

instance Bundle.Pullback.instMulAction {B : Type u_1} {B' : Type u_2} {M : Type u_3} [Monoid M] {E : B → Type u_4} [i : (b : B) → MulAction M (E b)] (f : B' → B) (x : B') : MulAction M ((f *ᵖ E) x)

The fibres of a pullback bundle f *ᵖ E carry the actions on the fibres of E: the fibre over x is the fibre of E over f x.

@[simp]

theorem Bundle.Pullback.range_lift {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} (f : B' → B) : Set.range (lift f) = TotalSpace.proj ⁻¹' Set.range f

The canonical lift from the pullback total space f *ᵖ E to E has image equal to the part of E lying over the range of f.

theorem Bundle.Pullback.lift_injective {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} {f : B' → B} (hf : Function.Injective f) : Function.Injective (lift f)

If f is injective, the canonical lift Pullback.lift f on total spaces is injective.

theorem Bundle.Pullback.continuous_iff {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] {Z : Type u_5} [TopologicalSpace Z] {f : B' → B} {g : Z → TotalSpace F (f *ᵖ E)} : Continuous g ↔ (Continuous fun (z : Z) => (g z).proj) ∧ Continuous fun (z : Z) => lift f (g z)

A map into the total space of a pullback bundle f *ᵖ E is continuous exactly when its projection to the new base and its lift to the total space of E are continuous.

theorem Bundle.Pullback.isInducing_lift_of_continuous_proj {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] {f : B' → B} (hf : Topology.IsInducing f) (hπ : Continuous TotalSpace.proj) : Topology.IsInducing (lift f)

If f is a topological inducing map and the projection π F E is continuous, then Pullback.lift f is a topological inducing map.

theorem Bundle.Pullback.isInducing_lift {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [TopologicalSpace F] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {f : B' → B} (hf : Topology.IsInducing f) : Topology.IsInducing (lift f)

Along a topological inducing map f, the canonical lift Pullback.lift f of a fibre bundle is a topological inducing map.

theorem Bundle.Pullback.isEmbedding_lift {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [TopologicalSpace F] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {f : B' → B} (hf : Topology.IsEmbedding f) : Topology.IsEmbedding (lift f)

Along a topological embedding f, the canonical lift Pullback.lift f of a fibre bundle is a topological embedding.

theorem Bundle.Pullback.isClosedEmbedding_lift {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [TopologicalSpace F] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {f : B' → B} (hf : Topology.IsClosedEmbedding f) : Topology.IsClosedEmbedding (lift f)

Along a closed embedding f, the canonical lift Pullback.lift f of a fibre bundle is a closed embedding.

theorem Bundle.Pullback.isOpenEmbedding_lift {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [TopologicalSpace F] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {f : B' → B} (hf : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding (lift f)

Along an open embedding f, the canonical lift Pullback.lift f of a fibre bundle is an open embedding.

theorem Bundle.Trivialization.coordChange_pullback {B : Type u_1} {B' : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [∀ (b : B), Nonempty (E b)] {K : Type u_5} [FunLike K B' B] [ContinuousMapClass K B' B] (e e' : Trivialization F TotalSpace.proj) (f : K) {x : B'} (hx : f x ∈ e.baseSet) (v : F) : (e.pullback f).coordChange (e'.pullback f) x v = e.coordChange e' (f x) v

The coordinate change between the pullbacks of two trivializations, over a point x whose image f x lies in the base set of the first, is the coordinate change between the trivializations over f x.