From b68e4a899f41b91923e70404a43ce275da5ffa91 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 13 Oct 2022 15:02:26 +0000 Subject: [PATCH] refactor(topology/continuous_function/{algebra, compact}): move `continuous_map.comp_right_alg_hom` (#16875) This moves `continuous_function.comp_right_alg_hom` to a better home. Along the way, we generalize it significantly. We also provide term-mode proofs for some very slow `tidy`s, and remove some unnecessary hypotheses in `topology/continuous_function/algebra` --- src/topology/continuous_function/algebra.lean | 18 +++++++- src/topology/continuous_function/compact.lean | 43 +++++-------------- .../continuous_function/polynomial.lean | 2 +- .../continuous_function/weierstrass.lean | 2 +- 4 files changed, 29 insertions(+), 36 deletions(-) diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean index f4ac6d39dbd4d..185f38f7625c6 100644 --- a/src/topology/continuous_function/algebra.lean +++ b/src/topology/continuous_function/algebra.lean @@ -575,8 +575,6 @@ def continuous_map.C : R →+* C(α, A) := @[simp] lemma continuous_map.C_apply (r : R) (a : α) : continuous_map.C r a = algebra_map R A r := rfl -variables [has_continuous_const_smul R A] [has_continuous_const_smul R A₂] - instance continuous_map.algebra : algebra R C(α, A) := { to_ring_hom := continuous_map.C, commutes' := λ c f, by ext x; exact algebra.commutes' _ _, @@ -592,6 +590,22 @@ variables (R) { commutes' := λ c, continuous_map.ext $ λ _, g.commutes' _, .. g.to_ring_hom.comp_left_continuous α hg } +variables (A) + +/-- +Precomposition of functions into a normed ring by a continuous map is an algebra homomorphism. +-/ +@[simps] def continuous_map.comp_right_alg_hom {α β : Type*} [topological_space α] + [topological_space β] (f : C(α, β)) : C(β, A) →ₐ[R] C(α, A) := +{ to_fun := λ g, g.comp f, + map_zero' := by { ext, refl, }, + map_add' := λ g₁ g₂, by { ext, refl, }, + map_one' := by { ext, refl, }, + map_mul' := λ g₁ g₂, by { ext, refl, }, + commutes' := λ r, by { ext, refl, }, } + +variables {A} + /-- Coercion to a function as an `alg_hom`. -/ @[simps] def continuous_map.coe_fn_alg_hom : C(α, A) →ₐ[R] (α → A) := diff --git a/src/topology/continuous_function/compact.lean b/src/topology/continuous_function/compact.lean index 6d94f0acc0e9b..00929bfc10e36 100644 --- a/src/topology/continuous_function/compact.lean +++ b/src/topology/continuous_function/compact.lean @@ -363,7 +363,7 @@ section comp_right Precomposition by a continuous map is itself a continuous map between spaces of continuous maps. -/ def comp_right_continuous_map {X Y : Type*} (T : Type*) [topological_space X] [compact_space X] - [topological_space Y] [compact_space Y] [normed_add_comm_group T] + [topological_space Y] [compact_space Y] [metric_space T] (f : C(X, Y)) : C(C(Y, T), C(X, T)) := { to_fun := λ g, g.comp f, continuous_to_fun := @@ -376,7 +376,7 @@ def comp_right_continuous_map {X Y : Type*} (T : Type*) [topological_space X] [c end } @[simp] lemma comp_right_continuous_map_apply {X Y : Type*} (T : Type*) [topological_space X] - [compact_space X] [topological_space Y] [compact_space Y] [normed_add_comm_group T] + [compact_space X] [topological_space Y] [compact_space Y] [metric_space T] (f : C(X, Y)) (g : C(Y, T)) : (comp_right_continuous_map T f) g = g.comp f := rfl @@ -385,39 +385,18 @@ rfl Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps. -/ def comp_right_homeomorph {X Y : Type*} (T : Type*) [topological_space X] [compact_space X] - [topological_space Y] [compact_space Y] [normed_add_comm_group T] + [topological_space Y] [compact_space Y] [metric_space T] (f : X ≃ₜ Y) : C(Y, T) ≃ₜ C(X, T) := { to_fun := comp_right_continuous_map T f.to_continuous_map, inv_fun := comp_right_continuous_map T f.symm.to_continuous_map, - left_inv := by tidy, - right_inv := by tidy, } - -/-- -Precomposition of functions into a normed ring by continuous map is an algebra homomorphism. --/ -def comp_right_alg_hom {X Y : Type*} (R : Type*) - [topological_space X] [topological_space Y] [normed_comm_ring R] (f : C(X, Y)) : - C(Y, R) →ₐ[R] C(X, R) := -{ to_fun := λ g, g.comp f, - map_zero' := by { ext, simp, }, - map_add' := λ g₁ g₂, by { ext, simp, }, - map_one' := by { ext, simp, }, - map_mul' := λ g₁ g₂, by { ext, simp, }, - commutes' := λ r, by { ext, simp, }, } - -@[simp] lemma comp_right_alg_hom_apply {X Y : Type*} (R : Type*) - [topological_space X] [topological_space Y] [normed_comm_ring R] (f : C(X, Y)) (g : C(Y, R)) : - (comp_right_alg_hom R f) g = g.comp f := -rfl - -lemma comp_right_alg_hom_continuous {X Y : Type*} (R : Type*) - [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] - [normed_comm_ring R] (f : C(X, Y)) : - continuous (comp_right_alg_hom R f) := -begin - change continuous (comp_right_continuous_map R f), - continuity, -end + left_inv := λ g, ext $ λ _, congr_arg g (f.apply_symm_apply _), + right_inv := λ g, ext $ λ _, congr_arg g (f.symm_apply_apply _) } + +lemma comp_right_alg_hom_continuous {X Y : Type*} (R A : Type*) + [topological_space X] [compact_space X] [topological_space Y] [compact_space Y] [comm_semiring R] + [semiring A] [metric_space A] [topological_semiring A] [algebra R A] (f : C(X, Y)) : + continuous (comp_right_alg_hom R A f) := +map_continuous (comp_right_continuous_map A f) end comp_right diff --git a/src/topology/continuous_function/polynomial.lean b/src/topology/continuous_function/polynomial.lean index 04ae3993512da..e03d45c5d6e79 100644 --- a/src/topology/continuous_function/polynomial.lean +++ b/src/topology/continuous_function/polynomial.lean @@ -138,7 +138,7 @@ open continuous_map is the polynomials on `[a,b]`. -/ lemma polynomial_functions.comap_comp_right_alg_hom_Icc_homeo_I (a b : ℝ) (h : a < b) : (polynomial_functions I).comap - (comp_right_alg_hom ℝ (Icc_homeo_I a b h).symm.to_continuous_map) = + (comp_right_alg_hom ℝ ℝ (Icc_homeo_I a b h).symm.to_continuous_map) = polynomial_functions (set.Icc a b) := begin ext f, diff --git a/src/topology/continuous_function/weierstrass.lean b/src/topology/continuous_function/weierstrass.lean index 6cf001aa8dfed..f2189eb8f3659 100644 --- a/src/topology/continuous_function/weierstrass.lean +++ b/src/topology/continuous_function/weierstrass.lean @@ -58,7 +58,7 @@ begin { -- We can pullback continuous functions on `[a,b]` to continuous functions on `[0,1]`, -- by precomposing with an affine map. let W : C(set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) := - comp_right_alg_hom ℝ (Icc_homeo_I a b h).symm.to_continuous_map, + comp_right_alg_hom ℝ ℝ (Icc_homeo_I a b h).symm.to_continuous_map, -- This operation is itself a homeomorphism -- (with respect to the norm topologies on continuous functions). let W' : C(set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := comp_right_homeomorph ℝ (Icc_homeo_I a b h).symm,