Trivializations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
Basic definitions #
-
trivialization F p: structure extending local homeomorphisms, defining a local trivialization of a topological spaceZwith projectionpand fiberF. -
pretrivialization F proj: trivialization as a local equivalence, mainly used when the topology on the total space has not yet been defined.
Operations on bundles #
We provide the following operations on trivializations.
trivialization.comp_homeomorph: given a local trivializationeof a fiber bundlep : Z → Band a homeomorphismh : Z' ≃ₜ Z, returns a local trivialization of the fiber bundlep ∘ h.
Implementation notes #
Previously, in mathlib, there was a structure topological_vector_bundle.trivialization which
extended another structure topological_fiber_bundle.trivialization by a linearity hypothesis. As
of PR #17359, we have changed this to a single structure trivialization (no namespace), together
with a mixin class trivialization.is_linear.
This permits all the data of a vector bundle to be held at the level of fiber bundles, so that the
same trivializations can underlie an object's structure as (say) a vector bundle over ℂ and as a
vector bundle over ℝ, as well as its structure simply as a fiber bundle.
This might be a little surprising, given the general trend of the library to ever-increased bundling. But in this case the typical motivation for more bundling does not apply: there is no algebraic or order structure on the whole type of linear (say) trivializations of a bundle. Indeed, since trivializations only have meaning on their base sets (taking junk values outside), the type of linear trivializations is not even particularly well-behaved.
theorem
pretrivialization.ext
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
{_inst_1 : topological_space B}
{_inst_2 : topological_space F}
{proj : Z → B}
(x y : pretrivialization F proj)
(h : x.to_local_equiv = y.to_local_equiv)
(h_1 : x.base_set = y.base_set) :
x = y
@[nolint, ext]
structure
pretrivialization
{B : Type u_2}
(F : Type u_3)
{Z : Type u_5}
[topological_space B]
[topological_space F]
(proj : Z → B) :
Type (max u_2 u_3 u_5)
- to_local_equiv : local_equiv Z (B × F)
- open_target : is_open self.to_local_equiv.target
- base_set : set B
- open_base_set : is_open self.base_set
- source_eq : self.to_local_equiv.source = proj ⁻¹' self.base_set
- target_eq : self.to_local_equiv.target = self.base_set ×ˢ set.univ
- proj_to_fun : ∀ (p : Z), p ∈ self.to_local_equiv.source → (self.to_local_equiv.to_fun p).fst = proj p
This structure contains the information left for a local trivialization (which is implemented
below as trivialization F proj) if the total space has not been given a topology, but we
have a topology on both the fiber and the base space. Through the construction
topological_fiber_prebundle F proj it will be possible to promote a
pretrivialization F proj to a trivialization F proj.
Instances for pretrivialization
- pretrivialization.has_sizeof_inst
- pretrivialization.has_coe_to_fun
- trivialization.pretrivialization.has_coe
theorem
pretrivialization.ext_iff
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
{_inst_1 : topological_space B}
{_inst_2 : topological_space F}
{proj : Z → B}
(x y : pretrivialization F proj) :
x = y ↔ x.to_local_equiv = y.to_local_equiv ∧ x.base_set = y.base_set
@[protected, instance]
def
pretrivialization.has_coe_to_fun
{B : Type u_2}
(F : Type u_3)
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B} :
has_coe_to_fun (pretrivialization F proj) (λ (_x : pretrivialization F proj), Z → B × F)
Equations
- pretrivialization.has_coe_to_fun F = {coe := λ (e : pretrivialization F proj), e.to_local_equiv.to_fun}
@[simp]
theorem
pretrivialization.coe_coe
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj) :
⇑(e.to_local_equiv) = ⇑e
@[simp]
theorem
pretrivialization.coe_fst
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_equiv.source) :
theorem
pretrivialization.mem_source
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z} :
theorem
pretrivialization.coe_fst'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z}
(ex : proj x ∈ e.base_set) :
@[protected]
theorem
pretrivialization.eq_on
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj) :
theorem
pretrivialization.mk_proj_snd
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_equiv.source) :
theorem
pretrivialization.mk_proj_snd'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z}
(ex : proj x ∈ e.base_set) :
def
pretrivialization.set_symm
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj) :
↥(e.to_local_equiv.target) → Z
Composition of inverse and coercion from the subtype of the target.
Equations
- e.set_symm = e.to_local_equiv.target.restrict ⇑(e.to_local_equiv.symm)
theorem
pretrivialization.mem_target
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : B × F} :
theorem
pretrivialization.proj_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : B × F}
(hx : x ∈ e.to_local_equiv.target) :
proj (⇑(e.to_local_equiv.symm) x) = x.fst
theorem
pretrivialization.proj_symm_apply'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{b : B}
{x : F}
(hx : b ∈ e.base_set) :
proj (⇑(e.to_local_equiv.symm) (b, x)) = b
theorem
pretrivialization.proj_surj_on_base_set
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
[nonempty F] :
set.surj_on proj e.to_local_equiv.source e.base_set
theorem
pretrivialization.apply_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : B × F}
(hx : x ∈ e.to_local_equiv.target) :
⇑e (⇑(e.to_local_equiv.symm) x) = x
theorem
pretrivialization.apply_symm_apply'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{b : B}
{x : F}
(hx : b ∈ e.base_set) :
⇑e (⇑(e.to_local_equiv.symm) (b, x)) = (b, x)
theorem
pretrivialization.symm_apply_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z}
(hx : x ∈ e.to_local_equiv.source) :
⇑(e.to_local_equiv.symm) (⇑e x) = x
@[simp]
theorem
pretrivialization.symm_apply_mk_proj
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_equiv.source) :
@[simp]
theorem
pretrivialization.preimage_symm_proj_base_set
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj) :
⇑(e.to_local_equiv.symm) ⁻¹' (proj ⁻¹' e.base_set) ∩ e.to_local_equiv.target = e.to_local_equiv.target
@[simp]
theorem
pretrivialization.preimage_symm_proj_inter
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e : pretrivialization F proj)
(s : set B) :
theorem
pretrivialization.target_inter_preimage_symm_source_eq
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e f : pretrivialization F proj) :
f.to_local_equiv.target ∩ ⇑(f.to_local_equiv.symm) ⁻¹' e.to_local_equiv.source = (e.base_set ∩ f.base_set) ×ˢ set.univ
theorem
pretrivialization.trans_source
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e f : pretrivialization F proj) :
theorem
pretrivialization.symm_trans_symm
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e e' : pretrivialization F proj) :
(e.to_local_equiv.symm.trans e'.to_local_equiv).symm = e'.to_local_equiv.symm.trans e.to_local_equiv
theorem
pretrivialization.symm_trans_source_eq
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e e' : pretrivialization F proj) :
theorem
pretrivialization.symm_trans_target_eq
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
(e e' : pretrivialization F proj) :
@[simp]
theorem
pretrivialization.coe_mem_source
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
(e' : pretrivialization F bundle.total_space.proj)
{b : B}
{y : E b} :
@[simp]
theorem
pretrivialization.coe_coe_fst
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
(e' : pretrivialization F bundle.total_space.proj)
{b : B}
{y : E b}
(hb : b ∈ e'.base_set) :
theorem
pretrivialization.mk_mem_target
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
(e' : pretrivialization F bundle.total_space.proj)
{x : B}
{y : F} :
theorem
pretrivialization.symm_coe_proj
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
{x : B}
{y : F}
(e' : pretrivialization F bundle.total_space.proj)
(h : x ∈ e'.base_set) :
(⇑(e'.to_local_equiv.symm) (x, y)).proj = x
@[protected]
noncomputable
def
pretrivialization.symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
(b : B)
(y : F) :
E b
A fiberwise inverse to e. This is the function F → E b that induces a local inverse
B × F → total_space F E of e on e.base_set. It is defined to be 0 outside e.base_set.
theorem
pretrivialization.symm_apply
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
theorem
pretrivialization.symm_apply_of_not_mem
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
{b : B}
(hb : b ∉ e.base_set)
(y : F) :
theorem
pretrivialization.coe_symm_of_not_mem
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
{b : B}
(hb : b ∉ e.base_set) :
theorem
pretrivialization.mk_symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
theorem
pretrivialization.symm_proj_apply
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
(z : bundle.total_space F E)
(hz : z.proj ∈ e.base_set) :
theorem
pretrivialization.symm_apply_apply_mk
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : E b) :
theorem
pretrivialization.apply_mk_symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[Π (x : B), has_zero (E x)]
(e : pretrivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
theorem
trivialization.ext_iff
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
{_inst_1 : topological_space B}
{_inst_2 : topological_space F}
{_inst_3 : topological_space Z}
{proj : Z → B}
(x y : trivialization F proj) :
x = y ↔ x.to_local_homeomorph = y.to_local_homeomorph ∧ x.base_set = y.base_set
theorem
trivialization.ext
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
{_inst_1 : topological_space B}
{_inst_2 : topological_space F}
{_inst_3 : topological_space Z}
{proj : Z → B}
(x y : trivialization F proj)
(h : x.to_local_homeomorph = y.to_local_homeomorph)
(h_1 : x.base_set = y.base_set) :
x = y
@[nolint, ext]
structure
trivialization
{B : Type u_2}
(F : Type u_3)
{Z : Type u_5}
[topological_space B]
[topological_space F]
[topological_space Z]
(proj : Z → B) :
Type (max u_2 u_3 u_5)
- to_local_homeomorph : local_homeomorph Z (B × F)
- base_set : set B
- open_base_set : is_open self.base_set
- source_eq : self.to_local_homeomorph.to_local_equiv.source = proj ⁻¹' self.base_set
- target_eq : self.to_local_homeomorph.to_local_equiv.target = self.base_set ×ˢ set.univ
- proj_to_fun : ∀ (p : Z), p ∈ self.to_local_homeomorph.to_local_equiv.source → (⇑(self.to_local_homeomorph) p).fst = proj p
A structure extending local homeomorphisms, defining a local trivialization of a projection
proj : Z → B with fiber F, as a local homeomorphism between Z and B × F defined between two
sets of the form proj ⁻¹' base_set and base_set × F, acting trivially on the first coordinate.
Instances for trivialization
- trivialization.has_sizeof_inst
- trivialization.has_coe_to_fun
- trivialization.pretrivialization.has_coe
def
trivialization.to_pretrivialization
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj) :
pretrivialization F proj
Natural identification as a pretrivialization.
Equations
- e.to_pretrivialization = {to_local_equiv := e.to_local_homeomorph.to_local_equiv, open_target := _, base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Instances for trivialization.to_pretrivialization
@[protected, instance]
def
trivialization.has_coe_to_fun
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z] :
has_coe_to_fun (trivialization F proj) (λ (_x : trivialization F proj), Z → B × F)
Equations
- trivialization.has_coe_to_fun = {coe := λ (e : trivialization F proj), e.to_local_homeomorph.to_local_equiv.to_fun}
@[protected, instance]
def
trivialization.pretrivialization.has_coe
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z] :
has_coe (trivialization F proj) (pretrivialization F proj)
Equations
theorem
trivialization.to_pretrivialization_injective
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z] :
function.injective (λ (e : trivialization F proj), e.to_pretrivialization)
@[simp]
theorem
trivialization.coe_coe
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj) :
⇑(e.to_local_homeomorph) = ⇑e
@[simp]
theorem
trivialization.coe_fst
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
@[protected]
theorem
trivialization.eq_on
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj) :
set.eq_on (prod.fst ∘ ⇑e) proj e.to_local_homeomorph.to_local_equiv.source
theorem
trivialization.mem_source
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z} :
x ∈ e.to_local_homeomorph.to_local_equiv.source ↔ proj x ∈ e.base_set
theorem
trivialization.coe_fst'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : proj x ∈ e.base_set) :
theorem
trivialization.mk_proj_snd
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
theorem
trivialization.mk_proj_snd'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : proj x ∈ e.base_set) :
theorem
trivialization.source_inter_preimage_target_inter
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
(s : set (B × F)) :
@[simp]
theorem
trivialization.coe_mk
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : local_homeomorph Z (B × F))
(i : set B)
(j : is_open i)
(k : e.to_local_equiv.source = proj ⁻¹' i)
(l : e.to_local_equiv.target = i ×ˢ set.univ)
(m : ∀ (p : Z), p ∈ e.to_local_equiv.source → (⇑e p).fst = proj p)
(x : Z) :
⇑{to_local_homeomorph := e, base_set := i, open_base_set := j, source_eq := k, target_eq := l, proj_to_fun := m} x = ⇑e x
theorem
trivialization.mem_target
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : B × F} :
x ∈ e.to_local_homeomorph.to_local_equiv.target ↔ x.fst ∈ e.base_set
theorem
trivialization.map_target
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : B × F}
(hx : x ∈ e.to_local_homeomorph.to_local_equiv.target) :
theorem
trivialization.proj_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : B × F}
(hx : x ∈ e.to_local_homeomorph.to_local_equiv.target) :
proj (⇑(e.to_local_homeomorph.symm) x) = x.fst
theorem
trivialization.proj_symm_apply'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
{x : F}
(hx : b ∈ e.base_set) :
proj (⇑(e.to_local_homeomorph.symm) (b, x)) = b
theorem
trivialization.proj_surj_on_base_set
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
[nonempty F] :
theorem
trivialization.apply_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : B × F}
(hx : x ∈ e.to_local_homeomorph.to_local_equiv.target) :
⇑e (⇑(e.to_local_homeomorph.symm) x) = x
theorem
trivialization.apply_symm_apply'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
{x : F}
(hx : b ∈ e.base_set) :
⇑e (⇑(e.to_local_homeomorph.symm) (b, x)) = (b, x)
@[simp]
theorem
trivialization.symm_apply_mk_proj
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
theorem
trivialization.symm_trans_source_eq
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e e' : trivialization F proj) :
theorem
trivialization.symm_trans_target_eq
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e e' : trivialization F proj) :
theorem
trivialization.coe_fst_eventually_eq_proj
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
theorem
trivialization.coe_fst_eventually_eq_proj'
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : proj x ∈ e.base_set) :
theorem
trivialization.map_proj_nhds
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
filter.map proj (nhds x) = nhds (proj x)
theorem
trivialization.preimage_subset_source
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{s : set B}
(hb : s ⊆ e.base_set) :
proj ⁻¹' s ⊆ e.to_local_homeomorph.to_local_equiv.source
theorem
trivialization.image_preimage_eq_prod_univ
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{s : set B}
(hb : s ⊆ e.base_set) :
def
trivialization.preimage_homeomorph
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{s : set B}
(hb : s ⊆ e.base_set) :
The preimage of a subset of the base set is homeomorphic to the product with the fiber.
Equations
- e.preimage_homeomorph hb = (e.to_local_homeomorph.homeomorph_of_image_subset_source _ _).trans ((homeomorph.set.prod s set.univ).trans ((homeomorph.refl ↥s).prod_congr (homeomorph.set.univ F)))
@[simp]
theorem
trivialization.preimage_homeomorph_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{s : set B}
(hb : s ⊆ e.base_set)
(p : ↥(proj ⁻¹' s)) :
@[simp]
theorem
trivialization.preimage_homeomorph_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{s : set B}
(hb : s ⊆ e.base_set)
(p : ↥s × F) :
def
trivialization.source_homeomorph_base_set_prod
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj) :
↥(e.to_local_homeomorph.to_local_equiv.source) ≃ₜ ↥(e.base_set) × F
The source is homeomorphic to the product of the base set with the fiber.
Equations
@[simp]
theorem
trivialization.source_homeomorph_base_set_prod_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
(p : ↥(e.to_local_homeomorph.to_local_equiv.source)) :
@[simp]
theorem
trivialization.source_homeomorph_base_set_prod_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
(p : ↥(e.base_set) × F) :
def
trivialization.preimage_singleton_homeomorph
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
(hb : b ∈ e.base_set) :
Each fiber of a trivialization is homeomorphic to the specified fiber.
Equations
- e.preimage_singleton_homeomorph hb = (e.preimage_homeomorph _).trans (((homeomorph.homeomorph_of_unique ↥{b} punit).prod_congr (homeomorph.refl F)).trans (homeomorph.punit_prod F))
@[simp]
theorem
trivialization.preimage_singleton_homeomorph_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
(hb : b ∈ e.base_set)
(p : ↥(proj ⁻¹' {b})) :
@[simp]
theorem
trivialization.preimage_singleton_homeomorph_symm_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
(hb : b ∈ e.base_set)
(p : F) :
⇑((e.preimage_singleton_homeomorph hb).symm) p = ⟨⇑(e.to_local_homeomorph.symm) (b, p), _⟩
theorem
trivialization.continuous_at_proj
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{x : Z}
(ex : x ∈ e.to_local_homeomorph.to_local_equiv.source) :
continuous_at proj x
In the domain of a bundle trivialization, the projection is continuous
@[protected]
def
trivialization.comp_homeomorph
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{Z' : Type u_1}
[topological_space Z']
(h : Z' ≃ₜ Z) :
trivialization F (proj ∘ ⇑h)
Composition of a trivialization and a homeomorph.
Equations
- e.comp_homeomorph h = {to_local_homeomorph := h.to_local_homeomorph.trans e.to_local_homeomorph, base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
theorem
trivialization.continuous_at_of_comp_right
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
{X : Type u_1}
[topological_space X]
{f : Z → X}
{z : Z}
(e : trivialization F proj)
(he : proj z ∈ e.base_set)
(hf : continuous_at (f ∘ ⇑(e.to_local_homeomorph.to_local_equiv.symm)) (⇑e z)) :
continuous_at f z
Read off the continuity of a function f : Z → X at z : Z by transferring via a
trivialization of Z containing z.
theorem
trivialization.continuous_at_of_comp_left
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
{X : Type u_1}
[topological_space X]
{f : X → Z}
{x : X}
(e : trivialization F proj)
(hf_proj : continuous_at (proj ∘ f) x)
(he : proj (f x) ∈ e.base_set)
(hf : continuous_at (⇑e ∘ f) x) :
continuous_at f x
Read off the continuity of a function f : X → Z at x : X by transferring via a
trivialization of Z containing f x.
@[protected]
theorem
trivialization.continuous_on
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
(e' : trivialization F bundle.total_space.proj) :
theorem
trivialization.coe_mem_source
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
(e' : trivialization F bundle.total_space.proj)
{b : B}
{y : E b} :
↑y ∈ e'.to_local_homeomorph.to_local_equiv.source ↔ b ∈ e'.base_set
theorem
trivialization.open_target
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
(e' : trivialization F bundle.total_space.proj) :
@[simp]
theorem
trivialization.coe_coe_fst
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
(e' : trivialization F bundle.total_space.proj)
{b : B}
{y : E b}
(hb : b ∈ e'.base_set) :
theorem
trivialization.mk_mem_target
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
(e' : trivialization F bundle.total_space.proj)
{b : B}
{y : F} :
(b, y) ∈ e'.to_local_homeomorph.to_local_equiv.target ↔ b ∈ e'.base_set
theorem
trivialization.symm_apply_apply
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
(e' : trivialization F bundle.total_space.proj)
{x : bundle.total_space F E}
(hx : x ∈ e'.to_local_homeomorph.to_local_equiv.source) :
⇑(e'.to_local_homeomorph.symm) (⇑e' x) = x
@[simp]
theorem
trivialization.symm_coe_proj
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
{x : B}
{y : F}
(e : trivialization F bundle.total_space.proj)
(h : x ∈ e.base_set) :
(⇑(e.to_local_homeomorph.symm) (x, y)).proj = x
@[protected]
noncomputable
def
trivialization.symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
(b : B)
(y : F) :
E b
A fiberwise inverse to e'. The function F → E x that induces a local inverse
B × F → total_space F E of e' on e'.base_set. It is defined to be 0 outside
e'.base_set.
Equations
- e.symm b y = e.to_pretrivialization.symm b y
theorem
trivialization.symm_apply
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
theorem
trivialization.symm_apply_of_not_mem
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
{b : B}
(hb : b ∉ e.base_set)
(y : F) :
theorem
trivialization.mk_symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
theorem
trivialization.symm_proj_apply
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
(z : bundle.total_space F E)
(hz : z.proj ∈ e.base_set) :
theorem
trivialization.symm_apply_apply_mk
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : E b) :
theorem
trivialization.apply_mk_symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj)
{b : B}
(hb : b ∈ e.base_set)
(y : F) :
theorem
trivialization.continuous_on_symm
{B : Type u_2}
{F : Type u_3}
{E : B → Type u_4}
[topological_space B]
[topological_space F]
[topological_space (bundle.total_space F E)]
[Π (x : B), has_zero (E x)]
(e : trivialization F bundle.total_space.proj) :
def
trivialization.trans_fiber_homeomorph
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
{F' : Type u_1}
[topological_space F']
(e : trivialization F proj)
(h : F ≃ₜ F') :
trivialization F' proj
If e is a trivialization of proj : Z → B with fiber F and h is a homeomorphism
F ≃ₜ F', then e.trans_fiber_homeomorph h is the trivialization of proj with the fiber F'
that sends p : Z to ((e p).1, h (e p).2).
Equations
- e.trans_fiber_homeomorph h = {to_local_homeomorph := e.to_local_homeomorph.trans_homeomorph ((homeomorph.refl B).prod_congr h), base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
@[simp]
theorem
trivialization.trans_fiber_homeomorph_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
{F' : Type u_1}
[topological_space F']
(e : trivialization F proj)
(h : F ≃ₜ F')
(x : Z) :
def
trivialization.coord_change
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ : trivialization F proj)
(b : B)
(x : F) :
F
Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
trivialization.coord_change_homeomorph for a version bundled as F ≃ₜ F.
Equations
- e₁.coord_change e₂ b x = (⇑e₂ (⇑(e₁.to_local_homeomorph.symm) (b, x))).snd
theorem
trivialization.mk_coord_change
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ : trivialization F proj)
{b : B}
(h₁ : b ∈ e₁.base_set)
(h₂ : b ∈ e₂.base_set)
(x : F) :
(b, e₁.coord_change e₂ b x) = ⇑e₂ (⇑(e₁.to_local_homeomorph.symm) (b, x))
theorem
trivialization.coord_change_apply_snd
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ : trivialization F proj)
{p : Z}
(h : proj p ∈ e₁.base_set) :
theorem
trivialization.coord_change_same_apply
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
(h : b ∈ e.base_set)
(x : F) :
e.coord_change e b x = x
theorem
trivialization.coord_change_same
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
{b : B}
(h : b ∈ e.base_set) :
e.coord_change e b = id
theorem
trivialization.coord_change_coord_change
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ e₃ : trivialization F proj)
{b : B}
(h₁ : b ∈ e₁.base_set)
(h₂ : b ∈ e₂.base_set)
(x : F) :
e₂.coord_change e₃ b (e₁.coord_change e₂ b x) = e₁.coord_change e₃ b x
theorem
trivialization.continuous_coord_change
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ : trivialization F proj)
{b : B}
(h₁ : b ∈ e₁.base_set)
(h₂ : b ∈ e₂.base_set) :
continuous (e₁.coord_change e₂ b)
@[protected]
def
trivialization.coord_change_homeomorph
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ : trivialization F proj)
{b : B}
(h₁ : b ∈ e₁.base_set)
(h₂ : b ∈ e₂.base_set) :
F ≃ₜ F
Coordinate transformation in the fiber induced by a pair of bundle trivializations, as a homeomorphism.
Equations
- e₁.coord_change_homeomorph e₂ h₁ h₂ = {to_equiv := {to_fun := e₁.coord_change e₂ b, inv_fun := e₂.coord_change e₁ b, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
trivialization.coord_change_homeomorph_coe
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e₁ e₂ : trivialization F proj)
{b : B}
(h₁ : b ∈ e₁.base_set)
(h₂ : b ∈ e₂.base_set) :
⇑(e₁.coord_change_homeomorph e₂ h₁ h₂) = e₁.coord_change e₂ b
theorem
trivialization.is_image_preimage_prod
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
(s : set B) :
e.to_local_homeomorph.is_image (proj ⁻¹' s) (s ×ˢ set.univ)
@[protected]
def
trivialization.restr_open
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
(s : set B)
(hs : is_open s) :
trivialization F proj
Restrict a trivialization to an open set in the base. `
Equations
- e.restr_open s hs = {to_local_homeomorph := (_.restr _).symm, base_set := e.base_set ∩ s, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
theorem
trivialization.frontier_preimage
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e : trivialization F proj)
(s : set B) :
noncomputable
def
trivialization.piecewise
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e e' : trivialization F proj)
(s : set B)
(Hs : e.base_set ∩ frontier s = e'.base_set ∩ frontier s)
(Heq : set.eq_on ⇑e ⇑e' (proj ⁻¹' (e.base_set ∩ frontier s))) :
trivialization F proj
Given two bundle trivializations e, e' of proj : Z → B and a set s : set B such that
the base sets of e and e' intersect frontier s on the same set and e p = e' p whenever
proj p ∈ e.base_set ∩ frontier s, e.piecewise e' s Hs Heq is the bundle trivialization over
set.ite s e.base_set e'.base_set that is equal to e on proj ⁻¹ s and is equal to e'
otherwise.
Equations
- e.piecewise e' s Hs Heq = {to_local_homeomorph := e.to_local_homeomorph.piecewise e'.to_local_homeomorph (proj ⁻¹' s) (s ×ˢ set.univ) _ _ _ _, base_set := s.ite e.base_set e'.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
noncomputable
def
trivialization.piecewise_le_of_eq
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
[linear_order B]
[order_topology B]
(e e' : trivialization F proj)
(a : B)
(He : a ∈ e.base_set)
(He' : a ∈ e'.base_set)
(Heq : ∀ (p : Z), proj p = a → ⇑e p = ⇑e' p) :
trivialization F proj
Given two bundle trivializations e, e' of a topological fiber bundle proj : Z → B
over a linearly ordered base B and a point a ∈ e.base_set ∩ e'.base_set such that
e equals e' on proj ⁻¹' {a}, e.piecewise_le_of_eq e' a He He' Heq is the bundle
trivialization over set.ite (Iic a) e.base_set e'.base_set that is equal to e on points p
such that proj p ≤ a and is equal to e' otherwise.
Equations
- e.piecewise_le_of_eq e' a He He' Heq = e.piecewise e' (set.Iic a) _ _
noncomputable
def
trivialization.piecewise_le
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
[linear_order B]
[order_topology B]
(e e' : trivialization F proj)
(a : B)
(He : a ∈ e.base_set)
(He' : a ∈ e'.base_set) :
trivialization F proj
Given two bundle trivializations e, e' of a topological fiber bundle proj : Z → B over a
linearly ordered base B and a point a ∈ e.base_set ∩ e'.base_set, e.piecewise_le e' a He He'
is the bundle trivialization over set.ite (Iic a) e.base_set e'.base_set that is equal to e on
points p such that proj p ≤ a and is equal to ((e' p).1, h (e' p).2) otherwise, where
h =e'.coord_change_homeomorph e _ _is the homeomorphism of the fiber such thath (e' p).2 = (e p).2whenevere p = a`.
Equations
- e.piecewise_le e' a He He' = e.piecewise_le_of_eq (e'.trans_fiber_homeomorph (e'.coord_change_homeomorph e He' He)) a He He' _
noncomputable
def
trivialization.disjoint_union
{B : Type u_2}
{F : Type u_3}
{Z : Type u_5}
[topological_space B]
[topological_space F]
{proj : Z → B}
[topological_space Z]
(e e' : trivialization F proj)
(H : disjoint e.base_set e'.base_set) :
trivialization F proj
Given two bundle trivializations e, e' over disjoint sets, e.disjoint_union e' H is the
bundle trivialization over the union of the base sets that agrees with e and e' over their
base sets.
Equations
- e.disjoint_union e' H = {to_local_homeomorph := e.to_local_homeomorph.disjoint_union e'.to_local_homeomorph _ _, base_set := e.base_set ∪ e'.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}