Trivializations

Main definitions

Basic definitions

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

• 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.

• 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 Trivialization (no namespace), together with a mixin class 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 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
• 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 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

instance 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

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

theorem 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 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 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 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 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 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 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 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

theorem 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

theorem 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 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 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 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 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 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

theorem 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

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

theorem 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

@[simp]

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

@[simp]

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

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

theorem 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 Bundle.TotalSpace.proj) (h : x ∈ e'.baseSet) : (↑e'.symm (x, y)).proj = x

noncomputable def 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 Bundle.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 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 Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : e.symm b y = cast ⋯ (↑e.symm (b, y)).snd

theorem Pretrivialization.symm_apply_of_not_mem {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 Bundle.TotalSpace.proj) {b : B} (hb : b ∉ e.baseSet) (y : F) : e.symm b y = 0

theorem Pretrivialization.coe_symm_of_not_mem {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 Bundle.TotalSpace.proj) {b : B} (hb : b ∉ e.baseSet) : e.symm b = 0

theorem 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 Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : { proj := b, snd := e.symm b y } = ↑e.symm (b, y)

theorem 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 Bundle.TotalSpace.proj) (z : Bundle.TotalSpace F E) (hz : z.proj ∈ e.baseSet) : e.symm z.proj (↑e z).2 = z.snd

theorem 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 Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : E b) : e.symm b (↑e { proj := b, snd := y }).2 = y

theorem 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 Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : ↑e { proj := b, snd := e.symm b y } = (b, y)

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

A structure extending partial homeomorphisms, defining a local trivialization of a projection proj : Z → B with fiber F, as a 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
• 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.toPartialHomeomorph p).1 = proj p

theorem 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.toPartialHomeomorph = e'.toPartialHomeomorph) (h₂ : e.baseSet = e'.baseSet) : e = e'

def 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 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 := ⋯ }

instance 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

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

instance 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

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

theorem 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 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.toPartialHomeomorph = ↑e

@[simp]

theorem 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 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 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

theorem 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 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 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 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 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 : PartialHomeomorph 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) : ↑{ toPartialHomeomorph := e, baseSet := i, open_baseSet := j, source_eq := k, target_eq := l, proj_toFun := m } x = ↑e x

theorem 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 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 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 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 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

theorem 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

theorem 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Trivialization.preimageHomeomorph_symm_apply.

Equations

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

@[simp]

theorem 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 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 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 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 Trivialization.sourceHomeomorphBaseSetProd_symm_apply.

Equations

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

@[simp]

theorem 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 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 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 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 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

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

Composition of a Trivialization and a Homeomorph.

Equations

• e.compHomeomorph h = { toPartialHomeomorph := h.toPartialHomeomorph.trans e.toPartialHomeomorph, baseSet := e.baseSet, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }

theorem 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 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 Trivialization.continuousOn {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) : ContinuousOn (↑e') e'.source

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

@[simp]

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

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

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

@[simp]

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

noncomputable def Trivialization.symm {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.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 Trivialization.symm_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : e.symm b y = cast ⋯ (↑e.symm (b, y)).snd

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

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

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

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

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

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

def 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 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 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 Trivialization.coordChangeHomeomorph for a version bundled as F ≃ₜ F.

Equations

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

theorem 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 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

theorem 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 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 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 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 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 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 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 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 = { toPartialHomeomorph := (⋯.restr ⋯).symm, baseSet := e.baseSet ∩ s, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }

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