Theorems · Inductive type · algebraic topology

VectorPrebundle

(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)] →
            [(x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [NormedSpace R F] →
                  [TopologicalSpace B] → [(x : B) → TopologicalSpace (E x)] → Type (max (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 partial equivalences are also open partial homeomorphisms and hence vector bundle trivializations. The topology on the fibers is induced from the one on the total space. The field exists_coordChange is stated as an existential statement (instead of 3 separate fields), since it depends on propositional information (namely e e' ∈ pretrivializationAtlas). This makes it inconvenient to explicitly define a coordChange function when constructing a VectorPrebundle.

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

21 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

NontriviallyNormedFieldAddCommMonoidModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpace