mathlib documentation

topology.fiber_bundle.trivialization

Trivializations #

Main definitions #

Basic definitions #

Operations on bundles #

We provide the following operations on trivializations.

Implementation notes #

Previously, in mathlib, there was a structure topological_vector_bundle.trivialization which extended another structure topological_fibre_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 fibre 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 fibre 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)

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
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) :
@[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
@[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) :
@[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) :
(e x).fst = proj x
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) :
(e x).fst = proj x
@[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) :
(proj x, (e x).snd) = e x
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) :
(proj x, (e x).snd) = e x
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) :

Composition of inverse and coercion from the subtype of the target.

Equations
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.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) :
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) :
@[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) :
(e.to_local_equiv.symm) (proj x, (e x).snd) = x
@[simp]
@[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) :
(e' y).fst = b
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)).fst = 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 E of e on e.base_set. It is defined to be 0 outside e.base_set.

Equations
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) :
e.symm b y = cast _ ((e.to_local_equiv.symm) (b, y)).snd
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) :
e.symm b y = 0
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) :
e.symm b = 0
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 E) (hz : z.proj e.base_set) :
e.symm z.proj (e z).snd = z.snd
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) :
e (bundle.total_space_mk b (e.symm b y)) = (b, y)
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) :
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)

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
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) :

Natural identification as a pretrivialization.

Equations
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
@[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) :
@[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) :
(e x).fst = proj x
@[protected]
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} :
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) :
(e x).fst = proj x
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) :
(proj x, (e x).snd) = e x
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) :
(proj x, (e x).snd) = e x
@[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) :
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} :
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) :
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.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) :
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) :
(e.to_local_homeomorph.symm) (proj x, (e x).snd) = x
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) :
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) :
e '' (proj ⁻¹' s) = s ×ˢ set.univ
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) :
(proj ⁻¹' s) ≃ₜ s × F

The preimage of a subset of the base set is homeomorphic to the product with the fiber.

Equations
@[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)) :
(e.preimage_homeomorph hb) p = (proj p, _⟩, (e p).snd)
@[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) :

The source is homeomorphic to the product of the base set with the fiber.

Equations
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) :
(proj ⁻¹' {b}) ≃ₜ F

Each fiber of a trivialization is homeomorphic to the specified fiber.

Equations
@[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) :
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) :

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) :

Composition of a trivialization and a homeomorph.

Equations
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)) :

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) :

Read off the continuity of a function f : X → Z at x : X by transferring via a trivialization of Z containing f x.

@[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 E)] (e' : trivialization F bundle.total_space.proj) {b : B} {y : E b} (hb : b e'.base_set) :
(e' y).fst = b
@[simp]
@[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 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 E of e' on e'.base_set. It is defined to be 0 outside e'.base_set.

Equations
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 E)] [Π (x : B), has_zero (E x)] (e : trivialization F bundle.total_space.proj) {b : B} (hb : b e.base_set) (y : F) :
e.symm b y = cast _ ((e.to_local_homeomorph.symm) (b, y)).snd
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 E)] [Π (x : B), has_zero (E x)] (e : trivialization F bundle.total_space.proj) {b : B} (hb : b e.base_set) (y : F) :
e.symm b y = 0
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 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_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 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 E)] [Π (x : B), has_zero (E x)] (e : trivialization F bundle.total_space.proj) {b : B} (hb : b e.base_set) (y : F) :
e (bundle.total_space_mk b (e.symm b y)) = (b, y)
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') :

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
@[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) :
(e.trans_fiber_homeomorph h) x = ((e x).fst, h (e x).snd)
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
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) :
e₁.coord_change e₂ (proj p) (e₁ p).snd = (e₂ p).snd
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) :
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
@[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) :
@[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) :

Restrict a trivialization to an open set in the base. `

Equations
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))) :

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
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) :

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
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) :

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
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) :

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