Documentation

Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

The groupoid of C^n, fiberwise-linear maps #

This file contains preliminaries for the definition of a C^n vector bundle: an associated StructureGroupoid, the groupoid of contMDiffFiberwiseLinear functions.

The groupoid of C^n, fiberwise-linear maps #

def FiberwiseLinear.openPartialHomeomorph {𝕜 : 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) ( : ContinuousOn (fun (x : B) => (φ x)) U) (h2φ : ContinuousOn (fun (x : B) => (φ x).symm) U) :

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[deprecated FiberwiseLinear.openPartialHomeomorph (since := "2025-08-29")]
    def FiberwiseLinear.PartialHomeomorph {𝕜 : 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) ( : ContinuousOn (fun (x : B) => (φ x)) U) (h2φ : ContinuousOn (fun (x : B) => (φ x).symm) U) :

    Alias of FiberwiseLinear.openPartialHomeomorph.


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

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

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

      @[deprecated FiberwiseLinear.trans_openPartialHomeomorph_apply (since := "2025-08-29")]
      theorem FiberwiseLinear.trans_PartialHomeomorph_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ φ' : BF ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U) ( : ContinuousOn (fun (x : B) => (φ x)) U) (h2φ : ContinuousOn (fun (x : B) => (φ x).symm) U) (hU' : IsOpen U') (hφ' : ContinuousOn (fun (x : B) => (φ' x)) U') (h2φ' : ContinuousOn (fun (x : B) => (φ' x).symm) U') (b : B) (v : F) :
      ((openPartialHomeomorph φ hU h2φ).trans (openPartialHomeomorph φ' hU' hφ' h2φ')) (b, v) = (b, (φ' b) ((φ b) v))

      Alias of FiberwiseLinear.trans_openPartialHomeomorph_apply.


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

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

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

      @[deprecated FiberwiseLinear.source_trans_openPartialHomeomorph (since := "2025-08-29")]
      theorem FiberwiseLinear.source_trans_PartialHomeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ φ' : BF ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U) ( : ContinuousOn (fun (x : B) => (φ x)) U) (h2φ : ContinuousOn (fun (x : B) => (φ x).symm) U) (hU' : IsOpen U') (hφ' : ContinuousOn (fun (x : B) => (φ' x)) U') (h2φ' : ContinuousOn (fun (x : B) => (φ' x).symm) U') :
      ((openPartialHomeomorph φ hU h2φ).trans (openPartialHomeomorph φ' hU' hφ' h2φ')).source = (U U') ×ˢ Set.univ

      Alias of FiberwiseLinear.source_trans_openPartialHomeomorph.


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

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

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

      @[deprecated FiberwiseLinear.target_trans_openPartialHomeomorph (since := "2025-08-29")]
      theorem FiberwiseLinear.target_trans_PartialHomeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ φ' : BF ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U) ( : ContinuousOn (fun (x : B) => (φ x)) U) (h2φ : ContinuousOn (fun (x : B) => (φ x).symm) U) (hU' : IsOpen U') (hφ' : ContinuousOn (fun (x : B) => (φ' x)) U') (h2φ' : ContinuousOn (fun (x : B) => (φ' x).symm) U') :
      ((openPartialHomeomorph φ hU h2φ).trans (openPartialHomeomorph φ' hU' hφ' h2φ')).target = (U U') ×ˢ Set.univ

      Alias of FiberwiseLinear.target_trans_openPartialHomeomorph.


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

      theorem ContMDiffFiberwiseLinear.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} (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F)) (h : pe.source, ∃ (s : Set (B × F)), IsOpen s p s ∃ (φ : BF ≃L[𝕜] F) (u : Set B) (hu : IsOpen u) ( : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x)) u) (h2φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x).symm) u), (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu )) :
      ∃ (U : Set B), e.source = U ×ˢ Set.univ xU, ∃ (φ : BF ≃L[𝕜] F) (u : Set B) (hu : IsOpen u) (_ : u U) (_ : x u) ( : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x)) u) (h2φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x).symm) u), (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu )

      Let e be an open partial 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-C^n fiberwise linear open partial 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-C^n fiberwise linear open partial homeomorphism.

      theorem ContMDiffFiberwiseLinear.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} (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F)) (U : Set B) (hU : e.source = U ×ˢ Set.univ) (h : xU, ∃ (φ : BF ≃L[𝕜] F) (u : Set B) (hu : IsOpen u) (_ : u U) (_ : x u) ( : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x)) u) (h2φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x).symm) u), (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu )) :
      ∃ (Φ : BF ≃L[𝕜] F) (U : Set B) (hU₀ : IsOpen U) ( : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (Φ x)) U) (h2Φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (Φ x).symm) U), e.EqOnSource (FiberwiseLinear.openPartialHomeomorph Φ hU₀ )

      Let e be an open partial 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-C^n fiberwise linear open partial homeomorphism. Then e itself is equal to some bi-C^n fiberwise linear open partial homeomorphism.

      This is the key mathematical point of the locality condition in the construction of the StructureGroupoid of bi-C^n fiberwise linear open partial homeomorphisms. The proof is by gluing together the various bi-C^n fiberwise linear open partial 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 contMDiffFiberwiseLinear.

      def contMDiffFiberwiseLinear {𝕜 : 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) (n : WithTop ℕ∞) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem mem_contMDiffFiberwiseLinear_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) {n : WithTop ℕ∞} (e : OpenPartialHomeomorph (B × F) (B × F)) :
        e contMDiffFiberwiseLinear B F IB n ∃ (φ : BF ≃L[𝕜] F) (U : Set B) (hU : IsOpen U) ( : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x)) U) (h2φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => (φ x).symm) U), e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU )