Vector bundles

Stream: new members

[Nicolò Cavalleri]

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!