diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index 53f4e3afd9a9d..f6f3e1f104624 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jan-David Salchow, SΓ©bastien GouΓ«zel, Jean Lo ! This file was ported from Lean 3 source module analysis.normed_space.operator_norm -! leanprover-community/mathlib commit 91862a6001a8b6ae3f261cdd8eea42f6ac596886 +! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -1991,52 +1991,6 @@ theorem coord_norm (x : E) (h : x β‰  0) : β€–coord π•œ x hβ€– = β€–x‖⁻¹ : homothety_inverse _ hx _ (toSpanNonzeroSingleton_homothety π•œ x h) _ #align continuous_linear_equiv.coord_norm ContinuousLinearEquiv.coord_norm -variable {π•œ} {π•œβ‚„ : Type _} [NontriviallyNormedField π•œβ‚„] - -variable {H : Type _} [NormedAddCommGroup H] [NormedSpace π•œβ‚„ H] [NormedSpace π•œβ‚ƒ G] - -variable {σ₂₃ : π•œβ‚‚ β†’+* π•œβ‚ƒ} {σ₁₃ : π•œ β†’+* π•œβ‚ƒ} - -variable {σ₃₄ : π•œβ‚ƒ β†’+* π•œβ‚„} {σ₄₃ : π•œβ‚„ β†’+* π•œβ‚ƒ} - -variable {Οƒβ‚‚β‚„ : π•œβ‚‚ β†’+* π•œβ‚„} {σ₁₄ : π•œ β†’+* π•œβ‚„} - -variable [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] - -variable [RingHomCompTriple σ₂₁ σ₁₄ Οƒβ‚‚β‚„] [RingHomCompTriple Οƒβ‚‚β‚„ σ₄₃ σ₂₃] - -variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] - -variable [RingHomIsometric σ₁₄] [RingHomIsometric σ₂₃] - -variable [RingHomIsometric σ₄₃] [RingHomIsometric Οƒβ‚‚β‚„] - -variable [RingHomIsometric σ₁₃] [RingHomIsometric σ₁₂] - -variable [RingHomIsometric σ₃₄] - -/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence -between the spaces of continuous (semi)linear maps. -/ -@[simps apply symm_apply] -def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E β†’SL[σ₁₄] H) ≃SL[σ₄₃] F β†’SL[σ₂₃] G := - {e₁₂.arrowCongrEquiv e₄₃ with -- given explicitly to help `simps` - toFun := fun L => (e₄₃ : H β†’SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F β†’SL[σ₂₁] E)) - invFun := fun L => (e₄₃.symm : G β†’SL[σ₃₄] H).comp (L.comp (e₁₂ : E β†’SL[σ₁₂] F)) - map_add' := fun f g => by simp only [add_comp, comp_add] - map_smul' := fun t f => by simp only [smul_comp, comp_smulβ‚›β‚—] - continuous_toFun := (continuous_id.clm_comp_const _).const_clm_comp _ - continuous_invFun := (continuous_id.clm_comp_const _).const_clm_comp _ } -set_option linter.uppercaseLean3 false in -#align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL - -/-- A pair of continuous linear equivalences generates an continuous linear equivalence between -the spaces of continuous linear maps. -/ -def arrowCongr {F H : Type _} [NormedAddCommGroup F] [NormedAddCommGroup H] [NormedSpace π•œ F] - [NormedSpace π•œ G] [NormedSpace π•œ H] (e₁ : E ≃L[π•œ] F) (eβ‚‚ : H ≃L[π•œ] G) : - (E β†’L[π•œ] H) ≃L[π•œ] F β†’L[π•œ] G := - arrowCongrSL e₁ eβ‚‚ -#align continuous_linear_equiv.arrow_congr ContinuousLinearEquiv.arrowCongr - end end ContinuousLinearEquiv diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean index 163c0f044b642..286a8fe425e92 100644 --- a/Mathlib/Analysis/NormedSpace/PiLp.lean +++ b/Mathlib/Analysis/NormedSpace/PiLp.lean @@ -945,19 +945,13 @@ protected def linearEquiv : PiLp p Ξ² ≃ₗ[π•œ] βˆ€ i, Ξ² i := #align pi_Lp.linear_equiv PiLp.linearEquiv /-- `PiLp.equiv` as a continuous linear equivalence. -/ -@[simps! (config := { fullyApplied := false }) toFun apply symm_apply] +@[simps! (config := { fullyApplied := false }) apply symm_apply] protected def continuousLinearEquiv : PiLp p Ξ² ≃L[π•œ] βˆ€ i, Ξ² i where toLinearEquiv := PiLp.linearEquiv _ _ _ continuous_toFun := continuous_equiv _ _ continuous_invFun := continuous_equiv_symm _ _ #align pi_Lp.continuous_linear_equiv PiLp.continuousLinearEquiv --- Porting note: defined separately to appease simpNF linter -@[simp high] -theorem continuousLinearEquiv_invFun : - (PiLp.continuousLinearEquiv p π•œ Ξ²).toLinearEquiv.invFun = ↑(PiLp.equiv p fun i ↦ Ξ² i).symm := - rfl - section Basis variable (ΞΉ) diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index f9c1f888ab947..be160eb9665b5 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -1992,8 +1992,7 @@ def Simps.symm_apply (h : M₁ ≃SL[σ₁₂] Mβ‚‚) : Mβ‚‚ β†’ M₁ := h.symm #align continuous_linear_equiv.simps.symm_apply ContinuousLinearEquiv.Simps.symm_apply -initialize_simps_projections ContinuousLinearEquiv - (toLinearEquiv_toFun β†’ apply, toLinearEquiv_invFun β†’ symm_apply) +initialize_simps_projections ContinuousLinearEquiv (toFun β†’ apply, invFun β†’ symm_apply) theorem symm_map_nhds_eq (e : M₁ ≃SL[σ₁₂] Mβ‚‚) (x : M₁) : map e.symm (𝓝 (e x)) = 𝓝 x := e.toHomeomorph.symm_map_nhds_eq x diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean index 3b227962f58eb..a40775b18ef0c 100644 --- a/Mathlib/Topology/Algebra/Module/StrongTopology.lean +++ b/Mathlib/Topology/Algebra/Module/StrongTopology.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Anatole Dedecker ! This file was ported from Lean 3 source module topology.algebra.module.strong_topology -! leanprover-community/mathlib commit b8627dbac120a9ad6267a75575ae1e070d5bff5b +! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -230,3 +230,82 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F end BoundedSets end ContinuousLinearMap + +open ContinuousLinearMap + +namespace ContinuousLinearEquiv + +section Semilinear + +variable {π•œ : Type _} {π•œβ‚‚ : Type _} {π•œβ‚ƒ : Type _} {π•œβ‚„ : Type _} {E : Type _} {F : Type _} + {G : Type _} {H : Type _} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] + [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œβ‚‚] [NontriviallyNormedField π•œβ‚ƒ] + [NontriviallyNormedField π•œβ‚„] [Module π•œ E] [Module π•œβ‚‚ F] [Module π•œβ‚ƒ G] [Module π•œβ‚„ H] + [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] + [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul π•œβ‚ƒ G] + [ContinuousConstSMul π•œβ‚„ H] {σ₁₂ : π•œ β†’+* π•œβ‚‚} {σ₂₁ : π•œβ‚‚ β†’+* π•œ} {σ₂₃ : π•œβ‚‚ β†’+* π•œβ‚ƒ} {σ₁₃ : π•œ β†’+* π•œβ‚ƒ} + {σ₃₄ : π•œβ‚ƒ β†’+* π•œβ‚„} {σ₄₃ : π•œβ‚„ β†’+* π•œβ‚ƒ} {Οƒβ‚‚β‚„ : π•œβ‚‚ β†’+* π•œβ‚„} {σ₁₄ : π•œ β†’+* π•œβ‚„} [RingHomInvPair σ₁₂ σ₂₁] + [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] + [RingHomCompTriple σ₂₁ σ₁₄ Οƒβ‚‚β‚„] [RingHomCompTriple Οƒβ‚‚β‚„ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] + +/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the +spaces of continuous (semi)linear maps. -/ +@[simps] +def arrowCongrβ‚›β‚— (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E β†’SL[σ₁₄] H) ≃ₛₗ[σ₄₃] F β†’SL[σ₂₃] G := + { e₁₂.arrowCongrEquiv e₄₃ with + -- given explicitly to help `simps` + toFun := fun L => (e₄₃ : H β†’SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F β†’SL[σ₂₁] E)) + -- given explicitly to help `simps` + invFun := fun L => (e₄₃.symm : G β†’SL[σ₃₄] H).comp (L.comp (e₁₂ : E β†’SL[σ₁₂] F)) + map_add' := fun f g => by simp only [add_comp, comp_add] + map_smul' := fun t f => by simp only [smul_comp, comp_smulβ‚›β‚—] } +#align continuous_linear_equiv.arrow_congrβ‚›β‚— ContinuousLinearEquiv.arrowCongrβ‚›β‚— + +variable [RingHomIsometric σ₂₁] + +theorem arrowCongrβ‚›β‚—_continuous (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : + Continuous (id (e₁₂.arrowCongrβ‚›β‚— e₄₃ : (E β†’SL[σ₁₄] H) ≃ₛₗ[σ₄₃] F β†’SL[σ₂₃] G)) := by + apply continuous_of_continuousAt_zero + show Filter.Tendsto _ _ _ + simp_rw [(arrowCongrβ‚›β‚— e₁₂ e₄₃).map_zero] + rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff ContinuousLinearMap.hasBasis_nhds_zero] + rintro ⟨sF, sG⟩ ⟨h1 : Bornology.IsVonNBounded π•œβ‚‚ sF, h2 : sG ∈ nhds (0 : G)⟩ + dsimp + refine' ⟨(e₁₂.symm '' sF, e₄₃ ⁻¹' sG), ⟨h1.image (e₁₂.symm : F β†’SL[σ₂₁] E), _⟩, fun _ h _ hx => + h _ (Set.mem_image_of_mem _ hx)⟩ + apply e₄₃.continuous.continuousAt + simpa using h2 +#align continuous_linear_equiv.arrow_congrβ‚›β‚—_continuous ContinuousLinearEquiv.arrowCongrβ‚›β‚—_continuous + +variable [RingHomIsometric σ₁₂] + +/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence +between the spaces of continuous (semi)linear maps. -/ +@[simps!] +def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E β†’SL[σ₁₄] H) ≃SL[σ₄₃] F β†’SL[σ₂₃] G := + { e₁₂.arrowCongrβ‚›β‚— e₄₃ with + continuous_toFun := e₁₂.arrowCongrβ‚›β‚—_continuous e₄₃ + continuous_invFun := e₁₂.symm.arrowCongrβ‚›β‚—_continuous e₄₃.symm } +set_option linter.uppercaseLean3 false in +#align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL + +end Semilinear + +section Linear + +variable {π•œ : Type _} {E : Type _} {F : Type _} {G : Type _} {H : Type _} [AddCommGroup E] + [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField π•œ] [Module π•œ E] + [Module π•œ F] [Module π•œ G] [Module π•œ H] [TopologicalSpace E] [TopologicalSpace F] + [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H] + [ContinuousConstSMul π•œ G] [ContinuousConstSMul π•œ H] + +/-- A pair of continuous linear equivalences generates an continuous linear equivalence between +the spaces of continuous linear maps. -/ +def arrowCongr (e₁ : E ≃L[π•œ] F) (eβ‚‚ : H ≃L[π•œ] G) : (E β†’L[π•œ] H) ≃L[π•œ] F β†’L[π•œ] G := + e₁.arrowCongrSL eβ‚‚ +#align continuous_linear_equiv.arrow_congr ContinuousLinearEquiv.arrowCongr + +end Linear + +end ContinuousLinearEquiv diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index ae7030530a3a8..5b48173e80162 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes HΓΆlzl, Mario Carneiro, Patrick Massot ! This file was ported from Lean 3 source module topology.constructions -! leanprover-community/mathlib commit 76f9c990d4b7c3dd26b87c4c4b51759e249d9e66 +! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -807,6 +807,18 @@ theorem Inducing.prod_map {f : Ξ± β†’ Ξ²} {g : Ξ³ β†’ Ξ΄} (hf : Inducing f) (hg hg.nhds_eq_comap, prod_comap_comap_eq] #align inducing.prod_mk Inducing.prod_map +@[simp] +theorem inducing_const_prod {a : Ξ±} {f : Ξ² β†’ Ξ³} : (Inducing fun x => (a, f x)) ↔ Inducing f := by + simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp, + induced_const, top_inf_eq] +#align inducing_const_prod inducing_const_prod + +@[simp] +theorem inducing_prod_const {b : Ξ²} {f : Ξ± β†’ Ξ³} : (Inducing fun x => (f x, b)) ↔ Inducing f := by + simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp, + induced_const, inf_top_eq] +#align inducing_prod_const inducing_prod_const + theorem Embedding.prod_map {f : Ξ± β†’ Ξ²} {g : Ξ³ β†’ Ξ΄} (hf : Embedding f) (hg : Embedding g) : Embedding (Prod.map f g) := { hf.toInducing.prod_map hg.toInducing with diff --git a/Mathlib/Topology/FiberBundle/Basic.lean b/Mathlib/Topology/FiberBundle/Basic.lean index 21a254ac9de7b..b0880111cce50 100644 --- a/Mathlib/Topology/FiberBundle/Basic.lean +++ b/Mathlib/Topology/FiberBundle/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: SΓ©bastien GouΓ«zel, Floris van Doorn, Heather Macbeth ! This file was ported from Lean 3 source module topology.fiber_bundle.basic -! leanprover-community/mathlib commit 0187644979f2d3e10a06e916a869c994facd9a87 +! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -779,6 +779,7 @@ end FiberBundleCore /-! ### Prebundle construction for constructing fiber bundles -/ variable (F) (E : B β†’ Type _) [TopologicalSpace B] [TopologicalSpace F] + [βˆ€ x, TopologicalSpace (E x)] /-- This structure permits to define a fiber bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a @@ -792,6 +793,7 @@ structure FiberPrebundle where pretrivialization_mem_atlas : βˆ€ x : B, pretrivializationAt x ∈ pretrivializationAtlas continuous_trivChange : βˆ€ e, e ∈ pretrivializationAtlas β†’ βˆ€ e', e' ∈ pretrivializationAtlas β†’ ContinuousOn (e ∘ e'.toLocalEquiv.symm) (e'.target ∩ e'.toLocalEquiv.symm ⁻¹' e.source) + totalSpaceMk_inducing : βˆ€ b : B, Inducing (pretrivializationAt b ∘ totalSpaceMk b) #align fiber_prebundle FiberPrebundle namespace FiberPrebundle @@ -862,35 +864,38 @@ theorem totalSpaceMk_preimage_source (b : B) : eq_univ_of_forall (a.mem_pretrivializationAt_source b) #align fiber_prebundle.total_space_mk_preimage_source FiberPrebundle.totalSpaceMk_preimage_source -/-- Topology on the fibers `E b` induced by the map `E b β†’ E.TotalSpace`. -/ -def fiberTopology (b : B) : TopologicalSpace (E b) := - TopologicalSpace.induced (totalSpaceMk b) a.totalSpaceTopology -#align fiber_prebundle.fiber_topology FiberPrebundle.fiberTopology - -@[continuity] -theorem inducing_totalSpaceMk (b : B) : - @Inducing _ _ (a.fiberTopology b) a.totalSpaceTopology (totalSpaceMk b) := by - letI := a.totalSpaceTopology - letI := a.fiberTopology b - exact ⟨rfl⟩ -#align fiber_prebundle.inducing_total_space_mk FiberPrebundle.inducing_totalSpaceMk - @[continuity] theorem continuous_totalSpaceMk (b : B) : - Continuous[a.fiberTopology b, a.totalSpaceTopology] (totalSpaceMk b) := by - letI := a.totalSpaceTopology; letI := a.fiberTopology b - exact (a.inducing_totalSpaceMk b).continuous + Continuous[_, a.totalSpaceTopology] (totalSpaceMk b) := by + letI := a.totalSpaceTopology + let e := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b) + rw [e.toLocalHomeomorph.continuous_iff_continuous_comp_left + (a.totalSpaceMk_preimage_source b)] + exact continuous_iff_le_induced.mpr (le_antisymm_iff.mp (a.totalSpaceMk_inducing b).induced).1 #align fiber_prebundle.continuous_total_space_mk FiberPrebundle.continuous_totalSpaceMk +theorem inducing_totalSpaceMk_of_inducing_comp (b : B) + (h : Inducing (a.pretrivializationAt b ∘ totalSpaceMk b)) : + @Inducing _ _ _ a.totalSpaceTopology (totalSpaceMk b) := by + letI := a.totalSpaceTopology + rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h + apply Inducing.of_codRestrict (a.mem_pretrivializationAt_source b) + refine inducing_of_inducing_compose ?_ (continuousOn_iff_continuous_restrict.mp + (a.trivializationOfMemPretrivializationAtlas + (a.pretrivialization_mem_atlas b)).continuous_toFun) h + exact (a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b) +#align fiber_prebundle.inducing_total_space_mk_of_inducing_comp FiberPrebundle.inducing_totalSpaceMk_of_inducing_comp + /-- Make a `FiberBundle` from a `FiberPrebundle`. Concretely this means that, given a `FiberPrebundle` structure for a sigma-type `E` -- which consists of a number of "pretrivializations" identifying parts of `E` with product spaces `U Γ— F` -- one establishes that for the topology constructed on the sigma-type using `FiberPrebundle.totalSpaceTopology`, these "pretrivializations" are actually "trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/ -def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology a.fiberTopology := - let _ := a.totalSpaceTopology; let _ := a.fiberTopology - { totalSpaceMk_inducing' := a.inducing_totalSpaceMk, +def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology _ := + let _ := a.totalSpaceTopology + { totalSpaceMk_inducing' := fun b ↦ a.inducing_totalSpaceMk_of_inducing_comp b + (a.totalSpaceMk_inducing b) trivializationAtlas' := { e | βˆƒ (eβ‚€ : _) (heβ‚€ : eβ‚€ ∈ a.pretrivializationAtlas), e = a.trivializationOfMemPretrivializationAtlas heβ‚€ }, @@ -902,7 +907,6 @@ def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology a.fiberTopology theorem continuous_proj : @Continuous _ _ a.totalSpaceTopology _ (Ο€ E) := by letI := a.totalSpaceTopology - letI := a.fiberTopology letI := a.toFiberBundle exact FiberBundle.continuous_proj F E #align fiber_prebundle.continuous_proj FiberPrebundle.continuous_proj diff --git a/Mathlib/Topology/VectorBundle/Basic.lean b/Mathlib/Topology/VectorBundle/Basic.lean index 4f95d228ff902..f3594a1a77106 100644 --- a/Mathlib/Topology/VectorBundle/Basic.lean +++ b/Mathlib/Topology/VectorBundle/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: NicolΓ² Cavalleri, Sebastien Gouezel, Heather Macbeth, Patrick Massot, Floris van Doorn ! This file was ported from Lean 3 source module topology.vector_bundle.basic -! leanprover-community/mathlib commit d2d964c64f8ddcccd6704a731c41f95d13e72f5c +! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -61,6 +61,7 @@ Vector bundle noncomputable section open Bundle Set Classical +open scoped Topology variable (R : Type _) {B : Type _} (F : Type _) (E : B β†’ Type _) @@ -841,7 +842,7 @@ end section variable [NontriviallyNormedField R] [βˆ€ x, AddCommMonoid (E x)] [βˆ€ x, Module R (E x)] - [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] + [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [βˆ€ x, TopologicalSpace (E x)] open TopologicalSpace @@ -867,6 +868,7 @@ structure VectorPrebundle where exists_coordChange : βˆ€α΅‰ (e ∈ pretrivializationAtlas) (e' ∈ pretrivializationAtlas), βˆƒ f : B β†’ F β†’L[R] F, ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧ βˆ€α΅‰ (b ∈ e.baseSet ∩ e'.baseSet) (v : F), f b v = (e' (totalSpaceMk b (e.symm b v))).2 + totalSpaceMk_inducing : βˆ€ b : B, Inducing (pretrivializationAt b ∘ totalSpaceMk b) #align vector_prebundle VectorPrebundle namespace VectorPrebundle @@ -953,26 +955,15 @@ theorem totalSpaceMk_preimage_source (b : B) : a.toFiberPrebundle.totalSpaceMk_preimage_source b #align vector_prebundle.total_space_mk_preimage_source VectorPrebundle.totalSpaceMk_preimage_source -/-- Topology on the fibers `E b` induced by the map `E b β†’ Bundle.TotalSpace E`. -/ -def fiberTopology (b : B) : TopologicalSpace (E b) := - a.toFiberPrebundle.fiberTopology b -#align vector_prebundle.fiber_topology VectorPrebundle.fiberTopology - -@[continuity] -theorem inducing_totalSpaceMk (b : B) : - @Inducing _ _ (a.fiberTopology b) a.totalSpaceTopology (totalSpaceMk b) := - a.toFiberPrebundle.inducing_totalSpaceMk b -#align vector_prebundle.inducing_total_space_mk VectorPrebundle.inducing_totalSpaceMk - @[continuity] theorem continuous_totalSpaceMk (b : B) : - @Continuous _ _ (a.fiberTopology b) a.totalSpaceTopology (totalSpaceMk b) := + Continuous[_, a.totalSpaceTopology] (totalSpaceMk b) := a.toFiberPrebundle.continuous_totalSpaceMk b #align vector_prebundle.continuous_total_space_mk VectorPrebundle.continuous_totalSpaceMk /-- Make a `FiberBundle` from a `VectorPrebundle`; auxiliary construction for `VectorPrebundle.to_vectorBundle`. -/ -def toFiberBundle : @FiberBundle B F _ _ _ a.totalSpaceTopology a.fiberTopology := +def toFiberBundle : @FiberBundle B F _ _ _ a.totalSpaceTopology _ := a.toFiberPrebundle.toFiberBundle #align vector_prebundle.to_fiber_bundle VectorPrebundle.toFiberBundle @@ -983,8 +974,8 @@ establishes that for the topology constructed on the sigma-type using `VectorPrebundle.totalSpaceTopology`, these "pretrivializations" are actually "trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/ theorem to_vectorBundle : - @VectorBundle R _ F E _ _ _ _ _ _ a.totalSpaceTopology a.fiberTopology a.toFiberBundle := - letI := a.totalSpaceTopology; letI := a.fiberTopology; letI := a.toFiberBundle + @VectorBundle R _ F E _ _ _ _ _ _ a.totalSpaceTopology _ a.toFiberBundle := + letI := a.totalSpaceTopology; letI := a.toFiberBundle { trivialization_linear' := by rintro _ ⟨e, he, rfl⟩ apply linear_trivializationOfMemPretrivializationAtlas @@ -1016,7 +1007,7 @@ variable [NormedSpace π•œβ‚ F] [βˆ€ x, Module π•œβ‚ (E x)] [TopologicalSpace variable {F' : Type _} [NormedAddCommGroup F'] [NormedSpace π•œβ‚‚ F'] {E' : B' β†’ Type _} [βˆ€ x, AddCommMonoid (E' x)] [βˆ€ x, Module π•œβ‚‚ (E' x)] [TopologicalSpace (TotalSpace E')] -variable [βˆ€ x, TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle π•œβ‚ F E] +variable [FiberBundle F E] [VectorBundle π•œβ‚ F E] variable [βˆ€ x, TopologicalSpace (E' x)] [FiberBundle F' E'] [VectorBundle π•œβ‚‚ F' E']