Pretrivialization.linear
theorem Pretrivialization.linear :
∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace B] (e : Pretrivialization F Bundle.TotalSpace.proj) [inst_3 : AddCommMonoid F]
[inst_4 : Module R F] [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
[inst_7 : Pretrivialization.IsLinear R e] {b : B},
b ∈ e.baseSet → IsLinearMap R fun x => (↑e { proj := b, snd := x }).2
The theorem `Pretrivialization.linear` states that for any semiring `R`, type `B`, type `F`, and a type `E` dependent on `B`, given the necessary topological space, additive commutative monoid and module structures, if a certain `Pretrivialization F Bundle.TotalSpace.proj` is linear (as specified by the `Pretrivialization.IsLinear R e` instance), then for any element `b` of type `B` that belongs to the base set of the pretrivialization `e`, the map that takes an element `x` and maps it to the second component of the pretrivialization applied to the pair `(b, x)` is a linear map over the semiring `R`.
More concisely: Given a semiring `R`, a type `B`, a type `F`, a pretrivialization `e` over `B` with base type `B`, and assuming the necessary topological space, additive commutative monoid, and module structures, if `Pretrivialization.IsLinear R e` holds, then for each `b` in `B`, the map `x ↔> e b x.2` is a linear map over `R`.
|
VectorBundleCore.isOpenMap_proj
theorem VectorBundleCore.isOpenMap_proj :
∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
IsOpenMap Z.proj
This theorem states that the projection on the base of a vector bundle created from the core is an open map. Here, an open map is a function that takes any open set from one topological space and maps it to an open set in another topological space. The theorem applies to any non-trivially normed field `R`, normed add commutative group `F`, topological space `B`, and any type `ι`, given a `VectorBundleCore` `Z` defined over these structures. The projection of this vector bundle, `Z.proj`, is guaranteed to be an open map.
More concisely: Given a non-trivially normed field `R`, normed add commutative group `F`, topological space `B`, and a `VectorBundleCore` `Z` over these structures, the projection map `Z.proj` is an open function.
|
VectorPrebundle.toVectorBundle
theorem VectorPrebundle.toVectorBundle :
∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
[inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
(a : VectorPrebundle R F E), VectorBundle R F E
The theorem `VectorPrebundle.toVectorBundle` states that we can construct a `VectorBundle` from a `VectorPrebundle`. In more concrete terms, if we have a `VectorPrebundle` structure for a sigma-type `E` -- which is given by a number of "pretrivializations" that identify parts of `E` with product spaces `U × F` -- we can establish that, for the topology constructed on the sigma-type using `VectorPrebundle.totalSpaceTopology`, these "pretrivializations" are actually "trivializations". That is, they are homeomorphisms with respect to the constructed topology. This theorem is defined for any types `R`, `B`, `F`, `E`, where `R` is a nontrivially normed field, `B` is a topological space, `F` is a normed additive commutative group and a normed `R`-space, and `E` is a family of `R`-modules indexed by `B` each carrying a topology.
More concisely: Given a `VectorPrebundle` structure on a sigma-type `E` with topology `VectorPrebundle.totalSpaceTopology`, the given "pretrivializations" are homeomorphisms.
|
VectorBundleCore.continuous_proj
theorem VectorBundleCore.continuous_proj :
∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
Continuous Z.proj
This theorem states that for any vector bundle, denoted by `Z`, the projection onto its base is a continuous function. Here, the vector bundle is defined over a base `B` with fibers `F` equipped with a normed vector space structure over a non-trivially normed field `R`. The type `ι` corresponds to the indices of the local trivializations of the vector bundle. So, in simple terms, no matter how we choose the vector bundle, the operation of projecting a point in the bundle down to its base always gives us a continuous function.
More concisely: For any vector bundle `Z` over a base `B` with fibers equipped with a normed vector space structure over a non-trivially normed field `R`, the projection function is a continuous function.
|
Trivialization.coordChangeL_apply'
theorem Trivialization.coordChangeL_apply' :
∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
[inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
(e e' : Trivialization F Bundle.TotalSpace.proj) [inst_8 : Trivialization.IsLinear R e]
[inst_9 : Trivialization.IsLinear R e'] {b : B},
b ∈ e.baseSet ∩ e'.baseSet → ∀ (y : F), (Trivialization.coordChangeL R e e' b) y = (↑e' (↑e.symm (b, y))).2
This theorem, "Trivialization.coordChangeL_apply'", states that for given types `R`, `B`, `F`, and `E`, with `R` being a semiring, `F`, `B`, and `Bundle.TotalSpace F E` being topological spaces, `F` being an additive commutative monoid and a module over `R`, and `E x` for each `x` in `B` being an additive commutative monoid and a module over `R`, and given two trivializations `e` and `e'` of the fiber bundle with base `B` and fiber `F`, where both `e` and `e'` are linear over `R`, for any point `b` in the intersection of the base sets of `e` and `e'`, for any `y` in `F`, the value of the coordinate change from `e` to `e'` at `b`, applied to `y`, is equal to the second component of the image under `e'` of the preimage under the inverse of `e` of the pair `(b, y)`. This theorem reveals an explicit form of the coordinate change between two trivializations, though at the cost of a somewhat convoluted expression.
More concisely: For trivializations `e` and `e'` of a fiber bundle with base space `B`, fiber `F`, and given that both are linear over a semiring `R`, the coordinate change from `e` to `e'` at a point `b` in their base sets is equal to the second component of the image under `e'` of the preimage under the inverse of `e` of `(b, y)` for any `y` in `F`.
|