mathlib3 documentation

topology.vector_bundle.basic

Vector bundles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define (topological) vector bundles.

Let B be the base space, let F be a normed space over a normed field R, and let E : B → Type* be a fiber_bundle with fiber F, in which, for each x, the fiber E x is a topological vector space over R.

To have a vector bundle structure on bundle.total_space F E, one should additionally have the following properties:

If these conditions are satisfied, we register the typeclass vector_bundle R F E.

We define constructions on vector bundles like pullbacks and direct sums in other files.

Main Definitions #

Implementation notes #

The implementation choices in the vector bundle definition are discussed in the "Implementation notes" section of topology.fiber_bundle.basic.

Tags #

Vector bundle

@[class]
structure pretrivialization.is_linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) :
Prop

A mixin class for pretrivialization, stating that a pretrivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

Instances of this typeclass
theorem pretrivialization.linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] (e : pretrivialization F bundle.total_space.proj) [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) :
is_linear_map R (λ (x : E b), (e {proj := b, snd := x}).snd)
@[protected]
noncomputable def pretrivialization.symmₗ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) :
F →ₗ[R] E b

A fiberwise linear inverse to e.

Equations
@[simp]
theorem pretrivialization.symmₗ_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (y : F) :
@[simp]
theorem pretrivialization.linear_equiv_at_symm_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (hb : b e.base_set) :
@[simp]
theorem pretrivialization.linear_equiv_at_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (hb : b e.base_set) :
(pretrivialization.linear_equiv_at R e b hb) = λ (y : E b), (e {proj := b, snd := y}).snd
noncomputable def pretrivialization.linear_equiv_at (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) (hb : b e.base_set) :
E b ≃ₗ[R] F

A pretrivialization for a vector bundle defines linear equivalences between the fibers and the model space.

Equations
@[protected]
noncomputable def pretrivialization.linear_map_at (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) :
E b →ₗ[R] F

A fiberwise linear map equal to e on e.base_set.

Equations
theorem pretrivialization.coe_linear_map_at {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] (b : B) :
(pretrivialization.linear_map_at R e b) = λ (y : E b), ite (b e.base_set) (e {proj := b, snd := y}).snd 0
theorem pretrivialization.coe_linear_map_at_of_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) :
(pretrivialization.linear_map_at R e b) = λ (y : E b), (e {proj := b, snd := y}).snd
theorem pretrivialization.linear_map_at_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (y : E b) :
theorem pretrivialization.linear_map_at_eq_zero {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) :
theorem pretrivialization.symmₗ_linear_map_at {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : E b) :
theorem pretrivialization.linear_map_at_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : pretrivialization F bundle.total_space.proj) [pretrivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : F) :
@[class]
structure trivialization.is_linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) :
Prop

A mixin class for trivialization, stating that a trivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

Instances of this typeclass
@[protected]
theorem trivialization.linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] (e : trivialization F bundle.total_space.proj) [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [trivialization.is_linear R e] {b : B} (hb : b e.base_set) :
is_linear_map R (λ (y : E b), (e {proj := b, snd := y}).snd)
noncomputable def trivialization.linear_equiv_at (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) :
E b ≃ₗ[R] F

A trivialization for a vector bundle defines linear equivalences between the fibers and the model space.

Equations
@[simp]
theorem trivialization.linear_equiv_at_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) (v : E b) :
(trivialization.linear_equiv_at R e b hb) v = (e {proj := b, snd := v}).snd
@[simp]
theorem trivialization.linear_equiv_at_symm_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) (v : F) :
@[protected]
noncomputable def trivialization.symmₗ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
F →ₗ[R] E b

A fiberwise linear inverse to e.

Equations
theorem trivialization.coe_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
@[protected]
noncomputable def trivialization.linear_map_at (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
E b →ₗ[R] F

A fiberwise linear map equal to e on e.base_set.

Equations
theorem trivialization.coe_linear_map_at {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
(trivialization.linear_map_at R e b) = λ (y : E b), ite (b e.base_set) (e {proj := b, snd := y}).snd 0
theorem trivialization.coe_linear_map_at_of_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {b : B} (hb : b e.base_set) :
(trivialization.linear_map_at R e b) = λ (y : E b), (e {proj := b, snd := y}).snd
theorem trivialization.linear_map_at_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {b : B} (y : E b) :
(trivialization.linear_map_at R e b) y = ite (b e.base_set) (e {proj := b, snd := y}).snd 0
theorem trivialization.symmₗ_linear_map_at {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : E b) :
theorem trivialization.linear_map_at_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {b : B} (hb : b e.base_set) (y : F) :
noncomputable def trivialization.coord_changeL (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] (b : B) :
F ≃L[R] F

A coordinate change function between two trivializations, as a continuous linear equivalence. Defined to be the identity when b does not lie in the base set of both trivializations.

Equations
theorem trivialization.coord_changeL_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] {b : B} (hb : b e.base_set e'.base_set) (y : F) :
(trivialization.coord_changeL R e e' b) y = (e' {proj := b, snd := e.symm b y}).snd
theorem trivialization.mk_coord_changeL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] {b : B} (hb : b e.base_set e'.base_set) (y : F) :
(b, (trivialization.coord_changeL R e e' b) y) = e' {proj := b, snd := e.symm b y}
theorem trivialization.coord_changeL_apply' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [semiring R] [topological_space F] [topological_space B] [topological_space (bundle.total_space F E)] [add_comm_monoid F] [module R F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] (e e' : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] [trivialization.is_linear R e'] {b : B} (hb : b e.base_set e'.base_set) (y : F) :

A version of coord_change_apply that fully unfolds coord_change. The right-hand side is ugly, but has good definitional properties for specifically defined trivializations.

def bundle.zero_section {B : Type u_2} (F : Type u_3) (E : B Type u_4) [Π (x : B), has_zero (E x)] :

The zero section of a vector bundle

Equations
@[simp]
theorem bundle.zero_section_proj {B : Type u_2} (F : Type u_3) (E : B Type u_4) [Π (x : B), has_zero (E x)] (x : B) :
@[simp]
theorem bundle.zero_section_snd {B : Type u_2} (F : Type u_3) (E : B Type u_4) [Π (x : B), has_zero (E x)] (x : B) :
@[class]
structure vector_bundle (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B Type u_4) [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] :
Prop

The space total_space F E (for E : B → Type* such that each E x is a topological vector space) has a topological vector space structure with fiber F (denoted with vector_bundle R F E) if around every point there is a fiber bundle trivialization which is linear in the fibers.

Instances of this typeclass
@[protected, instance]
noncomputable def trivialization.continuous_linear_map_at (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
E b →L[R] F

Forward map of continuous_linear_equiv_at (only propositionally equal), defined everywhere (0 outside domain).

Equations
@[simp]
noncomputable def trivialization.symmL (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) :
F →L[R] E b

Backwards map of continuous_linear_equiv_at, defined everywhere.

Equations
@[simp]
theorem trivialization.continuous_linear_equiv_at_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) :
(trivialization.continuous_linear_equiv_at R e b hb) = λ (y : E b), (e {proj := b, snd := y}).snd
noncomputable def trivialization.continuous_linear_equiv_at (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] (b : B) (hb : b e.base_set) :
E b ≃L[R] F

In a vector bundle, a trivialization in the fiber (which is a priori only linear) is in fact a continuous linear equiv between the fibers and the model fiber.

Equations
@[protected]
theorem trivialization.zero_section (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [topological_space (bundle.total_space F E)] [Π (x : B), topological_space (E x)] [fiber_bundle F E] (e : trivialization F bundle.total_space.proj) [trivialization.is_linear R e] {x : B} (hx : x e.base_set) :
e (bundle.zero_section F E x) = (x, 0)

Constructing vector bundles #

structure vector_bundle_core (R : Type u_1) (B : Type u_2) (F : Type u_3) [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] (ι : Type u_5) :
Type (max u_2 u_3 u_5)

Analogous construction of fiber_bundle_core for vector bundles. This construction gives a way to construct vector bundles from a structure registering how trivialization changes act on fibers.

Instances for vector_bundle_core

The trivial vector bundle core, in which all the changes of coordinates are the identity.

Equations
@[protected, instance]
Equations
@[simp]
theorem vector_bundle_core.coord_change_linear_comp {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i j k : ι) (x : B) (H : x Z.base_set i Z.base_set j Z.base_set k) :
(Z.coord_change j k x).comp (Z.coord_change i j x) = Z.coord_change i k x
@[nolint]
def vector_bundle_core.index {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) :
Type u_5

The index set of a vector bundle core, as a convenience function for dot notation

Equations
@[nolint, reducible]
def vector_bundle_core.base {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) :
Type u_2

The base space of a vector bundle core, as a convenience function for dot notation

Equations
@[protected, instance]
Equations
@[protected, instance]
def vector_bundle_core.module_fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (x : B) :
module R (Z.fiber x)
Equations
@[protected, instance]
Equations
@[protected, simp, reducible]

The projection from the total space of a fiber bundle core, on its base.

Equations
@[protected, nolint, reducible]
def vector_bundle_core.total_space {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) :
Type (max u_2 u_3)

The total space of the vector bundle, as a convenience function for dot notation. It is by definition equal to bundle.total_space Z.fiber.

Equations
def vector_bundle_core.triv_change {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i j : ι) :
local_homeomorph (B × F) (B × F)

Local homeomorphism version of the trivialization change.

Equations
@[simp]
theorem vector_bundle_core.mem_triv_change_source {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i j : ι) (p : B × F) :
@[protected, instance]

Topological structure on the total space of a vector bundle created from core, designed so that all the local trivialization are continuous.

Equations
@[simp]
theorem vector_bundle_core.coe_coord_change {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (b : B) (i j : ι) :

One of the standard local trivializations of a vector bundle constructed from core, taken by considering this in particular as a fiber bundle constructed from core.

Equations
Instances for vector_bundle_core.local_triv
@[protected, instance]

The standard local trivializations of a vector bundle constructed from core are linear.

@[simp]
theorem vector_bundle_core.base_set_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i : ι) :
@[simp]
theorem vector_bundle_core.local_triv_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i : ι) (p : Z.total_space) :
(Z.local_triv i) p = (p.proj, (Z.coord_change (Z.index_at p.proj) i p.proj) p.snd)
@[simp]
theorem vector_bundle_core.local_triv_symm_fst {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i : ι) (p : B × F) :
@[simp]
theorem vector_bundle_core.local_triv_symm_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i : ι) {b : B} (hb : b Z.base_set i) (v : F) :
(Z.local_triv i).symm b v = (Z.coord_change i (Z.index_at b) b) v
@[simp]
theorem vector_bundle_core.local_triv_coord_change_eq {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (i j : ι) {b : B} (hb : b Z.base_set i Z.base_set j) (v : F) :

Preferred local trivialization of a vector bundle constructed from core, at a given point, as a bundle trivialization

Equations
@[simp]
theorem vector_bundle_core.local_triv_at_def {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (b : B) :
@[simp]
theorem vector_bundle_core.mem_source_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (b : B) (a : F) :
@[simp]
theorem vector_bundle_core.local_triv_at_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (p : Z.total_space) :
(Z.local_triv_at p.proj) p = (p.proj, p.snd)
@[simp]
theorem vector_bundle_core.local_triv_at_apply_mk {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) (b : B) (a : F) :
(Z.local_triv_at b) {proj := b, snd := a} = (b, a)
@[simp]
@[protected, instance]
Equations
@[protected, instance]
@[continuity]

The projection on the base of a vector bundle created from core is continuous

The projection on the base of a vector bundle created from core is an open map

@[simp]
theorem vector_bundle_core.local_triv_symmL {R : Type u_1} {B : Type u_2} {F : Type u_3} [nontrivially_normed_field R] [normed_add_comm_group F] [normed_space R F] [topological_space B] {ι : Type u_5} (Z : vector_bundle_core R B F ι) {i : ι} {b : B} (hb : b Z.base_set i) :

Vector prebundle #

@[nolint]
structure vector_prebundle (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B Type u_4) [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] :
Type (max u_2 u_3 u_4)

This structure permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space or the fibers. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphisms and hence vector bundle trivializations. The topology on the fibers is induced from the one on the total space.

The field exists_coord_change is stated as an existential statement (instead of 3 separate fields), since it depends on propositional information (namely e e' ∈ pretrivialization_atlas). This makes it inconvenient to explicitly define a coord_change function when constructing a vector_prebundle.

Instances for vector_prebundle
  • vector_prebundle.has_sizeof_inst
noncomputable def vector_prebundle.coord_change {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) {e e' : pretrivialization F bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) (b : B) :
F →L[R] F

A randomly chosen coordinate change on a vector_prebundle, given by the field exists_coord_change.

Equations
theorem vector_prebundle.coord_change_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) {e e' : pretrivialization F bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.base_set e'.base_set) (v : F) :
(a.coord_change he he' b) v = (e' {proj := b, snd := e.symm b v}).snd
theorem vector_prebundle.mk_coord_change {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) {e e' : pretrivialization F bundle.total_space.proj} (he : e a.pretrivialization_atlas) (he' : e' a.pretrivialization_atlas) {b : B} (hb : b e.base_set e'.base_set) (v : F) :
(b, (a.coord_change he he' b) v) = e' {proj := b, snd := e.symm b v}
def vector_prebundle.total_space_topology {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) :

Topology on the total space that will make the prebundle into a bundle.

Equations
theorem vector_prebundle.mem_trivialization_at_source {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) (b : B) (x : E b) :
@[continuity]
theorem vector_prebundle.continuous_total_space_mk {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) (b : B) :
def vector_prebundle.to_fiber_bundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) :

Make a fiber_bundle from a vector_prebundle; auxiliary construction for vector_prebundle.vector_bundle.

Equations
theorem vector_prebundle.to_vector_bundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B Type u_4} [nontrivially_normed_field R] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module R (E x)] [normed_add_comm_group F] [normed_space R F] [topological_space B] [Π (x : B), topological_space (E x)] (a : vector_prebundle R F E) :

Make a vector_bundle from a vector_prebundle. Concretely this means that, given a vector_prebundle structure for a sigma-type E -- which consists of a number of "pretrivializations" identifying parts of E with product spaces U × F -- one establishes that for the topology constructed on the sigma-type using vector_prebundle.total_space_topology, these "pretrivializations" are actually "trivializations" (i.e., homeomorphisms with respect to the constructed topology).

noncomputable def continuous_linear_map.in_coordinates {B : Type u_2} (F : Type u_3) (E : B Type u_4) [Π (x : B), add_comm_monoid (E x)] [normed_add_comm_group F] [topological_space B] [Π (x : B), topological_space (E x)] {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [nontrivially_normed_field 𝕜₁] [nontrivially_normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [topological_space B'] [normed_space 𝕜₁ F] [Π (x : B), module 𝕜₁ (E x)] [topological_space (bundle.total_space F E)] (F' : Type u_8) [normed_add_comm_group F'] [normed_space 𝕜₂ F'] (E' : B' Type u_9) [Π (x : B'), add_comm_monoid (E' x)] [Π (x : B'), module 𝕜₂ (E' x)] [topological_space (bundle.total_space F' E')] [fiber_bundle F E] [vector_bundle 𝕜₁ F E] [Π (x : B'), topological_space (E' x)] [fiber_bundle F' E'] [vector_bundle 𝕜₂ F' E'] (x₀ x : B) (y₀ y : B') (ϕ : E x →SL[σ] E' y) :
F →SL[σ] F'

When ϕ is a continuous (semi)linear map between the fibers E x and E' y of two vector bundles E and E', continuous_linear_map.in_coordinates F E F' E' x₀ x y₀ y ϕ is a coordinate change of this continuous linear map w.r.t. the chart around x₀ and the chart around y₀.

It is defined by composing ϕ with appropriate coordinate changes given by the vector bundles E and E'. We use the operations trivialization.continuous_linear_map_at and trivialization.symmL in the definition, instead of trivialization.continuous_linear_equiv_at, so that continuous_linear_map.in_coordinates is defined everywhere (but see continuous_linear_map.in_coordinates_eq).

This is the (second component of the) underlying function of a trivialization of the hom-bundle (see hom_trivialization_at_apply). However, note that continuous_linear_map.in_coordinates is defined even when x and y live in different base sets. Therefore, it is is also convenient when working with the hom-bundle between pulled back bundles.

Equations
theorem continuous_linear_map.in_coordinates_eq {B : Type u_2} {F : Type u_3} (E : B Type u_4) [Π (x : B), add_comm_monoid (E x)] [normed_add_comm_group F] [topological_space B] [Π (x : B), topological_space (E x)] {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [nontrivially_normed_field 𝕜₁] [nontrivially_normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [topological_space B'] [normed_space 𝕜₁ F] [Π (x : B), module 𝕜₁ (E x)] [topological_space (bundle.total_space F E)] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕜₂ F'] (E' : B' Type u_9) [Π (x : B'), add_comm_monoid (E' x)] [Π (x : B'), module 𝕜₂ (E' x)] [topological_space (bundle.total_space F' E')] [fiber_bundle F E] [vector_bundle 𝕜₁ F E] [Π (x : B'), topological_space (E' x)] [fiber_bundle F' E'] [vector_bundle 𝕜₂ F' E'] (x₀ x : B) (y₀ y : B') (ϕ : E x →SL[σ] E' y) (hx : x (fiber_bundle.trivialization_at F E x₀).base_set) (hy : y (fiber_bundle.trivialization_at F' E' y₀).base_set) :

rewrite in_coordinates using continuous linear equivalences.

@[protected]
theorem continuous_linear_map.vector_bundle_core.in_coordinates_eq {B : Type u_2} {F : Type u_3} [normed_add_comm_group F] [topological_space B] {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [nontrivially_normed_field 𝕜₁] [nontrivially_normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [topological_space B'] [normed_space 𝕜₁ F] {F' : Type u_8} [normed_add_comm_group F'] [normed_space 𝕜₂ F'] {ι : Type u_1} {ι' : Type u_4} (Z : vector_bundle_core 𝕜₁ B F ι) (Z' : vector_bundle_core 𝕜₂ B' F' ι') {x₀ x : B} {y₀ y : B'} (ϕ : F →SL[σ] F') (hx : x Z.base_set (Z.index_at x₀)) (hy : y Z'.base_set (Z'.index_at y₀)) :
continuous_linear_map.in_coordinates F Z.fiber F' Z'.fiber x₀ x y₀ y ϕ = (Z'.coord_change (Z'.index_at y) (Z'.index_at y₀) y).comp (ϕ.comp (Z.coord_change (Z.index_at x₀) (Z.index_at x) x))

rewrite in_coordinates in a vector_bundle_core.