Documentation

Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

The groupoid of smooth, fiberwise-linear maps #

This file contains preliminaries for the definition of a smooth vector bundle: an associated StructureGroupoid, the groupoid of smoothFiberwiseLinear functions.

The groupoid of smooth, fiberwise-linear maps #

def FiberwiseLinear.localHomeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {U : Set B} (φ : BF ≃L[𝕜] F) (hU : IsOpen U) (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) U) :
LocalHomeomorph (B × F) (B × F)

For B a topological space and F a 𝕜-normed space, a map from U : Set B to F ≃L[𝕜] F determines a local homeomorphism from B × F to itself by its action fiberwise.

Instances For
    theorem FiberwiseLinear.trans_localHomeomorph_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : BF ≃L[𝕜] F} {φ' : BF ≃L[𝕜] F} {U : Set B} {U' : Set B} (hU : IsOpen U) (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) U) (hU' : IsOpen U') (hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ' x))) U') (b : B) (v : F) :
    ↑(LocalHomeomorph.trans (FiberwiseLinear.localHomeomorph φ hU h2φ) (FiberwiseLinear.localHomeomorph φ' hU' hφ' h2φ')) (b, v) = (b, ↑(φ' b) (↑(φ b) v))

    Compute the composition of two local homeomorphisms induced by fiberwise linear equivalences.

    theorem FiberwiseLinear.source_trans_localHomeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : BF ≃L[𝕜] F} {φ' : BF ≃L[𝕜] F} {U : Set B} {U' : Set B} (hU : IsOpen U) (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) U) (hU' : IsOpen U') (hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ' x))) U') :
    (LocalHomeomorph.trans (FiberwiseLinear.localHomeomorph φ hU h2φ) (FiberwiseLinear.localHomeomorph φ' hU' hφ' h2φ')).toLocalEquiv.source = (U U') ×ˢ Set.univ

    Compute the source of the composition of two local homeomorphisms induced by fiberwise linear equivalences.

    theorem FiberwiseLinear.target_trans_localHomeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : BF ≃L[𝕜] F} {φ' : BF ≃L[𝕜] F} {U : Set B} {U' : Set B} (hU : IsOpen U) (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) U) (hU' : IsOpen U') (hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ' x))) U') :
    (LocalHomeomorph.trans (FiberwiseLinear.localHomeomorph φ hU h2φ) (FiberwiseLinear.localHomeomorph φ' hU' hφ' h2φ')).toLocalEquiv.target = (U U') ×ˢ Set.univ

    Compute the target of the composition of two local homeomorphisms induced by fiberwise linear equivalences.

    theorem SmoothFiberwiseLinear.locality_aux₁ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {EB : Type u_4} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_5} [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} (e : LocalHomeomorph (B × F) (B × F)) (h : ∀ (p : B × F), p e.sources, IsOpen s p s φ u hu h2φ, LocalHomeomorph.EqOnSource (LocalHomeomorph.restr e s) (FiberwiseLinear.localHomeomorph φ hu (_ : ContinuousOn (fun x => ↑(φ x)) u) (_ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) u))) :
    U, e.source = U ×ˢ Set.univ ∀ (x : B), x Uφ u hu _huU _hux h2φ, LocalHomeomorph.EqOnSource (LocalHomeomorph.restr e (u ×ˢ Set.univ)) (FiberwiseLinear.localHomeomorph φ hu (_ : ContinuousOn (fun x => ↑(φ x)) u) (_ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) u))

    Let e be a local homeomorphism of B × F. Suppose that at every point p in the source of e, there is some neighbourhood s of p on which e is equal to a bi-smooth fiberwise linear local homeomorphism. Then the source of e is of the form U ×ˢ univ, for some set U in B, and, at any point x in U, admits a neighbourhood u of x such that e is equal on u ×ˢ univ to some bi-smooth fiberwise linear local homeomorphism.

    theorem SmoothFiberwiseLinear.locality_aux₂ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {EB : Type u_4} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_5} [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} (e : LocalHomeomorph (B × F) (B × F)) (U : Set B) (hU : e.source = U ×ˢ Set.univ) (h : ∀ (x : B), x Uφ u hu _hUu _hux h2φ, LocalHomeomorph.EqOnSource (LocalHomeomorph.restr e (u ×ˢ Set.univ)) (FiberwiseLinear.localHomeomorph φ hu (_ : ContinuousOn (fun x => ↑(φ x)) u) (_ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) u))) :
    Φ U hU₀ h2Φ, LocalHomeomorph.EqOnSource e (FiberwiseLinear.localHomeomorph Φ hU₀ (_ : ContinuousOn (fun x => ↑(Φ x)) U) (_ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (Φ x))) U))

    Let e be a local homeomorphism of B × F whose source is U ×ˢ univ, for some set U in B, and which, at any point x in U, admits a neighbourhood u of x such that e is equal on u ×ˢ univ to some bi-smooth fiberwise linear local homeomorphism. Then e itself is equal to some bi-smooth fiberwise linear local homeomorphism.

    This is the key mathematical point of the locality condition in the construction of the StructureGroupoid of bi-smooth fiberwise linear local homeomorphisms. The proof is by gluing together the various bi-smooth fiberwise linear local homeomorphism which exist locally.

    The U in the conclusion is the same U as in the hypothesis. We state it like this, because this is exactly what we need for smoothFiberwiseLinear.

    def smoothFiberwiseLinear {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {EB : Type u_4} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_5} [TopologicalSpace HB] [ChartedSpace HB B] (IB : ModelWithCorners 𝕜 EB HB) :

    For B a manifold and F a normed space, the groupoid on B × F consisting of local homeomorphisms which are bi-smooth and fiberwise linear, and induce the identity on B. When a (topological) vector bundle is smooth, then the composition of charts associated to the vector bundle belong to this groupoid.

    Instances For
      @[simp]
      theorem mem_smoothFiberwiseLinear_iff {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {EB : Type u_4} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_5} [TopologicalSpace HB] [ChartedSpace HB B] (IB : ModelWithCorners 𝕜 EB HB) (e : LocalHomeomorph (B × F) (B × F)) :
      e smoothFiberwiseLinear B F IB φ U hU h2φ, LocalHomeomorph.EqOnSource e (FiberwiseLinear.localHomeomorph φ hU (_ : ContinuousOn (fun x => ↑(φ x)) U) (_ : ContinuousOn (fun x => ↑(ContinuousLinearEquiv.symm (φ x))) U))