Trivializations over the whole base

A trivialization e of a fibre bundle E whose base set is the whole base is a homeomorphism E ≃ₜ B × F. Read through Bundle.Trivial.homeomorphProd, it is a homeomorphism of total spaces E ≃ₜ TotalSpace F (Bundle.Trivial B F) onto the trivial bundle (Bundle.Trivialization.homeomorphTrivial). It covers the identity of the base, sends v to the fibre coordinate of e v, and its inverse is the partial inverse of e (Bundle.Trivialization.homeomorphTrivial_apply, Bundle.Trivialization.homeomorphTrivial_symm_apply). For a linear trivialization of a vector bundle over a nontrivially normed field 𝕜, on the fibre over b it is the continuous linear equivalence e.continuousLinearEquivAt 𝕜 b, with inverse its symmetric (Bundle.Trivialization.homeomorphTrivial_apply_eq_continuousLinearEquivAt, Bundle.Trivialization.homeomorphTrivial_symm_apply_eq_continuousLinearEquivAt).

More generally, any linear trivialization sends a vector over its base set to a nonzero vector exactly when the vector is nonzero (Bundle.Trivialization.snd_apply_ne_zero_iff). Over the base set, its fibrewise linear inverse e.symmₗ R b is the inverse of the fibrewise linear equivalence (Bundle.Trivialization.coe_linearEquivAt_symm), hence injective (Bundle.Trivialization.symmₗ_injective). For two linear trivializations whose base sets contain b, the fibre equivalence E_b ≃ F of the second is that of the first followed by the coordinate change from the first to the second (Bundle.Trivialization.continuousLinearEquivAt_trans_coordChangeL). Linear coordinate changes satisfy the identity and cocycle laws over the relevant base sets (Bundle.Trivialization.coordChangeL_same_apply, Bundle.Trivialization.coordChangeL_coordChangeL_apply), and send the coordinate of a point in the first trivialization to its coordinate in the second (Bundle.Trivialization.coordChangeL_apply_snd). Convergence in the total space of a vector bundle is convergence of base points and of fibre coordinates in any linear trivialization over the limit point (Bundle.Trivialization.tendsto_mk_nhds_mk_iff).

We also record the product trivialization's fibrewise inverse (Bundle.Trivialization.prod_symm_apply'), the preferred trivialization of a direct-sum fibre bundle (FiberBundle.trivializationAt_prod), and scalar restriction of linear trivializations and coordinate changes (Bundle.Trivialization.isLinear_restrictScalars, Bundle.Trivialization.restrictScalars_coordChangeL).

def Bundle.Trivialization.homeomorphTrivial {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [TopologicalSpace F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] (e : Trivialization F TotalSpace.proj) (he : e.baseSet = Set.univ) : TotalSpace F E ≃ₜ TotalSpace F (Trivial B F)

The homeomorphism E ≃ₜ B × F of a trivialization over the whole base, read as a homeomorphism onto the total space of the trivial bundle.

@[simp]

theorem Bundle.Trivialization.homeomorphTrivial_apply {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [TopologicalSpace F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] (e : Trivialization F TotalSpace.proj) (he : e.baseSet = Set.univ) (v : TotalSpace F E) : (e.homeomorphTrivial he) v = TotalSpace.mk' F v.proj (↑e v).2

@[simp]

theorem Bundle.Trivialization.homeomorphTrivial_symm_apply {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [TopologicalSpace F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] (e : Trivialization F TotalSpace.proj) (he : e.baseSet = Set.univ) (w : TotalSpace F (Trivial B F)) : (e.homeomorphTrivial he).symm w = ↑e.symm (w.proj, w.snd)

theorem Bundle.Trivialization.snd_apply_ne_zero_iff {B : Type u_1} [TopologicalSpace B] (R : Type u_4) [Semiring R] {F : Type u_5} [TopologicalSpace F] [AddCommMonoid F] [Module R F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module R (E b)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear R e] {v : TotalSpace F E} (hv : v.proj ∈ e.baseSet) : (↑e v).2 ≠ 0 ↔ v.snd ≠ 0

A linear trivialization sends a vector over its base set to a nonzero vector exactly when the vector is nonzero.

theorem Bundle.Trivialization.coe_linearEquivAt_symm {B : Type u_1} [TopologicalSpace B] (R : Type u_4) [Semiring R] {F : Type u_5} [TopologicalSpace F] [AddCommMonoid F] [Module R F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module R (E b)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b ∈ e.baseSet) : ↑(linearEquivAt R e b hb).symm = Trivialization.symmₗ R e b

Over the base set, the fibrewise linear inverse of a linear trivialization is the inverse of its fibrewise linear equivalence.

theorem Bundle.Trivialization.symmₗ_injective {B : Type u_1} [TopologicalSpace B] (R : Type u_4) [Semiring R] {F : Type u_5} [TopologicalSpace F] [AddCommMonoid F] [Module R F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module R (E b)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b ∈ e.baseSet) : Function.Injective ⇑(Trivialization.symmₗ R e b)

Over the base set, the fibrewise linear inverse of a linear trivialization is injective.

theorem Bundle.Trivialization.homeomorphTrivial_apply_eq_continuousLinearEquivAt {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (he : e.baseSet = Set.univ) (v : TotalSpace F E) : (e.homeomorphTrivial he) v = TotalSpace.mk' F v.proj ((continuousLinearEquivAt 𝕜 e v.proj ⋯) v.snd)

theorem Bundle.Trivialization.homeomorphTrivial_symm_apply_eq_continuousLinearEquivAt {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (he : e.baseSet = Set.univ) (w : TotalSpace F (Trivial B F)) : (e.homeomorphTrivial he).symm w = TotalSpace.mk' F w.proj ((continuousLinearEquivAt 𝕜 e w.proj ⋯).symm w.snd)

theorem Bundle.Trivialization.tendsto_mk_nhds_mk_iff {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] {ι : Type u_7} {l : Filter ι} {x : ι → B} {x₀ : B} {ξ : (i : ι) → E (x i)} {ξ₀ : E x₀} (hx₀ : x₀ ∈ e.baseSet) : Filter.Tendsto (fun (i : ι) => TotalSpace.mk' F (x i) (ξ i)) l (nhds (TotalSpace.mk' F x₀ ξ₀)) ↔ Filter.Tendsto x l (nhds x₀) ∧ Filter.Tendsto (fun (i : ι) => (continuousLinearMapAt 𝕜 e (x i)) (ξ i)) l (nhds ((continuousLinearMapAt 𝕜 e x₀) ξ₀))

Convergence in a vector bundle, read in a linear trivialization. Vectors ξ i over points x i converge in the total space to a vector ξ₀ over a point x₀ of the base set of e exactly when x i → x₀ and the fibre coordinates e (x i) (ξ i) converge to those of ξ₀.

theorem Bundle.Trivialization.continuousLinearEquivAt_trans_coordChangeL {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e'] {b : B} (hb : b ∈ e.baseSet) (hb' : b ∈ e'.baseSet) : (continuousLinearEquivAt 𝕜 e b hb).trans (coordChangeL 𝕜 e e' b) = continuousLinearEquivAt 𝕜 e' b hb'

The fibre equivalences of two trivializations differ by the coordinate change: for linear trivializations e and e' whose base sets contain b, the equivalence E_b ≃ F given by e, followed by the coordinate change from e to e', is the one given by e'.

@[simp]

theorem Bundle.Trivialization.coordChangeL_same_apply {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] {b : B} (hb : b ∈ e.baseSet) (v : F) : (coordChangeL 𝕜 e e b) v = v

The coordinate change from a linear trivialization to itself is the identity over its base set.

@[simp]

theorem Bundle.Trivialization.coordChangeL_coordChangeL_apply {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e'] {b : B} (e'' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e''] (hb : b ∈ e.baseSet) (hb' : b ∈ e'.baseSet) (hb'' : b ∈ e''.baseSet) (v : F) : (coordChangeL 𝕜 e' e'' b) ((coordChangeL 𝕜 e e' b) v) = (coordChangeL 𝕜 e e'' b) v

Cocycle law for linear coordinate changes: over the intersection of three base sets, the coordinate change from e to e' followed by the one from e' to e'' is the coordinate change from e to e''.

theorem Bundle.Trivialization.coordChangeL_apply_snd {B : Type u_1} [TopologicalSpace B] (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module 𝕜 (E b)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e'] {p : TotalSpace F E} (hb : p.proj ∈ e.baseSet) (hb' : p.proj ∈ e'.baseSet) : (coordChangeL 𝕜 e e' p.proj) (↑e p).2 = (↑e' p).2

The linear coordinate change from e to e' sends the coordinate of a point in e to its coordinate in e'.

theorem Bundle.Trivialization.prod_symm_apply' {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} {F₂ : Type u_3} {E₁ : B → Type u_4} {E₂ : B → Type u_5} [TopologicalSpace F₁] [TopologicalSpace F₂] [TopologicalSpace (TotalSpace F₁ E₁)] [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] (e₁ : Trivialization F₁ TotalSpace.proj) (e₂ : Trivialization F₂ TotalSpace.proj) {x : B} (hx : x ∈ e₁.baseSet ∩ e₂.baseSet) (w : F₁ × F₂) : (e₁.prod e₂).symm x w = (e₁.symm x w.1, e₂.symm x w.2)

Over e₁.baseSet ∩ e₂.baseSet, the fibrewise inverse (e₁.prod e₂).symm acts componentwise.

theorem FiberBundle.trivializationAt_prod {B : Type u_1} [TopologicalSpace B] (F₁ : Type u_2) (E₁ : B → Type u_3) (F₂ : Type u_4) (E₂ : B → Type u_5) [TopologicalSpace F₁] [TopologicalSpace F₂] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] (b : B) : trivializationAt (F₁ × F₂) (fun (x : B) => E₁ x × E₂ x) b = (trivializationAt F₁ E₁ b).prod (trivializationAt F₂ E₂ b)

The preferred trivialization of E₁ ×ᵇ E₂ at b is (trivializationAt F₁ E₁ b).prod (trivializationAt F₂ E₂ b).

theorem Bundle.Trivialization.isLinear_restrictScalars {B : Type u_1} [TopologicalSpace B] (𝕜' : Type u_2) (𝕜 : Type u_3) [Semiring 𝕜'] [Semiring 𝕜] [SMul 𝕜' 𝕜] {F : Type u_4} {E : B → Type u_5} [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [AddCommMonoid F] [Module 𝕜' F] [Module 𝕜 F] [IsScalarTower 𝕜' 𝕜 F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜' (E x)] [(x : B) → Module 𝕜 (E x)] [∀ (x : B), IsScalarTower 𝕜' 𝕜 (E x)] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] : Trivialization.IsLinear 𝕜' e

A 𝕜-linear trivialization is also 𝕜'-linear for any compatible scalar action 𝕜'.

theorem Bundle.Trivialization.restrictScalars_coordChangeL {B : Type u_1} [TopologicalSpace B] (𝕜' : Type u_2) (𝕜 : Type u_3) [NontriviallyNormedField 𝕜'] [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜' 𝕜] {F : Type u_4} {E : B → Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜' F] [NormedSpace 𝕜 F] [IsScalarTower 𝕜' 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜' (E x)] [(x : B) → Module 𝕜 (E x)] (e e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜' e] [Trivialization.IsLinear 𝕜' e'] [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] {b : B} : ContinuousLinearMap.restrictScalars 𝕜' ↑(coordChangeL 𝕜 e e' b) = ↑(coordChangeL 𝕜' e e' b)

Restricting scalars of a 𝕜-linear coordinate change recovers the 𝕜'-linear coordinate change.