Orientations of real vector bundles

An orientation of a real vector bundle E → B with finite-dimensional model fibre F is a choice of an orientation of every fibre E b that varies continuously with b. Continuity is read in local trivializations: a linear trivialization e identifies the fibre over each point of its base set with F, so it reads a family of fibre orientations as a family of orientations of the single space F (Bundle.Trivialization.mapOrientation), and the family is continuous when these readings are locally constant.

A TauCeti.VectorBundleOrientation F E ι asks for this in the preferred trivialization at every point. When ι has cardinality the rank of the bundle, the coordinate changes between trivializations of the atlas have continuous, nowhere-vanishing determinants, so local constancy in one trivialization of the atlas implies it in every other (Bundle.Trivialization.eventually_mapOrientation_eq_of_eventually): an orientation is locally constant in every trivialization of the atlas (TauCeti.VectorBundleOrientation.eventually_mapOrientation_eq), and conversely it suffices to check local constancy in any chosen trivializations of the atlas (TauCeti.VectorBundleOrientation.ofEventually).

An orientation of a plane bundle (ι = Fin 2) is the data on which the Euler class of the bundle in H²(B; ℤ) depends, the opposite orientation giving the opposite class. Over a preconnected base an orientation is determined by its value at a single point: two orientations either agree or are opposite (TauCeti.VectorBundleOrientation.eq_or_eq_neg). The trivial bundle B × F carries the constant orientations (TauCeti.VectorBundleOrientation.trivial), and over a preconnected base these are all of its orientations (TauCeti.VectorBundleOrientation.eq_trivial).

Main definitions

• Bundle.Trivialization.mapOrientation: an orientation of a fibre, read in a trivialization as an orientation of the model fibre.
• TauCeti.VectorBundleOrientation F E ι: an orientation of the vector bundle E.
• TauCeti.VectorBundleOrientation.ofEventually: an orientation from local constancy in chosen trivializations of the atlas.
• TauCeti.VectorBundleOrientation.trivial: the constant orientations of a trivial bundle.
• TauCeti.VectorBundleOrientation.pullback: the pullback of an orientation along a continuous map of bases.

Main results

• TauCeti.VectorBundleOrientation.eventually_mapOrientation_eq: an orientation is locally constant when read in any trivialization of the atlas.
• TauCeti.VectorBundleOrientation.eq_or_eq_neg: over a preconnected base, two orientations of a bundle are equal or opposite.
• TauCeti.VectorBundleOrientation.eq_trivial: over a preconnected base, every orientation of a trivial bundle is constant.

References

• J. W. Milnor, J. D. Stasheff, Characteristic Classes, Annals of Mathematics Studies 76, Princeton (1974), §9 (oriented vector bundles and the Euler class).

noncomputable def Bundle.Trivialization.mapOrientation {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] (ι : Type u_4) (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear ℝ e] {b : B} (hb : b ∈ e.baseSet) : Orientation ℝ (E b) ι ≃ Orientation ℝ F ι

An orientation of the fibre over a point b of the base set of a linear trivialization e, read as an orientation of the model fibre: its transport along the linear equivalence E b ≃ F given by e.

theorem Bundle.Trivialization.mapOrientation_apply {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear ℝ e] {b : B} (hb : b ∈ e.baseSet) (o : Orientation ℝ (E b) ι) : (mapOrientation ι e hb) o = (Orientation.map ι (linearEquivAt ℝ e b hb)) o

@[simp]

theorem Bundle.Trivialization.mapOrientation_pullback {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} {B' : Type u_5} [TopologicalSpace 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) (o : Orientation ℝ (E (f b)) ι) : (mapOrientation ι (e.pullback f) hb) o = (mapOrientation ι e ⋯) o

Reading an orientation in a pulled-back chart agrees with reading it in the original chart at the image point.

@[simp]

theorem Bundle.Trivialization.mapOrientation_neg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear ℝ e] {b : B} (hb : b ∈ e.baseSet) (o : Orientation ℝ (E b) ι) : (mapOrientation ι e hb) (-o) = -(mapOrientation ι e hb) o

theorem Bundle.Trivialization.mapOrientation_eq_map_coordChangeL {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} (e e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear ℝ e] [Trivialization.IsLinear ℝ e'] {b : B} (hb : b ∈ e.baseSet) (hb' : b ∈ e'.baseSet) (o : Orientation ℝ (E b) ι) : (mapOrientation ι e' hb') o = (Orientation.map ι ↑(coordChangeL ℝ e e' b)) ((mapOrientation ι e hb) o)

Reading a fibre orientation in a second trivialization applies the coordinate change to its reading in the first.

theorem Bundle.Trivialization.mapOrientation_eq_orientation_iff {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_4} {E' : B → Type u_5} [TopologicalSpace (TotalSpace F E')] [(b : B) → AddCommGroup (E' b)] [(b : B) → Module ℝ (E' b)] [Fintype ι] [DecidableEq ι] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear ℝ e] {b : B} (hb : b ∈ e.baseSet) (β : Module.Basis ι ℝ F) (o : Orientation ℝ (E' b) ι) : (mapOrientation ι e hb) o = β.orientation ↔ o = (β.map (linearEquivAt ℝ e b hb).symm).orientation

Reading an orientation of a fibre in a linear trivialization e gives the orientation of a basis β of the model fibre exactly when the orientation is that of the basis of the fibre carried from β by e.

theorem Bundle.Trivialization.eventually_mapOrientation_eq_of_eventually {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Fintype ι] (hι : Fintype.card ι = Module.finrank ℝ F) (e e' : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {o : (b : B) → Orientation ℝ (E b) ι} {b : B} (hb : b ∈ e.baseSet) (hb' : b ∈ e'.baseSet) (h : ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ e.baseSet), (mapOrientation ι e hx) (o x) = (mapOrientation ι e hb) (o b)) : ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ e'.baseSet), (mapOrientation ι e' hx) (o x) = (mapOrientation ι e' hb') (o b)

If a family of fibre orientations is locally constant near b when read in one trivialization of the atlas, then it is locally constant near b when read in any other, provided ι has cardinality the rank of the bundle: the coordinate change has continuous nonvanishing determinant, whose sign is therefore locally constant.

theorem Bundle.Trivialization.eventually_mapOrientation_symm_eq {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Fintype ι] (hι : Fintype.card ι = Module.finrank ℝ F) (e e' : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {b : B} (hb : b ∈ e.baseSet) (hb' : b ∈ e'.baseSet) (o : Orientation ℝ F ι) : ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ e.baseSet) (hx' : x ∈ e'.baseSet), (mapOrientation ι e' hx') ((mapOrientation ι e hx).symm o) = (mapOrientation ι e' hb') ((mapOrientation ι e hb).symm o)

The fibre orientations read as a fixed orientation o of the model fibre in one trivialization e of the atlas are locally constant when read in any other trivialization e' of the atlas, provided ι has cardinality the rank of the bundle.

structure TauCeti.VectorBundleOrientation {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] (ι : Type u_4) [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] : Type (max (max u_1 u_3) u_4)

An orientation of the real vector bundle E with model fibre F, indexed by ι: an orientation of every fibre, such that near each point b the orientations of the fibres, read in the preferred trivialization at b, all agree with that of the fibre over b. This is meaningful when ι has cardinality the rank of the bundle; it is the condition that the fibre orientations vary continuously with the base point.

• toFun (b : B) : Orientation ℝ (E b) ι

  The orientation of the fibre over each point.

• eventually_mapOrientation_eq' (b : B) : ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ (trivializationAt F E b).baseSet), (Bundle.Trivialization.mapOrientation ι (trivializationAt F E b) hx) (self.toFun x) = (Bundle.Trivialization.mapOrientation ι (trivializationAt F E b) ⋯) (self.toFun b)

  The fibre orientations are locally constant in the preferred trivializations.

@[instance_reducible]

instance TauCeti.VectorBundleOrientation.instDFunLikeOrientationReal {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] : DFunLike (VectorBundleOrientation F E ι) B fun (b : B) => Orientation ℝ (E b) ι

@[simp]

theorem TauCeti.VectorBundleOrientation.coe_mk {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (o : (b : B) → Orientation ℝ (E b) ι) (ho : ∀ (b : B), ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ (trivializationAt F E b).baseSet), (Bundle.Trivialization.mapOrientation ι (trivializationAt F E b) hx) (o x) = (Bundle.Trivialization.mapOrientation ι (trivializationAt F E b) ⋯) (o b)) : ⇑{ toFun := o, eventually_mapOrientation_eq' := ho } = o

theorem TauCeti.VectorBundleOrientation.ext {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {o o' : VectorBundleOrientation F E ι} (h : ∀ (b : B), o b = o' b) : o = o'

theorem TauCeti.VectorBundleOrientation.ext_iff {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {o o' : VectorBundleOrientation F E ι} : o = o' ↔ ∀ (b : B), o b = o' b

@[instance_reducible]

instance TauCeti.VectorBundleOrientation.instNeg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] : Neg (VectorBundleOrientation F E ι)

The opposite orientation, reversing the orientation of every fibre.

@[simp]

theorem TauCeti.VectorBundleOrientation.neg_apply {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (o : VectorBundleOrientation F E ι) (b : B) : (-o) b = -o b

theorem TauCeti.VectorBundleOrientation.neg_neg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (o : VectorBundleOrientation F E ι) : - -o = o

@[instance_reducible]

instance TauCeti.VectorBundleOrientation.instInvolutiveNeg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] : InvolutiveNeg (VectorBundleOrientation F E ι)

theorem TauCeti.VectorBundleOrientation.ne_neg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Nonempty B] (o : VectorBundleOrientation F E ι) : o ≠ -o

Over a nonempty base, an orientation differs from the opposite orientation.

def TauCeti.VectorBundleOrientation.trivial (B : Type u_1) [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_4} (o : Orientation ℝ F ι) : VectorBundleOrientation F (Bundle.Trivial B F) ι

The constant orientation o of the fibres of the trivial bundle B × F.

@[simp]

theorem TauCeti.VectorBundleOrientation.trivial_apply {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_4} (o : Orientation ℝ F ι) (b : B) : (trivial B o) b = o

@[simp]

theorem TauCeti.VectorBundleOrientation.neg_trivial {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_4} (o : Orientation ℝ F ι) : -trivial B o = trivial B (-o)

def TauCeti.VectorBundleOrientation.pullback {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {B' : Type u_5} [TopologicalSpace B'] (f : C(B', B)) (o : VectorBundleOrientation F E ι) : VectorBundleOrientation F (⇑f *ᵖ E) ι

The pullback of an orientation along a continuous map f : B' → B: the orientation of the pullback bundle f*E whose fibre over b' is oriented as the fibre of E over f b'.

@[simp]

theorem TauCeti.VectorBundleOrientation.pullback_apply {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {B' : Type u_5} [TopologicalSpace B'] (f : C(B', B)) (o : VectorBundleOrientation F E ι) (b' : B') : (pullback f o) b' = o (f b')

@[simp]

theorem TauCeti.VectorBundleOrientation.pullback_neg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] {B' : Type u_5} [TopologicalSpace B'] (f : C(B', B)) (o : VectorBundleOrientation F E ι) : pullback f (-o) = -pullback f o

theorem TauCeti.VectorBundleOrientation.isOpen_setOf_eq {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (o o' : VectorBundleOrientation F E ι) : IsOpen {b : B | o b = o' b}

The set of points where two orientations agree is open.

theorem TauCeti.VectorBundleOrientation.eventually_mapOrientation_eq {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Fintype ι] (hι : Fintype.card ι = Module.finrank ℝ F) (o : VectorBundleOrientation F E ι) (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] {b : B} (hb : b ∈ e.baseSet) : ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ e.baseSet), (Bundle.Trivialization.mapOrientation ι e hx) (o x) = (Bundle.Trivialization.mapOrientation ι e hb) (o b)

An orientation is locally constant when read in any trivialization of the atlas.

def TauCeti.VectorBundleOrientation.ofEventually {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Fintype ι] (hι : Fintype.card ι = Module.finrank ℝ F) (o : (b : B) → Orientation ℝ (E b) ι) (e : B → Bundle.Trivialization F Bundle.TotalSpace.proj) [∀ (b : B), MemTrivializationAtlas (e b)] (he : ∀ (b : B), b ∈ (e b).baseSet) (ho : ∀ (b : B), ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ (e b).baseSet), (Bundle.Trivialization.mapOrientation ι (e b) hx) (o x) = (Bundle.Trivialization.mapOrientation ι (e b) ⋯) (o b)) : VectorBundleOrientation F E ι

An orientation of the bundle from fibre orientations that are locally constant near each point b when read in some trivialization e b of the atlas whose base set contains b.

@[simp]

theorem TauCeti.VectorBundleOrientation.coe_ofEventually {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Fintype ι] (hι : Fintype.card ι = Module.finrank ℝ F) (o : (b : B) → Orientation ℝ (E b) ι) (e : B → Bundle.Trivialization F Bundle.TotalSpace.proj) [∀ (b : B), MemTrivializationAtlas (e b)] (he : ∀ (b : B), b ∈ (e b).baseSet) (ho : ∀ (b : B), ∀ᶠ (x : B) in nhds b, ∀ (hx : x ∈ (e b).baseSet), (Bundle.Trivialization.mapOrientation ι (e b) hx) (o x) = (Bundle.Trivialization.mapOrientation ι (e b) ⋯) (o b)) : ⇑(ofEventually hι o e he ho) = o

theorem TauCeti.VectorBundleOrientation.eq_or_eq_neg {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → AddCommMonoid (E b)] [(b : B) → Module ℝ (E b)] {ι : Type u_4} [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [Fintype ι] [FiniteDimensional ℝ F] [PreconnectedSpace B] (hι : Fintype.card ι = Module.finrank ℝ F) (o o' : VectorBundleOrientation F E ι) : o = o' ∨ o = -o'

Over a preconnected base, two orientations of a bundle of rank card ι either agree or are opposite.

theorem TauCeti.VectorBundleOrientation.eq_trivial {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ F] [PreconnectedSpace B] (hι : Fintype.card ι = Module.finrank ℝ F) (o : VectorBundleOrientation F (Bundle.Trivial B F) ι) (b : B) : o = trivial B (o b)

Over a preconnected base, an orientation of a trivial bundle of rank card ι is the constant orientation given by its value at any point.