# Zulip Chat Archive

## Stream: new members

### Topic: Vector bundles

#### Nicolò Cavalleri (Jul 10 2020 at 10:53):

In the topic Lie groups and Lie algebras of the stream maths, Sebastien said, regarding vector bundles:

You have a type, a projection, and you want to express the fact that this projection corresponds to a vector bundle. So you want to express that you have a vector space structure on the fibers, continuous and locally trivial. How to write this data? What I want to avoid is requiring that the underlying type is $E \times F$, or $\Sigma (x : E), F_x$ with some topology: the setup should cover both situations (and other natural situations), just like the predicate for topological fiber bundles does. For instance, the two following definition would work.

`import topology.topological_fiber_bundle import analysis.normed_space.basic namespace vector_bundle1 variables (𝕜 : Type*) {B : Type*} (F : Type*) {Z : Type*} [topological_space B] [topological_space Z] [normed_field 𝕜] [topological_space F] [add_comm_group F] [module 𝕜 F] [topological_module 𝕜 F] (proj : Z → B) [∀ (x : B), add_comm_group {y // proj y = x}] [∀ (x : B), module 𝕜 {y // proj y = x}] [∀ (x : B), topological_module 𝕜 {y // proj y = x}] structure vector_bundle_trivialization extends bundle_trivialization F proj := (linear : ∀ x ∈ base_set, is_linear_map 𝕜 (λ (y : {y // proj y = x}), (to_fun y).2)) def is_topological_vector_bundle : Prop := ∀ x : Z, ∃e : vector_bundle_trivialization 𝕜 F proj, x ∈ e.source end vector_bundle1`

Here, I require that typeclass inference knows about the topological vector space structure on the fibers of the projection, written as

`{y // proj y = x}`

(which is defeq to`proj ⁻¹' {x}`

, but synctactically different so one should choose a representation and use it constantly if one wants typeclass inference to succeed).

I am trying to understand the pros and the cons of this possible definition, but I do not understand the sentence "one should choose a representation and use it constantly if one wants typeclass inference to succeed" and I am wondering if someone could tell me more about what the word representation refers to here.

My knowledge of Lean up to now only makes me think of trying to define a natural bijection between `{y // proj y = x}`

and `tangent_bundle I M`

(that I actually can't define but I can try harder) to define manually an instance of vector space on the fibers via something like

```
import geometry.manifold.basic_smooth_bundle
variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{H : Type*} [topological_space H] {I : model_with_corners 𝕜 E H}
{M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
def F : Π x : M, {y : tangent_bundle I M // tangent_bundle.proj I M y = x} → tangent_space I x :=
sorry,
def G : Π x : M, tangent_space I x → {y : tangent_bundle I M // tangent_bundle.proj I M y = x} :=
sorry,
instance add_comm_group_fiber_tangent_bundle : ∀ (x : M), add_comm_group {y : tangent_bundle I M // tangent_bundle.proj I M y = x} :=
λ x,
{ add := λ a b, G x (F x a + F x b),
add_assoc := sorry,
zero := sorry,
zero_add := sorry,
add_zero := sorry,
neg := sorry,
add_left_neg := sorry,
add_comm := sorry, }
```

but the above sentence seems to suggest there is something more natural, so I was wondering if someone can confirm this!

Last updated: May 14 2021 at 03:27 UTC