diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean index 1ed5d8debe5ce..b4cc643968f53 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean @@ -83,10 +83,7 @@ lemma isClosedEmbedding_cfcₙAux : IsClosedEmbedding (cfcₙAux hp₁ a ha) := refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp ContinuousMapZero.isClosedEmbedding_toContinuousMap let e : C(σₙ 𝕜 a, 𝕜) ≃ₜ C(σ 𝕜 (a : A⁺¹), 𝕜) := - { (Homeomorph.compStarAlgEquiv' 𝕜 𝕜 <| .setCongr <| - (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a).symm) with - continuous_toFun := ContinuousMap.continuous_comp_left _ - continuous_invFun := ContinuousMap.continuous_comp_left _ } + (Homeomorph.setCongr (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a)).arrowCongr (.refl _) exact e.isClosedEmbedding @[deprecated (since := "2024-10-20")] diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean index ed76c4a88dc63..458c86fac7e39 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean @@ -178,7 +178,7 @@ theorem cfcₙHom_comp [UniqueNonUnitalContinuousFunctionalCalculus R A] (f : C( suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_ · refine (cfcₙHom_isClosedEmbedding ha).continuous.comp <| continuous_induced_rng.mpr ?_ - exact f'.toContinuousMap.continuous_comp_left.comp continuous_induced_dom + exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom · simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk', NonUnitalAlgHom.coe_mk] congr diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean index 5186931925074..0643b90789114 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean @@ -56,7 +56,7 @@ namespace ContinuousMap noncomputable def toNNReal (f : C(X, ℝ)) : C(X, ℝ≥0) := .realToNNReal |>.comp f @[fun_prop] -lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_comp _ +lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_postcomp _ @[simp] lemma toNNReal_apply (f : C(X, ℝ)) (x : X) : f.toNNReal x = (f x).toNNReal := rfl @@ -187,7 +187,7 @@ instance NNReal.instUniqueContinuousFunctionalCalculus [UniqueContinuousFunction Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by intro ξ' refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <| - ContinuousMap.continuous_comp_left _, ?_⟩ + ContinuousMap.continuous_precomp _, ?_⟩ exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0) obtain ⟨hφ', hφ_id⟩ := this φ hφ obtain ⟨hψ', hψ_id⟩ := this ψ hψ @@ -249,7 +249,7 @@ lemma toNNReal_apply (f : C(X, ℝ)₀) (x : X) : f.toNNReal x = Real.toNNReal ( lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := by rw [continuous_induced_rng] convert_to Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1 - exact ContinuousMap.continuous_comp _ |>.comp continuous_induced_dom + exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom lemma toContinuousMapHom_toNNReal (f : C(X, ℝ)₀) : (toContinuousMapHom (X := X) (R := ℝ) f).toNNReal = @@ -401,7 +401,7 @@ instance NNReal.instUniqueNonUnitalContinuousFunctionalCalculus intro ξ' refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩ · rw [continuous_induced_rng] - exact ContinuousMap.continuous_comp_left _ |>.comp continuous_induced_dom + exact ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom · exact ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id h0) obtain ⟨hφ', hφ_id⟩ := this φ hφ obtain ⟨hψ', hψ_id⟩ := this ψ hψ diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean index b193f3c40b439..820b45e9bdb3c 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean @@ -271,7 +271,7 @@ theorem cfcHom_comp [UniqueContinuousFunctionalCalculus R A] (f : C(spectrum R a (cfcHom ha).comp <| ContinuousMap.compStarAlgHom' R R f' suffices cfcHom (cfcHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_ - · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_comp_left + · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_precomp · simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply] congr ext x diff --git a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean index faf9ab016a5e2..ff9ec26c16279 100644 --- a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean +++ b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean @@ -302,13 +302,13 @@ theorem continuous_comp [LocallyCompactSpace B] : theorem continuous_comp_left (f : ContinuousMonoidHom A B) : Continuous fun g : ContinuousMonoidHom B C => g.comp f := (inducing_toContinuousMap A C).continuous_iff.2 <| - f.toContinuousMap.continuous_comp_left.comp (inducing_toContinuousMap B C).continuous + f.toContinuousMap.continuous_precomp.comp (inducing_toContinuousMap B C).continuous @[to_additive] theorem continuous_comp_right (f : ContinuousMonoidHom B C) : Continuous fun g : ContinuousMonoidHom A B => f.comp g := (inducing_toContinuousMap A C).continuous_iff.2 <| - f.toContinuousMap.continuous_comp.comp (inducing_toContinuousMap A B).continuous + f.toContinuousMap.continuous_postcomp.comp (inducing_toContinuousMap A B).continuous variable (E) diff --git a/Mathlib/Topology/CompactOpen.lean b/Mathlib/Topology/CompactOpen.lean index 4ff883b2e49b1..8f58dc36f0245 100644 --- a/Mathlib/Topology/CompactOpen.lean +++ b/Mathlib/Topology/CompactOpen.lean @@ -78,27 +78,45 @@ lemma continuous_compactOpen {f : X → C(Y, Z)} : section Functorial /-- `C(X, ·)` is a functor. -/ -theorem continuous_comp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) := +theorem continuous_postcomp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) := continuous_compactOpen.2 fun _K hK _U hU ↦ isOpen_setOf_mapsTo hK (hU.preimage g.2) +@[deprecated (since := "2024-10-19")] alias continuous_comp := continuous_postcomp + /-- If `g : C(Y, Z)` is a topology inducing map, then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is a topology inducing map too. -/ -theorem inducing_comp (g : C(Y, Z)) (hg : Inducing g) : Inducing (g.comp : C(X, Y) → C(X, Z)) where +theorem inducing_postcomp (g : C(Y, Z)) (hg : Inducing g) : + Inducing (g.comp : C(X, Y) → C(X, Z)) where induced := by simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen, image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply] +@[deprecated (since := "2024-10-19")] alias inducing_comp := inducing_postcomp + /-- If `g : C(Y, Z)` is a topological embedding, then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is an embedding too. -/ -theorem embedding_comp (g : C(Y, Z)) (hg : Embedding g) : Embedding (g.comp : C(X, Y) → C(X, Z)) := - ⟨inducing_comp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩ +theorem embedding_postcomp (g : C(Y, Z)) (hg : Embedding g) : + Embedding (g.comp : C(X, Y) → C(X, Z)) := + ⟨inducing_postcomp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩ + +@[deprecated (since := "2024-10-19")] alias embedding_comp := embedding_postcomp /-- `C(·, Z)` is a functor. -/ -@[fun_prop] -theorem continuous_comp_left (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) := +@[continuity, fun_prop] +theorem continuous_precomp (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) := continuous_compactOpen.2 fun K hK U hU ↦ by simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU +@[deprecated (since := "2024-10-19")] alias continuous_comp_left := continuous_precomp + +variable (Z) in +/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps. +-/ +@[simps apply] +def compRightContinuousMap (f : C(X, Y)) : + C(C(Y, Z), C(X, Z)) where + toFun g := g.comp f + /-- Any pair of homeomorphisms `X ≃ₜ Z` and `Y ≃ₜ T` gives rise to a homeomorphism `C(X, Y) ≃ₜ C(Z, T)`. -/ protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) : @@ -107,8 +125,16 @@ protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) : invFun f := .comp ψ.symm <| f.comp φ left_inv f := ext fun _ ↦ ψ.left_inv (f _) |>.trans <| congrArg f <| φ.left_inv _ right_inv f := ext fun _ ↦ ψ.right_inv (f _) |>.trans <| congrArg f <| φ.right_inv _ - continuous_toFun := continuous_comp _ |>.comp <| continuous_comp_left _ - continuous_invFun := continuous_comp _ |>.comp <| continuous_comp_left _ + continuous_toFun := continuous_postcomp _ |>.comp <| continuous_precomp _ + continuous_invFun := continuous_postcomp _ |>.comp <| continuous_precomp _ + +variable (Z) in +/-- Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps. +-/ +@[deprecated Homeomorph.arrowCongr (since := "2024-10-19")] +def compRightHomeomorph (f : X ≃ₜ Y) : + C(Y, Z) ≃ₜ C(X, Z) := + .arrowCongr f.symm (.refl _) variable [LocallyCompactPair Y Z] @@ -234,7 +260,7 @@ section InfInduced /-- For any subset `s` of `X`, the restriction of continuous functions to `s` is continuous as a function from `C(X, Y)` to `C(s, Y)` with their respective compact-open topologies. -/ theorem continuous_restrict (s : Set X) : Continuous fun F : C(X, Y) => F.restrict s := - continuous_comp_left <| restrict s <| .id X + continuous_precomp <| restrict s <| .id X theorem compactOpen_le_induced (s : Set X) : (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) ≤ @@ -340,7 +366,7 @@ section Curry compact, then this is a homeomorphism, see `Homeomorph.curry`. -/ def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) where toFun a := ⟨Function.curry f a, f.continuous.comp <| by fun_prop⟩ - continuous_toFun := (continuous_comp f).comp continuous_coev + continuous_toFun := (continuous_postcomp f).comp continuous_coev @[simp] theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b) := diff --git a/Mathlib/Topology/ContinuousMap/Algebra.lean b/Mathlib/Topology/ContinuousMap/Algebra.lean index c475ae94f7dc9..c36b582bb8332 100644 --- a/Mathlib/Topology/ContinuousMap/Algebra.lean +++ b/Mathlib/Topology/ContinuousMap/Algebra.lean @@ -697,6 +697,10 @@ def ContinuousMap.compRightAlgHom {α β : Type*} [TopologicalSpace α] [Topolog map_mul' _ _ := ext fun _ ↦ rfl commutes' _ := ext fun _ ↦ rfl +theorem ContinuousMap.compRightAlgHom_continuous {α β : Type*} [TopologicalSpace α] + [TopologicalSpace β] (f : C(α, β)) : Continuous (compRightAlgHom R A f) := + continuous_precomp f + variable {A} /-- Coercion to a function as an `AlgHom`. -/ diff --git a/Mathlib/Topology/ContinuousMap/Compact.lean b/Mathlib/Topology/ContinuousMap/Compact.lean index 24fb53d8c00e8..9400fa18c4860 100644 --- a/Mathlib/Topology/ContinuousMap/Compact.lean +++ b/Mathlib/Topology/ContinuousMap/Compact.lean @@ -417,57 +417,6 @@ end CompLeft namespace ContinuousMap -/-! -We now setup variations on `compRight* f`, where `f : C(X, Y)` -(that is, precomposition by a continuous map), -as a morphism `C(Y, T) → C(X, T)`, respecting various types of structure. - -In particular: -* `compRightContinuousMap`, the bundled continuous map (for this we need `X Y` compact). -* `compRightHomeomorph`, when we precompose by a homeomorphism. -* `compRightAlgHom`, when `T = R` is a topological ring. --/ - - -section CompRight - -/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps. --/ -def compRightContinuousMap {X Y : Type*} (T : Type*) [TopologicalSpace X] [CompactSpace X] - [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : C(X, Y)) : - C(C(Y, T), C(X, T)) where - toFun g := g.comp f - continuous_toFun := by - refine Metric.continuous_iff.mpr ?_ - intro g ε ε_pos - refine ⟨ε, ε_pos, fun g' h => ?_⟩ - rw [ContinuousMap.dist_lt_iff ε_pos] at h ⊢ - exact fun x => h (f x) - -@[simp] -theorem compRightContinuousMap_apply {X Y : Type*} (T : Type*) [TopologicalSpace X] - [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : C(X, Y)) - (g : C(Y, T)) : (compRightContinuousMap T f) g = g.comp f := - rfl - -/-- Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps. --/ -def compRightHomeomorph {X Y : Type*} (T : Type*) [TopologicalSpace X] [CompactSpace X] - [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : X ≃ₜ Y) : - C(Y, T) ≃ₜ C(X, T) where - toFun := compRightContinuousMap T f - invFun := compRightContinuousMap T f.symm - left_inv g := ext fun _ => congr_arg g (f.apply_symm_apply _) - right_inv g := ext fun _ => congr_arg g (f.symm_apply_apply _) - -theorem compRightAlgHom_continuous {X Y : Type*} (R A : Type*) [TopologicalSpace X] - [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [CommSemiring R] [Semiring A] - [PseudoMetricSpace A] [TopologicalSemiring A] [Algebra R A] (f : C(X, Y)) : - Continuous (compRightAlgHom R A f) := - map_continuous (compRightContinuousMap A f) - -end CompRight - section LocalNormalConvergence /-! ### Local normal convergence @@ -476,7 +425,6 @@ A sum of continuous functions (on a locally compact space) is "locally normally sum of its sup-norms on any compact subset is summable. This implies convergence in the topology of `C(X, E)` (i.e. locally uniform convergence). -/ - open TopologicalSpace variable {X : Type*} [TopologicalSpace X] [LocallyCompactSpace X] diff --git a/Mathlib/Topology/ContinuousMap/Sigma.lean b/Mathlib/Topology/ContinuousMap/Sigma.lean index 320fd5cc4ab1f..f205d452cbc48 100644 --- a/Mathlib/Topology/ContinuousMap/Sigma.lean +++ b/Mathlib/Topology/ContinuousMap/Sigma.lean @@ -44,7 +44,7 @@ namespace ContinuousMap theorem embedding_sigmaMk_comp [Nonempty X] : Embedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where toInducing := inducing_sigma.2 - ⟨fun i ↦ (sigmaMk i).inducing_comp embedding_sigmaMk.toInducing, fun i ↦ + ⟨fun i ↦ (sigmaMk i).inducing_postcomp embedding_sigmaMk.toInducing, fun i ↦ let ⟨x⟩ := ‹Nonempty X› ⟨_, (isOpen_sigma_fst_preimage {i}).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩ inj := by diff --git a/Mathlib/Topology/ContinuousMap/Weierstrass.lean b/Mathlib/Topology/ContinuousMap/Weierstrass.lean index 8e903e39101e1..5e1edd95c1dc8 100644 --- a/Mathlib/Topology/ContinuousMap/Weierstrass.lean +++ b/Mathlib/Topology/ContinuousMap/Weierstrass.lean @@ -58,7 +58,7 @@ theorem polynomialFunctions_closure_eq_top (a b : ℝ) : compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm -- This operation is itself a homeomorphism -- (with respect to the norm topologies on continuous functions). - let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := compRightHomeomorph ℝ (iccHomeoI a b h).symm + let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _) have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl -- Thus we take the statement of the Weierstrass approximation theorem for `[0,1]`, have p := polynomialFunctions_closure_eq_top' diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean index 21ad316e36339..65ce882fec5b0 100644 --- a/Mathlib/Topology/Homotopy/HomotopyGroup.lean +++ b/Mathlib/Topology/Homotopy/HomotopyGroup.lean @@ -192,7 +192,7 @@ theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) := (continuous_eval.comp <| Continuous.prodMap (ContinuousMap.continuous_curry.comp <| - (ContinuousMap.continuous_comp_left _).comp continuous_subtype_val) + (ContinuousMap.continuous_precomp _).comp continuous_subtype_val) continuous_id) _ @@ -211,9 +211,9 @@ def fromLoop (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : Ω^ N X x := · exact GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩⟩ theorem continuous_fromLoop (i : N) : Continuous (@fromLoop N X _ x _ i) := - ((ContinuousMap.continuous_comp_left _).comp <| + ((ContinuousMap.continuous_precomp _).comp <| ContinuousMap.continuous_uncurry.comp <| - (ContinuousMap.continuous_comp _).comp continuous_induced_dom).subtype_mk + (ContinuousMap.continuous_postcomp _).comp continuous_induced_dom).subtype_mk _ theorem to_from (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : toLoop i (fromLoop i p) = p := by @@ -244,7 +244,7 @@ theorem fromLoop_apply (i : N) {p : Ω (Ω^ { j // j ≠ i } X x) const} {t : I^ /-- Composition with `Cube.insertAt` as a continuous map. -/ abbrev cCompInsert (i : N) : C(C(I^N, X), C(I × I^{ j // j ≠ i }, X)) := ⟨fun f => f.comp (Cube.insertAt i), - (toContinuousMap <| Cube.insertAt i).continuous_comp_left⟩ + (toContinuousMap <| Cube.insertAt i).continuous_precomp⟩ /-- A homotopy between `n+1`-dimensional loops `p` and `q` constant on the boundary seen as a homotopy between two paths in the space of `n`-dimensional paths. -/