Trivializations

Main definitions

Basic definitions

• Bundle.Trivialization F p : structure extending open partial homeomorphisms, defining a local trivialization of a topological space Z with projection p and fiber F.

• Bundle.Pretrivialization F proj : trivialization as a partial 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.

• Bundle.Trivialization.compHomeomorph: given a local trivialization e of a fiber bundle p : Z → B and a homeomorphism h : Z' ≃ₜ Z, returns a local trivialization of the fiber bundle p ∘ 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 https://github.com/leanprover-community/mathlib3/pull/17359, we have changed this to a single structure Bundle.Trivialization, together with a mixin class Bundle.Trivialization.IsLinear.

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.

structure Bundle.Pretrivialization {B : Type u_1} (F : Type u_2) {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] (proj : Z → B) extends PartialEquiv Z (B × F) : Type (max (max u_1 u_2) u_4)

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.

• toFun : Z → B × F
• invFun : B × F → Z
• source : Set Z
• target : Set (B × F)
• map_source' ⦃x : Z⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : B × F⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : Z⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : B × F⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• open_target : IsOpen self.target
• baseSet : Set B

  The domain of the local trivialisation (i.e., a subset of the bundle Z's base): outside of it, the pretrivialisation returns a junk value

• open_baseSet : IsOpen self.baseSet
• source_eq : self.source = proj ⁻¹' self.baseSet
• target_eq : self.target = self.baseSet ×ˢ Set.univ
• proj_toFun (p : Z) : p ∈ self.source → (↑self.toPartialEquiv p).1 = proj p

def Bundle.Pretrivialization.toFun' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : Z → B × F

Coercion of a pretrivialization to a function. We don't use e.toFun in the CoeFun instance because it is actually e.toPartialEquiv.toFun, so simp will apply lemmas about toPartialEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

Equations

• ↑e = ↑e.toPartialEquiv

@[implicit_reducible]

instance Bundle.Pretrivialization.instCoeFunForallProd {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} : CoeFun (Pretrivialization F proj) fun (x : Pretrivialization F proj) => Z → B × F

Equations

• Bundle.Pretrivialization.instCoeFunForallProd = { coe := Bundle.Pretrivialization.toFun' }

theorem Bundle.Pretrivialization.ext' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e e' : Pretrivialization F proj) (h₁ : e.toPartialEquiv = e'.toPartialEquiv) (h₂ : e.baseSet = e'.baseSet) : e = e'

theorem Bundle.Pretrivialization.ext'_iff {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {e e' : Pretrivialization F proj} : e = e' ↔ e.toPartialEquiv = e'.toPartialEquiv ∧ e.baseSet = e'.baseSet

theorem Bundle.Pretrivialization.ext {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {e e' : Pretrivialization F proj} (h₁ : ∀ (x : Z), ↑e x = ↑e' x) (h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x) (h₃ : e.baseSet = e'.baseSet) : e = e'

theorem Bundle.Pretrivialization.toPartialEquiv_injective {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [Nonempty F] : Function.Injective toPartialEquiv

If the fiber is nonempty, then the projection also is.

@[simp]

theorem Bundle.Pretrivialization.coe_coe {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : ↑e.toPartialEquiv = ↑e

@[simp]

theorem Bundle.Pretrivialization.coe_fst {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : x ∈ e.source) : (↑e x).1 = proj x

theorem Bundle.Pretrivialization.mem_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} : x ∈ e.source ↔ proj x ∈ e.baseSet

theorem Bundle.Pretrivialization.coe_fst' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (↑e x).1 = proj x

theorem Bundle.Pretrivialization.eqOn {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : Set.EqOn (Prod.fst ∘ ↑e) proj e.source

@[simp]

theorem Bundle.Pretrivialization.mk_proj_snd {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : x ∈ e.source) : (proj x, (↑e x).2) = ↑e x

@[simp]

theorem Bundle.Pretrivialization.mk_proj_snd' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (proj x, (↑e x).2) = ↑e x

def Bundle.Pretrivialization.setSymm {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : ↑e.target → Z

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

Equations

• e.setSymm = e.target.restrict ↑e.symm

theorem Bundle.Pretrivialization.mem_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.baseSet

theorem Bundle.Pretrivialization.proj_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : B × F} (hx : x ∈ e.target) : proj (↑e.symm x) = x.1

theorem Bundle.Pretrivialization.proj_symm_apply' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : proj (↑e.symm (b, x)) = b

theorem Bundle.Pretrivialization.proj_surjOn_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) [Nonempty F] : Set.SurjOn proj e.source e.baseSet

@[simp]

theorem Bundle.Pretrivialization.apply_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e (↑e.symm x) = x

@[simp]

theorem Bundle.Pretrivialization.apply_symm_apply' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : ↑e (↑e.symm (b, x)) = (b, x)

@[simp]

theorem Bundle.Pretrivialization.symm_apply_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (hx : x ∈ e.source) : ↑e.symm (↑e x) = x

theorem Bundle.Pretrivialization.symm_apply_mk_proj {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : x ∈ e.source) : ↑e.symm (proj x, (↑e x).2) = x

@[simp]

theorem Bundle.Pretrivialization.preimage_symm_proj_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : ↑e.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target

@[simp]

theorem Bundle.Pretrivialization.preimage_symm_proj_inter {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) : ↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ Set.univ = (s ∩ e.baseSet) ×ˢ Set.univ

theorem Bundle.Pretrivialization.target_inter_preimage_symm_source_eq {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e f : Pretrivialization F proj) : f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ

theorem Bundle.Pretrivialization.trans_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e f : Pretrivialization F proj) : (f.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ

theorem Bundle.Pretrivialization.symm_trans_symm {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e e' : Pretrivialization F proj) : (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv

theorem Bundle.Pretrivialization.symm_trans_source_eq {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e e' : Pretrivialization F proj) : (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

theorem Bundle.Pretrivialization.symm_trans_target_eq {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e e' : Pretrivialization F proj) : (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

@[simp]

theorem Bundle.Pretrivialization.coe_mem_source {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] (e' : Pretrivialization F TotalSpace.proj) {b : B} {y : E b} : { proj := b, snd := y } ∈ e'.source ↔ b ∈ e'.baseSet

theorem Bundle.Pretrivialization.coe_coe_fst {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] (e' : Pretrivialization F TotalSpace.proj) {b : B} {y : E b} (hb : b ∈ e'.baseSet) : (↑e' { proj := b, snd := y }).1 = b

theorem Bundle.Pretrivialization.mk_mem_target {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] (e' : Pretrivialization F TotalSpace.proj) {x : B} {y : F} : (x, y) ∈ e'.target ↔ x ∈ e'.baseSet

@[simp]

theorem Bundle.Pretrivialization.symm_coe_proj {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] {x : B} {y : F} (e' : Pretrivialization F TotalSpace.proj) (h : x ∈ e'.baseSet) : (↑e'.symm (x, y)).proj = x

noncomputable def Bundle.Pretrivialization.symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.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 → TotalSpace F E of e on e.baseSet. It is defined to be 0 outside e.baseSet.

Equations

• e.symm b y = if hb : b ∈ e.baseSet then cast ⋯ (↑e.symm (b, y)).snd else 0

theorem Bundle.Pretrivialization.symm_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : e.symm b y = cast ⋯ (↑e.symm (b, y)).snd

theorem Bundle.Pretrivialization.symm_apply_of_notMem {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) {b : B} (hb : b ∉ e.baseSet) (y : F) : e.symm b y = 0

theorem Bundle.Pretrivialization.coe_symm_of_notMem {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) {b : B} (hb : b ∉ e.baseSet) : e.symm b = 0

theorem Bundle.Pretrivialization.mk_symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : { proj := b, snd := e.symm b y } = ↑e.symm (b, y)

@[simp]

theorem Bundle.Pretrivialization.symm_proj_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) (z : TotalSpace F E) (hz : z.proj ∈ e.baseSet) : e.symm z.proj (↑e z).2 = z.snd

@[simp]

theorem Bundle.Pretrivialization.symm_apply_apply_mk {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : E b) : e.symm b (↑e { proj := b, snd := y }).2 = y

@[simp]

theorem Bundle.Pretrivialization.apply_mk_symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : ↑e { proj := b, snd := e.symm b y } = (b, y)

noncomputable def Bundle.Pretrivialization.restrictPreimage' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : Pretrivialization F (s.restrictPreimage proj)

The restriction of a pretrivialization to a subset of the base.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage'_toFun {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] (z : ↑(proj ⁻¹' s)) : ↑(e.restrictPreimage' s).toPartialEquiv z = (⟨proj ↑z, ⋯⟩, (↑e ↑z).2)

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage'_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : (e.restrictPreimage' s).baseSet = Subtype.val ⁻¹' e.baseSet

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage'_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : (e.restrictPreimage' s).source = Subtype.val ⁻¹' e.source

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage'_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : (e.restrictPreimage' s).target = Prod.map Subtype.val id ⁻¹' e.target

noncomputable def Bundle.Pretrivialization.restrictPreimage {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : Pretrivialization F (s.restrictPreimage proj)

The restriction of a pretrivialization to a set with nonempty intersection with the base set.

Equations

• e.restrictPreimage hs = e.restrictPreimage' s

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : (e.restrictPreimage hs).source = Subtype.val ⁻¹' e.source

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : (e.restrictPreimage hs).baseSet = Subtype.val ⁻¹' e.baseSet

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : (e.restrictPreimage hs).target = Prod.map Subtype.val id ⁻¹' e.target

@[simp]

theorem Bundle.Pretrivialization.restrictPreimage_toFun {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) (z : ↑(proj ⁻¹' s)) : ↑(e.restrictPreimage hs).toPartialEquiv z = (⟨proj ↑z, ⋯⟩, (↑e ↑z).2)

noncomputable def Bundle.Pretrivialization.domExtend {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {s : Set B} (e : Pretrivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : Pretrivialization F proj

Extend the total space of a pretrivialization from the preimage of a set to the whole space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Pretrivialization.domExtend_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {s : Set B} (e : Pretrivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : e.domExtend.source = Subtype.val '' e.source

@[simp]

theorem Bundle.Pretrivialization.domExtend_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {s : Set B} (e : Pretrivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : e.domExtend.target = e.target

@[simp]

theorem Bundle.Pretrivialization.domExtend_invFun {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {s : Set B} (e : Pretrivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] (x : B × F) : e.domExtend.invFun x = ↑(e.invFun x)

@[simp]

theorem Bundle.Pretrivialization.domExtend_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {s : Set B} (e : Pretrivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : e.domExtend.baseSet = e.baseSet

noncomputable def Bundle.Pretrivialization.codExtend' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [Nonempty (B → F → Z)] : Pretrivialization F (Subtype.val ∘ proj)

Extend the base of a pretrivialization from a set to the whole space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Pretrivialization.codExtend'_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [Nonempty (B → F → Z)] : (codExtend' hs e).source = e.source

@[simp]

theorem Bundle.Pretrivialization.codExtend'_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [Nonempty (B → F → Z)] : (codExtend' hs e).target = Prod.map Subtype.val id '' e.target

@[simp]

theorem Bundle.Pretrivialization.codExtend'_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [Nonempty (B → F → Z)] : (codExtend' hs e).baseSet = Subtype.val '' e.baseSet

@[simp]

theorem Bundle.Pretrivialization.codExtend'_toFun {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [Nonempty (B → F → Z)] (z : Z) : ↑(codExtend' hs e).toPartialEquiv z = (↑(↑e z).1, (↑e z).2)

noncomputable def Bundle.Pretrivialization.codExtend {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Pretrivialization F proj) : Pretrivialization F (Subtype.val ∘ proj)

Extend the base of a pretrivialization from a nonempty set to the whole space.

Equations

• Bundle.Pretrivialization.codExtend hs nonempty e = Bundle.Pretrivialization.codExtend' hs e

@[simp]

theorem Bundle.Pretrivialization.codExtend_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Pretrivialization F proj) : (codExtend hs nonempty e).baseSet = Subtype.val '' e.baseSet

@[simp]

theorem Bundle.Pretrivialization.codExtend_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Pretrivialization F proj) : (codExtend hs nonempty e).source = e.source

@[simp]

theorem Bundle.Pretrivialization.codExtend_toFun {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Pretrivialization F proj) (z : Z) : ↑(codExtend hs nonempty e).toPartialEquiv z = (↑(↑e z).1, (↑e z).2)

@[simp]

theorem Bundle.Pretrivialization.codExtend_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Pretrivialization F proj) : (codExtend hs nonempty e).target = Prod.map Subtype.val id '' e.target

structure Bundle.Trivialization {B : Type u_1} (F : Type u_2) {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] (proj : Z → B) extends OpenPartialHomeomorph Z (B × F) : Type (max (max u_1 u_2) u_4)

A structure extending open partial homeomorphisms, defining a local trivialization of a projection proj : Z → B with fiber F, as an open partial homeomorphism between Z and B × F defined between two sets of the form proj ⁻¹' baseSet and baseSet × F, acting trivially on the first coordinate.

• toFun : Z → B × F
• invFun : B × F → Z
• source : Set Z
• target : Set (B × F)
• map_source' ⦃x : Z⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : B × F⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : Z⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : B × F⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• open_source : IsOpen self.source
• open_target : IsOpen self.target
• continuousOn_toFun : ContinuousOn (↑self.toPartialEquiv) self.source
• continuousOn_invFun : ContinuousOn self.invFun self.target
• baseSet : Set B

  The domain of the local trivialisation (i.e., a subset of the bundle Z's base): outside of it, the pretrivialisation returns a junk value

• open_baseSet : IsOpen self.baseSet
• source_eq : self.source = proj ⁻¹' self.baseSet
• target_eq : self.target = self.baseSet ×ˢ Set.univ
• proj_toFun (p : Z) : p ∈ self.source → (↑self.toOpenPartialHomeomorph p).1 = proj p

theorem Bundle.Trivialization.ext' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e e' : Trivialization F proj) (h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph) (h₂ : e.baseSet = e'.baseSet) : e = e'

theorem Bundle.Trivialization.ext'_iff {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {e e' : Trivialization F proj} : e = e' ↔ e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph ∧ e.baseSet = e'.baseSet

def Bundle.Trivialization.toFun' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : Z → B × F

Coercion of a trivialization to a function. We don't use e.toFun in the CoeFun instance because it is actually e.toPartialEquiv.toFun, so simp will apply lemmas about toPartialEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

Equations

• ↑e = ↑e.toPartialEquiv

def Bundle.Trivialization.toPretrivialization {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : Pretrivialization F proj

Natural identification as a Pretrivialization.

Equations

• e.toPretrivialization = { toPartialEquiv := e.toPartialEquiv, open_target := ⋯, baseSet := e.baseSet, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }

@[implicit_reducible]

instance Bundle.Trivialization.instCoeFunForallProd {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] : CoeFun (Trivialization F proj) fun (x : Trivialization F proj) => Z → B × F

Equations

• Bundle.Trivialization.instCoeFunForallProd = { coe := Bundle.Trivialization.toFun' }

@[implicit_reducible]

instance Bundle.Trivialization.instCoePretrivialization {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] : Coe (Trivialization F proj) (Pretrivialization F proj)

Equations

• Bundle.Trivialization.instCoePretrivialization = { coe := Bundle.Trivialization.toPretrivialization }

def Bundle.Trivialization.Simps.apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] (proj : Z → B) (e : Trivialization F proj) : Z → B × F

See Note [custom simps projection]

Equations

• Bundle.Trivialization.Simps.apply proj e = ↑e

noncomputable def Bundle.Trivialization.Simps.symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] (proj : Z → B) (e : Trivialization F proj) : B × F → Z

See Note [custom simps projection]

Equations

• Bundle.Trivialization.Simps.symm_apply proj e = ↑e.symm

theorem Bundle.Trivialization.toPretrivialization_injective {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] : Function.Injective fun (e : Trivialization F proj) => e.toPretrivialization

@[simp]

theorem Bundle.Trivialization.coe_coe {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : ↑e.toOpenPartialHomeomorph = ↑e

@[simp]

theorem Bundle.Trivialization.coe_fst {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : (↑e x).1 = proj x

theorem Bundle.Trivialization.eqOn {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : Set.EqOn (Prod.fst ∘ ↑e) proj e.source

theorem Bundle.Trivialization.mem_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} : x ∈ e.source ↔ proj x ∈ e.baseSet

@[simp]

theorem Bundle.Trivialization.coe_fst' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (↑e x).1 = proj x

theorem Bundle.Trivialization.mk_proj_snd {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : (proj x, (↑e x).2) = ↑e x

theorem Bundle.Trivialization.mk_proj_snd' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (proj x, (↑e x).2) = ↑e x

theorem Bundle.Trivialization.source_inter_preimage_target_inter {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set (B × F)) : e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s

@[simp]

theorem Bundle.Trivialization.coe_mk {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : OpenPartialHomeomorph Z (B × F)) (i : Set B) (j : IsOpen i) (k : e.source = proj ⁻¹' i) (l : e.target = i ×ˢ Set.univ) (m : ∀ p ∈ e.source, (↑e p).1 = proj p) (x : Z) : ↑{ toOpenPartialHomeomorph := e, baseSet := i, open_baseSet := j, source_eq := k, target_eq := l, proj_toFun := m } x = ↑e x

theorem Bundle.Trivialization.mem_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.baseSet

theorem Bundle.Trivialization.map_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e.symm x ∈ e.source

theorem Bundle.Trivialization.proj_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : proj (↑e.symm x) = x.1

theorem Bundle.Trivialization.proj_symm_apply' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : proj (↑e.symm (b, x)) = b

theorem Bundle.Trivialization.proj_surjOn_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) [Nonempty F] : Set.SurjOn proj e.source e.baseSet

@[simp]

theorem Bundle.Trivialization.apply_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e (↑e.symm x) = x

@[simp]

theorem Bundle.Trivialization.apply_symm_apply' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : ↑e (↑e.symm (b, x)) = (b, x)

@[simp]

theorem Bundle.Trivialization.symm_apply_mk_proj {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : ↑e.symm (proj x, (↑e x).2) = x

theorem Bundle.Trivialization.symm_trans_source_eq {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e e' : Trivialization F proj) : (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

theorem Bundle.Trivialization.symm_trans_target_eq {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e e' : Trivialization F proj) : (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

theorem Bundle.Trivialization.coe_fst_eventuallyEq_proj {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : Prod.fst ∘ ↑e =ᶠ[nhds x] proj

theorem Bundle.Trivialization.coe_fst_eventuallyEq_proj' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : Prod.fst ∘ ↑e =ᶠ[nhds x] proj

theorem Bundle.Trivialization.map_proj_nhds {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : Filter.map proj (nhds x) = nhds (proj x)

theorem Bundle.Trivialization.preimage_subset_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : proj ⁻¹' s ⊆ e.source

theorem Bundle.Trivialization.image_preimage_eq_prod_univ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : ↑e '' (proj ⁻¹' s) = s ×ˢ Set.univ

theorem Bundle.Trivialization.tendsto_nhds_iff {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {α : Type u_5} {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) : Filter.Tendsto f l (nhds z) ↔ Filter.Tendsto (proj ∘ f) l (nhds (proj z)) ∧ Filter.Tendsto (fun (x : α) => (↑e (f x)).2) l (nhds (↑e z).2)

theorem Bundle.Trivialization.nhds_eq_inf_comap {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {z : Z} (hz : z ∈ e.source) : nhds z = Filter.comap proj (nhds (proj z)) ⊓ Filter.comap (Prod.snd ∘ ↑e) (nhds (↑e z).2)

def Bundle.Trivialization.preimageHomeomorph {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : ↑(proj ⁻¹' s) ≃ₜ ↑s × F

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

Equations

• e.preimageHomeomorph hb = (e.homeomorphOfImageSubsetSource ⋯ ⋯).trans ((Homeomorph.Set.prod s Set.univ).trans ((Homeomorph.refl ↑s).prodCongr (Homeomorph.Set.univ F)))

@[simp]

theorem Bundle.Trivialization.preimageHomeomorph_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑(proj ⁻¹' s)) : (e.preimageHomeomorph hb) p = (⟨proj ↑p, ⋯⟩, (↑e ↑p).2)

def Bundle.Trivialization.preimageHomeomorph_symm_apply.aux {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : ↑s × F ≃ₜ ↑(proj ⁻¹' s)

Auxiliary definition to avoid looping in dsimp with Bundle.Trivialization.preimageHomeomorph_symm_apply.

Equations

• Bundle.Trivialization.preimageHomeomorph_symm_apply.aux e hb = (e.preimageHomeomorph hb).symm

@[simp]

theorem Bundle.Trivialization.preimageHomeomorph_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑s × F) : (e.preimageHomeomorph hb).symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩

def Bundle.Trivialization.sourceHomeomorphBaseSetProd {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : ↑e.source ≃ₜ ↑e.baseSet × F

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

Equations

• e.sourceHomeomorphBaseSetProd = (Homeomorph.setCongr ⋯).trans (e.preimageHomeomorph ⋯)

@[simp]

theorem Bundle.Trivialization.sourceHomeomorphBaseSetProd_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (p : ↑e.source) : e.sourceHomeomorphBaseSetProd p = (⟨proj ↑p, ⋯⟩, (↑e ↑p).2)

def Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply.aux {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : ↑e.baseSet × F ≃ₜ ↑e.source

Auxiliary definition to avoid looping in dsimp with Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply.

Equations

• Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply.aux e = e.sourceHomeomorphBaseSetProd.symm

@[simp]

theorem Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (p : ↑e.baseSet × F) : e.sourceHomeomorphBaseSetProd.symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩

def Bundle.Trivialization.preimageSingletonHomeomorph {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) : ↑(proj ⁻¹' {b}) ≃ₜ F

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

Equations

• e.preimageSingletonHomeomorph hb = (e.preimageHomeomorph ⋯).trans (((Homeomorph.homeomorphOfUnique (↑{b}) PUnit.{1}).prodCongr (Homeomorph.refl F)).trans (Homeomorph.punitProd F))

@[simp]

theorem Bundle.Trivialization.preimageSingletonHomeomorph_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : ↑(proj ⁻¹' {b})) : (e.preimageSingletonHomeomorph hb) p = (↑e ↑p).2

@[simp]

theorem Bundle.Trivialization.preimageSingletonHomeomorph_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : F) : (e.preimageSingletonHomeomorph hb).symm p = ⟨↑e.symm (b, p), ⋯⟩

theorem Bundle.Trivialization.continuousAt_proj {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : ContinuousAt proj x

In the domain of a bundle trivialization, the projection is continuous

theorem Bundle.Trivialization.continuousOn_proj {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : ContinuousOn proj e.source

def Bundle.Trivialization.compHomeomorph {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {Z' : Type u_5} [TopologicalSpace Z'] (h : Z' ≃ₜ Z) : Trivialization F (proj ∘ ⇑h)

Pre-composition of a Bundle.Trivialization and a Homeomorph.

Equations

• One or more equations did not get rendered due to their size.

def Bundle.Trivialization.homeomorphComp {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {B' : Type u_5} [TopologicalSpace B'] (h : B ≃ₜ B') : Trivialization F (⇑h ∘ proj)

Post-composition of a Bundle.Trivialization and a Homeomorph.

Equations

• One or more equations did not get rendered due to their size.

theorem Bundle.Trivialization.continuousAt_of_comp_right {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {X : Type u_5} [TopologicalSpace X] {f : Z → X} {z : Z} (e : Trivialization F proj) (he : proj z ∈ e.baseSet) (hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)) : ContinuousAt 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 Bundle.Trivialization.continuousAt_of_comp_left {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {X : Type u_5} [TopologicalSpace X] {f : X → Z} {x : X} (e : Trivialization F proj) (hf_proj : ContinuousAt (proj ∘ f) x) (he : proj (f x) ∈ e.baseSet) (hf : ContinuousAt (↑e ∘ f) x) : ContinuousAt 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.

theorem Bundle.Trivialization.continuousOn {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] (e' : Trivialization F TotalSpace.proj) : ContinuousOn (↑e') e'.source

theorem Bundle.Trivialization.coe_mem_source {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] (e' : Trivialization F TotalSpace.proj) {b : B} {y : E b} : { proj := b, snd := y } ∈ e'.source ↔ b ∈ e'.baseSet

theorem Bundle.Trivialization.coe_coe_fst {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] (e' : Trivialization F TotalSpace.proj) {b : B} {y : E b} (hb : b ∈ e'.baseSet) : (↑e' { proj := b, snd := y }).1 = b

theorem Bundle.Trivialization.mk_mem_target {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] (e' : Trivialization F TotalSpace.proj) {b : B} {y : F} : (b, y) ∈ e'.target ↔ b ∈ e'.baseSet

@[simp]

theorem Bundle.Trivialization.symm_apply_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] (e' : Trivialization F TotalSpace.proj) {x : TotalSpace F E} (hx : x ∈ e'.source) : ↑e'.symm (↑e' x) = x

@[simp]

theorem Bundle.Trivialization.symm_coe_proj {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] {x : B} {y : F} (e : Trivialization F TotalSpace.proj) (h : x ∈ e.baseSet) : (↑e.symm (x, y)).proj = x

noncomputable def Bundle.Trivialization.symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) (b : B) (y : F) : E b

A fiberwise inverse to e'. The function F → E x that induces a local inverse B × F → TotalSpace F E of e' on e'.baseSet. It is defined to be 0 outside e'.baseSet.

Equations

• e.symm b y = e.toPretrivialization.symm b y

theorem Bundle.Trivialization.symm_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : e.symm b y = cast ⋯ (↑e.symm (b, y)).snd

theorem Bundle.Trivialization.symm_apply_of_notMem {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) {b : B} (hb : b ∉ e.baseSet) (y : F) : e.symm b y = 0

theorem Bundle.Trivialization.mk_symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : { proj := b, snd := e.symm b y } = ↑e.symm (b, y)

@[simp]

theorem Bundle.Trivialization.symm_proj_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) (z : TotalSpace F E) (hz : z.proj ∈ e.baseSet) : e.symm z.proj (↑e z).2 = z.snd

@[simp]

theorem Bundle.Trivialization.symm_apply_apply_mk {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : E b) : e.symm b (↑e { proj := b, snd := y }).2 = y

@[simp]

theorem Bundle.Trivialization.apply_mk_symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : ↑e { proj := b, snd := e.symm b y } = (b, y)

theorem Bundle.Trivialization.continuousOn_symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F TotalSpace.proj) : ContinuousOn (fun (z : B × F) => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ Set.univ)

def Bundle.Trivialization.transFiberHomeomorph {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {F' : Type u_5} [TopologicalSpace 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Trivialization.transFiberHomeomorph_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {F' : Type u_5} [TopologicalSpace F'] (e : Trivialization F proj) (h : F ≃ₜ F') (x : Z) : ↑(e.transFiberHomeomorph h) x = ((↑e x).1, h (↑e x).2)

def Bundle.Trivialization.coordChange {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace 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 Bundle.Trivialization.coordChangeHomeomorph for a version bundled as F ≃ₜ F.

Equations

• e₁.coordChange e₂ b x = (↑e₂ (↑e₁.symm (b, x))).2

theorem Bundle.Trivialization.mk_coordChange {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (x : F) : (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))

theorem Bundle.Trivialization.coordChange_apply_snd {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ : Trivialization F proj) {p : Z} (h : proj p ∈ e₁.baseSet) : e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2

@[simp]

theorem Bundle.Trivialization.coordChange_same_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) (x : F) : e.coordChange e b x = x

theorem Bundle.Trivialization.coordChange_same {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) : e.coordChange e b = id

theorem Bundle.Trivialization.coordChange_coordChange {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ e₃ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (x : F) : e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x

theorem Bundle.Trivialization.continuous_coordChange {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) : Continuous (e₁.coordChange e₂ b)

def Bundle.Trivialization.coordChangeHomeomorph {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) : F ≃ₜ F

Coordinate transformation in the fiber induced by a pair of bundle trivializations, as a homeomorphism.

Equations

• e₁.coordChangeHomeomorph e₂ h₁ h₂ = { toFun := e₁.coordChange e₂ b, invFun := e₂.coordChange e₁ b, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Bundle.Trivialization.coordChangeHomeomorph_coe {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) : ⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b

theorem Bundle.Trivialization.isImage_preimage_prod {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) : e.IsImage (proj ⁻¹' s) (s ×ˢ Set.univ)

def Bundle.Trivialization.restrOpen {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) (hs : IsOpen s) : Trivialization F proj

Restrict a Trivialization to an open set in the base.

Equations

• e.restrOpen s hs = { toOpenPartialHomeomorph := (⋯.restr ⋯).symm, baseSet := e.baseSet ∩ s, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }

noncomputable def Bundle.Trivialization.restrictPreimage' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : Trivialization F (s.restrictPreimage proj)

The restriction of a trivialization to a subset of the base.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Trivialization.restrictPreimage'_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : (e.restrictPreimage' s).target = Prod.map Subtype.val id ⁻¹' e.toPretrivialization.target

@[simp]

theorem Bundle.Trivialization.restrictPreimage'_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : (e.restrictPreimage' s).baseSet = Subtype.val ⁻¹' e.toPretrivialization.baseSet

@[simp]

theorem Bundle.Trivialization.restrictPreimage'_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] (z : ↑(proj ⁻¹' s)) : ↑(e.restrictPreimage' s) z = (⟨proj ↑z, ⋯⟩, (↑e.toPretrivialization ↑z).2)

@[simp]

theorem Bundle.Trivialization.restrictPreimage'_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) [Nonempty (↑s → F → ↑(proj ⁻¹' s))] : (e.restrictPreimage' s).source = Subtype.val ⁻¹' e.toPretrivialization.source

noncomputable def Bundle.Trivialization.restrictPreimage {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : Trivialization F (s.restrictPreimage proj)

The restriction of a trivialization to a set with nonempty intersection with the base set.

Equations

• e.restrictPreimage hs = e.restrictPreimage' s

@[simp]

theorem Bundle.Trivialization.restrictPreimage_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : (e.restrictPreimage hs).source = Subtype.val ⁻¹' e.toPretrivialization.source

@[simp]

theorem Bundle.Trivialization.restrictPreimage_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : (e.restrictPreimage hs).baseSet = Subtype.val ⁻¹' e.toPretrivialization.baseSet

@[simp]

theorem Bundle.Trivialization.restrictPreimage_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) (z : ↑(proj ⁻¹' s)) : ↑(e.restrictPreimage hs) z = (⟨proj ↑z, ⋯⟩, (↑e.toPretrivialization ↑z).2)

@[simp]

theorem Bundle.Trivialization.restrictPreimage_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty) : (e.restrictPreimage hs).target = Prod.map Subtype.val id ⁻¹' e.toPretrivialization.target

noncomputable def Bundle.Trivialization.domExtend {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Trivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : Trivialization F proj

Extend the total space of a trivialization from the preimage of a set to the whole space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Trivialization.domExtend_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Trivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : (domExtend hps e).target = e.toPretrivialization.target

@[simp]

theorem Bundle.Trivialization.domExtend_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Trivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : (domExtend hps e).baseSet = e.toPretrivialization.baseSet

@[simp]

theorem Bundle.Trivialization.domExtend_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Trivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] : (domExtend hps e).source = Subtype.val '' e.toPretrivialization.source

@[simp]

theorem Bundle.Trivialization.domExtend_symm_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Trivialization F fun (z : ↑(proj ⁻¹' s)) => proj ↑z) [Nonempty (Z → F)] (x : B × F) : ↑(domExtend hps e).symm x = ↑(↑e.toPretrivialization.symm x)

noncomputable def Bundle.Trivialization.codExtend' {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Trivialization F proj) [Nonempty (B → F → Z)] : Trivialization F (Subtype.val ∘ proj)

Extend the base of a trivialization from a set to the whole space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bundle.Trivialization.codExtend'_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Trivialization F proj) [Nonempty (B → F → Z)] : (codExtend' hs e).target = Prod.map Subtype.val id '' e.toPretrivialization.target

@[simp]

theorem Bundle.Trivialization.codExtend'_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Trivialization F proj) [Nonempty (B → F → Z)] : (codExtend' hs e).baseSet = Subtype.val '' e.toPretrivialization.baseSet

@[simp]

theorem Bundle.Trivialization.codExtend'_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Trivialization F proj) [Nonempty (B → F → Z)] : (codExtend' hs e).source = e.toPretrivialization.source

@[simp]

theorem Bundle.Trivialization.codExtend'_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Trivialization F proj) [Nonempty (B → F → Z)] (z : Z) : ↑(codExtend' hs e) z = (↑(↑e.toPretrivialization z).1, (↑e.toPretrivialization z).2)

noncomputable def Bundle.Trivialization.codExtend {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Trivialization F proj) : Trivialization F (Subtype.val ∘ proj)

Extend the base of a pretrivialization from a nonempty set to the whole space.

Equations

• Bundle.Trivialization.codExtend hs nonempty e = Bundle.Trivialization.codExtend' hs e

@[simp]

theorem Bundle.Trivialization.codExtend_source {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Trivialization F proj) : (codExtend hs nonempty e).source = e.toPretrivialization.source

@[simp]

theorem Bundle.Trivialization.codExtend_baseSet {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Trivialization F proj) : (codExtend hs nonempty e).baseSet = Subtype.val '' e.toPretrivialization.baseSet

@[simp]

theorem Bundle.Trivialization.codExtend_apply {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Trivialization F proj) (z : Z) : ↑(codExtend hs nonempty e) z = (↑(↑e.toPretrivialization z).1, (↑e.toPretrivialization z).2)

@[simp]

theorem Bundle.Trivialization.codExtend_target {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Trivialization F proj) : (codExtend hs nonempty e).target = Prod.map Subtype.val id '' e.toPretrivialization.target

theorem Bundle.Trivialization.frontier_preimage {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) : e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)

noncomputable def Bundle.Trivialization.piecewise {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e e' : Trivialization F proj) (s : Set B) (Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ 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.baseSet ∩ frontier s, e.piecewise e' s Hs Heq is the bundle trivialization over Set.ite s e.baseSet e'.baseSet that is equal to e on proj ⁻¹ s and is equal to e' otherwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Bundle.Trivialization.piecewiseLeOfEq {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] [LinearOrder B] [OrderTopology B] (e e' : Trivialization F proj) (a : B) (He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) (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.baseSet ∩ e'.baseSet 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.baseSet e'.baseSet that is equal to e on points p such that proj p ≤ a and is equal to e' otherwise.

Equations

• e.piecewiseLeOfEq e' a He He' Heq = e.piecewise e' (Set.Iic a) ⋯ ⋯

noncomputable def Bundle.Trivialization.piecewiseLe {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] [LinearOrder B] [OrderTopology B] (e e' : Trivialization F proj) (a : B) (He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) : 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.baseSet ∩ e'.baseSet, e.piecewise_le e' a He He' is the bundle trivialization over Set.ite (Iic a) e.baseSet e'.baseSet 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 that h (e' p).2 = (e p).2 whenever e p = a.

Equations

• e.piecewiseLe e' a He He' = e.piecewiseLeOfEq (e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) a He He' ⋯

noncomputable def Bundle.Trivialization.disjointUnion {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e e' : Trivialization F proj) (H : Disjoint e.baseSet e'.baseSet) : 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

• One or more equations did not get rendered due to their size.

def Bundle.Trivialization.lift {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (T : Trivialization F proj) (z : Z) (b : B) : Z

The local lifting through a Trivialization T from the base to the leaf containing z.

Equations

• T.lift z b = T.invFun (b, (↑T z).2)

@[simp]

theorem Bundle.Trivialization.lift_self {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {T : Trivialization F proj} {z : Z} (he : proj z ∈ T.baseSet) : T.lift z (proj z) = z

theorem Bundle.Trivialization.proj_lift {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {T : Trivialization F proj} {z : Z} {b : B} (hx : b ∈ T.baseSet) : proj (T.lift z b) = b

def Bundle.Trivialization.liftCM {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (T : Trivialization F proj) : C(↑T.source × ↑T.baseSet, ↑T.source)

The restriction of lift to the source and base set of T, as a bundled continuous map.

Equations

• T.liftCM = { toFun := fun (ex : ↑T.source × ↑T.baseSet) => ⟨T.lift ↑ex.1 ↑ex.2, ⋯⟩, continuous_toFun := ⋯ }

def Bundle.Trivialization.clift {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {ι : Type u_5} [TopologicalSpace ι] (T : Trivialization F proj) [LocallyCompactPair ι ↑T.baseSet] : C(↑T.source × C(ι, ↑T.baseSet), C(ι, ↑T.source))

Extension of liftCM to continuous maps taking values in T.baseSet (local version of homotopy lifting)

Equations

• T.clift = (T.liftCM.comp { toFun := fun (eγt : (↑T.source × C(ι, ↑T.baseSet)) × ι) => (eγt.1.1, eγt.1.2 eγt.2), continuous_toFun := ⋯ }).curry

@[simp]

theorem Bundle.Trivialization.clift_self {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {T : Trivialization F proj} {ι : Type u_5} [TopologicalSpace ι] [LocallyCompactPair ι ↑T.baseSet] {γ : C(ι, ↑T.baseSet)} {i : ι} {e : ↑T.source} (h : proj ↑e = ↑(γ i)) : (T.clift (e, γ)) i = e

theorem Bundle.Trivialization.proj_clift {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {T : Trivialization F proj} {ι : Type u_5} [TopologicalSpace ι] [LocallyCompactPair ι ↑T.baseSet] {γ : C(ι, ↑T.baseSet)} {i : ι} {e : ↑T.source} : proj ↑((T.clift (e, γ)) i) = ↑(γ i)