Trivializations from local frames, and trivial line bundles

Let V → B be a C^n vector bundle whose model fibre F has a finite basis b. A C^n local frame s of V on an open set U (in the sense of Mathlib's IsLocalFrameOn) determines a linear trivialization over U: a vector v ∈ V x is sent to the vector of F having the same coordinates in b as v has in the frame s · x. This file constructs that trivialization and shows that it belongs to the maximal atlas of trivializations compatible with the C^n structure of V. Conversely, for a member e of that maximal atlas, the sections x ↦ e.symm x (b i) form a C^n local frame on its base set. So V admits a compatible trivialization over U exactly when it admits a C^n local frame on U.

Read in a trivialization e' of the bundle's atlas, the frame becomes a family of invertible operators of F, the coordinate change from the frame trivialization to e'. Its entries are the coordinates of the frame sections in e', hence C^n, and its inverse is C^n because operator inversion is smooth. This gives both the continuity needed to define the trivialization and its C^n compatibility with the atlas. The same construction for continuous local frames of a family of subspaces of a topological vector bundle, with the subspace topology, is TauCeti.IsSubbundleFrameOn.trivialization. Mathlib's Bundle.Trivialization.localFrame gives the converse direction for trivializations of the bundle's own atlas.

For a bundle of rank one a single section that vanishes nowhere on U is a local frame on U. Hence a line bundle admits a compatible trivialization over U exactly when it has a C^n section without zeros on U; with U = univ, it is trivial exactly when it has a nowhere-zero C^n section. Over the model 𝓘(ℂ, EB) with n = ∞, the maximal atlas consists of the holomorphic trivializations of a holomorphic vector bundle, and this is the criterion that a holomorphic line bundle is holomorphically trivial exactly when it has a nowhere-vanishing holomorphic section.

Main definitions

• IsLocalFrameOn.trivialization: the trivialization over U defined by a local frame on an open set U and a basis of the model fibre.

Main results

• IsLocalFrameOn.contMDiffOn_coeff: a Cᵐ section has Cᵐ coefficients in a Cⁿ frame, for m ≤ n.
• IsLocalFrameOn.trivialization_mem_maximalAtlas: the trivialization of a C^n local frame lies in the maximal atlas of C^n trivializations.
• Bundle.Trivialization.isLocalFrameOn_symm_of_mem_maximalAtlas: a member of the maximal atlas carries the basis of the model fibre to a C^n local frame on its base set.
• ContMDiffVectorBundle.exists_trivialization_baseSet_eq_iff_exists_isLocalFrameOn: a compatible trivialization over an open set exists exactly when a C^n local frame on it does.
• IsLocalFrameOn.of_finrank_eq_one: in a bundle of rank one, a section without zeros is a frame.
• ContMDiffVectorBundle.exists_trivialization_baseSet_eq_univ_iff_exists_ne_zero: a line bundle has a global compatible trivialization exactly when it has a nowhere-zero C^n section.

References

• Daniel Huybrechts, Complex Geometry: An Introduction, Springer, 2005, Section 2.2 (holomorphic vector bundles, local frames and trivializations).
• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 10 (local frames and the local trivializations associated with them).

Coordinates in a frame

The frame read in a trivialization

The trivialization

noncomputable def IsLocalFrameOn.trivialization {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) : Bundle.Trivialization F Bundle.TotalSpace.proj

The trivialization of V over an open set U defined by a local frame s on U and a basis b of the model fibre: over U, a vector of V x is sent to the vector of F with the same coordinates in b as it has in the frame s · x.

@[simp]

theorem IsLocalFrameOn.baseSet_trivialization {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) : (hs.trivialization hU b).baseSet = U

theorem IsLocalFrameOn.trivialization_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) {x : B} (hx : x ∈ U) (v : V x) : ↑(hs.trivialization hU b) ⟨x, v⟩ = (x, ((hs.toBasisAt hx).equiv b (Equiv.refl ι)) v)

Over U, the frame trivialization sends a vector to the vector of F with the same coordinates in b as it has in the frame.

@[simp]

theorem IsLocalFrameOn.trivialization_apply_frame {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) {x : B} (hx : x ∈ U) (i : ι) : ↑(hs.trivialization hU b) ⟨x, s i x⟩ = (x, b i)

Over U, the frame trivialization sends the frame vector s i x to the basis vector b i.

@[simp]

theorem IsLocalFrameOn.trivialization_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) [Fintype ι] {x : B} (hx : x ∈ U) (w : F) : (hs.trivialization hU b).symm x w = ∑ i : ι, (b.repr w) i • s i x

Over U, the inverse of the frame trivialization sends w to the combination of the frame with coefficients b.repr w.

instance IsLocalFrameOn.isLinear_trivialization {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) : Bundle.Trivialization.IsLinear 𝕜 (hs.trivialization hU b)

The frame trivialization is fibrewise linear.

theorem IsLocalFrameOn.trivialization_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [Finite ι] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) [ContMDiffVectorBundle n F V IB] : (hs.trivialization hU b).toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (Bundle.TotalSpace F V) (contMDiffFiberwiseLinear B F IB n)

Local frames give compatible trivializations. The trivialization defined by a C^n local frame lies in the maximal atlas of trivializations compatible with the C^n structure of the bundle.

theorem IsLocalFrameOn.contMDiffOn_coeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} {s : ι → (x : B) → V x} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [FiniteDimensional 𝕜 F] {m : WithTop ℕ∞} [ContMDiffVectorBundle m F V IB] (hs : IsLocalFrameOn IB F n s U) (hU : IsOpen U) (hm : m ≤ n) {σ : (x : B) → V x} (hσ : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) m (fun (x : B) => ⟨x, σ x⟩) U) (i : ι) : ContMDiffOn IB (modelWithCornersSelf 𝕜 𝕜) m (fun (x : B) => (hs.coeff i x) (σ x)) U

The coefficients of a C^m section in a C^n local frame on an open set are C^m, provided m ≤ n.

Frames from compatible trivializations

theorem Bundle.Trivialization.isLocalFrameOn_symm_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} [VectorBundle 𝕜 F V] [ContMDiffVectorBundle n F V IB] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F V) (contMDiffFiberwiseLinear B F IB n)) (b : Module.Basis ι 𝕜 F) : IsLocalFrameOn IB F n (fun (i : ι) (x : B) => e.symm x (b i)) e.baseSet

Compatible trivializations give local frames. A member e of the maximal atlas of C^n trivializations carries a basis b of the model fibre to the C^n local frame x ↦ e.symm x (b i) on its base set.

theorem ContMDiffVectorBundle.exists_trivialization_baseSet_eq_iff_exists_isLocalFrameOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} [CompleteSpace 𝕜] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle n F V IB] [Finite ι] (hU : IsOpen U) (b : Module.Basis ι 𝕜 F) : (∃ (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (_ : Bundle.Trivialization.IsLinear 𝕜 e), e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (Bundle.TotalSpace F V) (contMDiffFiberwiseLinear B F IB n) ∧ e.baseSet = U) ↔ ∃ (s : ι → (x : B) → V x), IsLocalFrameOn IB F n s U

A C^n vector bundle whose model fibre has a finite basis indexed by ι admits a trivialization over an open set U in the maximal atlas of C^n trivializations exactly when it admits a C^n local frame on U indexed by ι.

Line bundles

theorem IsLocalFrameOn.of_finrank_eq_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {ι : Type u_7} {U : Set B} [VectorBundle 𝕜 F V] [Unique ι] (hF : Module.finrank 𝕜 F = 1) {σ : (x : B) → V x} (hσ : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => ⟨x, σ x⟩) U) (hσ₀ : ∀ x ∈ U, σ x ≠ 0) : IsLocalFrameOn IB F n (fun (x : ι) => σ) U

In a vector bundle of rank one, a C^n section without zeros on U is a C^n local frame on U, indexed by any type with a single element.

theorem ContMDiffVectorBundle.exists_trivialization_baseSet_eq_iff_exists_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} {U : Set B} [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [ContMDiffVectorBundle n F V IB] (hF : Module.finrank 𝕜 F = 1) (hU : IsOpen U) : (∃ (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (_ : Bundle.Trivialization.IsLinear 𝕜 e), e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (Bundle.TotalSpace F V) (contMDiffFiberwiseLinear B F IB n) ∧ e.baseSet = U) ↔ ∃ (σ : (x : B) → V x), ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => ⟨x, σ x⟩) U ∧ ∀ x ∈ U, σ x ≠ 0

A C^n line bundle admits a trivialization over an open set U in the maximal atlas of C^n trivializations exactly when it has a C^n section without zeros on U.

theorem ContMDiffVectorBundle.exists_trivialization_baseSet_eq_univ_iff_exists_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] {n : WithTop ℕ∞} [VectorBundle 𝕜 F V] [CompleteSpace 𝕜] [ContMDiffVectorBundle n F V IB] (hF : Module.finrank 𝕜 F = 1) : (∃ (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (_ : Bundle.Trivialization.IsLinear 𝕜 e), e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (Bundle.TotalSpace F V) (contMDiffFiberwiseLinear B F IB n) ∧ e.baseSet = Set.univ) ↔ ∃ (σ : (x : B) → V x), (ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : B) => ⟨x, σ x⟩) ∧ ∀ (x : B), σ x ≠ 0

The trivial line bundle criterion. A C^n line bundle has a trivialization over the whole base in the maximal atlas of C^n trivializations, that is, it is trivial as a C^n vector bundle, exactly when it has a C^n section that vanishes nowhere. For a holomorphic line bundle, over 𝓘(ℂ, EB) with n = ∞, this says that it is holomorphically trivial exactly when it has a nowhere-vanishing holomorphic section.