mathlib3 documentation

geometry.manifold.vector_bundle.fiberwise_linear

The groupoid of smooth, fiberwise-linear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

The groupoid of smooth, fiberwise-linear maps #

source
def fiberwise_linear.local_homeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {U : set B} (φ : B → (F ≃L[𝕜] F)) (hU : is_open U) (hφ : continuous_on (λ (x : B), ↑(φ x)) U) (h2φ : continuous_on (λ (x : B), ↑((φ x).symm)) U) :
local_homeomorph (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.

Equations
source
theorem fiberwise_linear.trans_local_homeomorph_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {φ φ' : B → (F ≃L[𝕜] F)} {U U' : set B} (hU : is_open U) (hφ : continuous_on (λ (x : B), ↑(φ x)) U) (h2φ : continuous_on (λ (x : B), ↑((φ x).symm)) U) (hU' : is_open U') (hφ' : continuous_on (λ (x : B), ↑(φ' x)) U') (h2φ' : continuous_on (λ (x : B), ↑((φ' x).symm)) U') (b : B) (v : F) :
⇑((fiberwise_linear.local_homeomorph φ hU hφ h2φ).trans (fiberwise_linear.local_homeomorph φ' hU' hφ' h2φ')) (b, v) = (b, ⇑(φ' b) (⇑(φ b) v))

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

source
theorem fiberwise_linear.source_trans_local_homeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {φ φ' : B → (F ≃L[𝕜] F)} {U U' : set B} (hU : is_open U) (hφ : continuous_on (λ (x : B), ↑(φ x)) U) (h2φ : continuous_on (λ (x : B), ↑((φ x).symm)) U) (hU' : is_open U') (hφ' : continuous_on (λ (x : B), ↑(φ' x)) U') (h2φ' : continuous_on (λ (x : B), ↑((φ' x).symm)) U') :
((fiberwise_linear.local_homeomorph φ hU hφ h2φ).trans (fiberwise_linear.local_homeomorph φ' hU' hφ' h2φ')).to_local_equiv.source = (U ∩ U') ×ˢ set.univ

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

source
theorem fiberwise_linear.target_trans_local_homeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {φ φ' : B → (F ≃L[𝕜] F)} {U U' : set B} (hU : is_open U) (hφ : continuous_on (λ (x : B), ↑(φ x)) U) (h2φ : continuous_on (λ (x : B), ↑((φ x).symm)) U) (hU' : is_open U') (hφ' : continuous_on (λ (x : B), ↑(φ' x)) U') (h2φ' : continuous_on (λ (x : B), ↑((φ' x).symm)) U') :
((fiberwise_linear.local_homeomorph φ hU hφ h2φ).trans (fiberwise_linear.local_homeomorph φ' hU' hφ' h2φ')).to_local_equiv.target = (U ∩ U') ×ˢ set.univ

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

source
theorem smooth_fiberwise_linear.locality_aux₁ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {EB : Type u_4} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_5} [topological_space HB] [charted_space HB B] {IB : model_with_corners 𝕜 EB HB} (e : local_homeomorph (B × F) (B × F)) (h : ∀ (p : B × F), p ∈ e.to_local_equiv.source → (∃ (s : set (B × F)), is_open s ∧ p ∈ s ∧ ∃ (φ : B → (F ≃L[𝕜] F)) (u : set B) (hu : is_open u) (hφ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑(φ x)) u) (h2φ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑((φ x).symm)) u), (e.restr s).eq_on_source (fiberwise_linear.local_homeomorph φ hu _ _))) :
∃ (U : set B) (hU : e.to_local_equiv.source = U ×ˢ set.univ), ∀ (x : B), x ∈ U → (∃ (φ : B → (F ≃L[𝕜] F)) (u : set B) (hu : is_open u) (huU : u ⊆ U) (hux : x ∈ u) (hφ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑(φ x)) u) (h2φ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑((φ x).symm)) u), (e.restr (u ×ˢ set.univ)).eq_on_source (fiberwise_linear.local_homeomorph φ hu _ _))

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.

source
theorem smooth_fiberwise_linear.locality_aux₂ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {EB : Type u_4} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_5} [topological_space HB] [charted_space HB B] {IB : model_with_corners 𝕜 EB HB} (e : local_homeomorph (B × F) (B × F)) (U : set B) (hU : e.to_local_equiv.source = U ×ˢ set.univ) (h : ∀ (x : B), x ∈ U → (∃ (φ : B → (F ≃L[𝕜] F)) (u : set B) (hu : is_open u) (hUu : u ⊆ U) (hux : x ∈ u) (hφ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑(φ x)) u) (h2φ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑((φ x).symm)) u), (e.restr (u ×ˢ set.univ)).eq_on_source (fiberwise_linear.local_homeomorph φ hu _ _))) :
∃ (Φ : B → (F ≃L[𝕜] F)) (U : set B) (hU₀ : is_open U) (hΦ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑(Φ x)) U) (h2Φ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑((Φ x).symm)) U), e.eq_on_source (fiberwise_linear.local_homeomorph Φ hU₀ _ _)

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 structure_groupoid 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 smooth_fiberwise_linear.

source
def smooth_fiberwise_linear {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {EB : Type u_4} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_5} [topological_space HB] [charted_space HB B] (IB : model_with_corners 𝕜 EB HB) :
structure_groupoid (B × F)

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.

Equations
Instances for smooth_fiberwise_linear
source
@[simp]
theorem mem_smooth_fiberwise_linear_iff {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [topological_space B] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {EB : Type u_4} [normed_add_comm_group EB] [normed_space 𝕜 EB] {HB : Type u_5} [topological_space HB] [charted_space HB B] (IB : model_with_corners 𝕜 EB HB) (e : local_homeomorph (B × F) (B × F)) :
e ∈ smooth_fiberwise_linear B F IB ↔ ∃ (φ : B → (F ≃L[𝕜] F)) (U : set B) (hU : is_open U) (hφ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑(φ x)) U) (h2φ : smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (x : B), ↑((φ x).symm)) U), e.eq_on_source (fiberwise_linear.local_homeomorph φ hU _ _)