From 655c2f06a0ad597467f1a586d619e0be96b4899a Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 30 Dec 2021 08:19:12 +0000 Subject: [PATCH] chore(topology/algebra/weak_dual_topology): review (#11141) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Fix universes in `pi.has_continuous_smul`. * Add `function.injective.embedding_induced` and `weak_dual.coe_fn_embedding`. * Golf some proofs. * Review `weak_dual.module` etc instances to ensure, e.g., `module ℝ (weak_dual ℂ E)`. --- src/topology/algebra/mul_action.lean | 2 +- src/topology/algebra/weak_dual_topology.lean | 67 ++++++++++---------- src/topology/maps.lean | 6 ++ 3 files changed, 41 insertions(+), 34 deletions(-) diff --git a/src/topology/algebra/mul_action.lean b/src/topology/algebra/mul_action.lean index 5e09601c3bafc..4e3b02115e6f2 100644 --- a/src/topology/algebra/mul_action.lean +++ b/src/topology/algebra/mul_action.lean @@ -323,7 +323,7 @@ instance [topological_space β] [has_scalar M α] [has_scalar M β] [has_continu (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩ @[to_additive] -instance {ι : Type*} {γ : ι → Type} +instance {ι : Type*} {γ : ι → Type*} [∀ i, topological_space (γ i)] [Π i, has_scalar M (γ i)] [∀ i, has_continuous_smul M (γ i)] : has_continuous_smul M (Π i, γ i) := ⟨continuous_pi $ λ i, diff --git a/src/topology/algebra/weak_dual_topology.lean b/src/topology/algebra/weak_dual_topology.lean index debc6d3366826..0b803b066342c 100644 --- a/src/topology/algebra/weak_dual_topology.lean +++ b/src/topology/algebra/weak_dual_topology.lean @@ -100,6 +100,11 @@ of functionals is equipped with the topology of pointwise convergence (product t instance : topological_space (weak_dual 𝕜 E) := topological_space.induced (λ x' : weak_dual 𝕜 E, λ z : E, x' z) Pi.topological_space +/-- The coercion `coe_fn : weak_dual 𝕜 E → (E → 𝕜)` is an embedding. -/ +lemma coe_fn_embedding : + embedding (coe_fn : weak_dual 𝕜 E → (E → 𝕜)) := +by convert continuous_linear_map.coe_fn_injective.embedding_induced + lemma coe_fn_continuous : continuous (λ (x' : (weak_dual 𝕜 E)), (λ (z : E), x' z)) := continuous_induced_dom @@ -114,44 +119,40 @@ continuous_induced_rng (continuous_pi_iff.mpr h) theorem tendsto_iff_forall_eval_tendsto {γ : Type u} {F : filter γ} {ψs : γ → weak_dual 𝕜 E} {ψ : weak_dual 𝕜 E} : tendsto ψs F (𝓝 ψ) ↔ ∀ z : E, tendsto (λ i, ψs i z) F (𝓝 (ψ z)) := -begin - rw ← tendsto_pi_nhds, - split, - { intros weak_star_conv, - exact (((coe_fn_continuous 𝕜 E).tendsto ψ).comp weak_star_conv), }, - { intro h_lim_forall, - rwa [nhds_induced, tendsto_comap_iff], }, -end +by rw [← tendsto_pi_nhds, (coe_fn_embedding 𝕜 E).tendsto_nhds_iff] /-- Addition in `weak_dual 𝕜 E` is continuous. -/ instance [has_continuous_add 𝕜] : has_continuous_add (weak_dual 𝕜 E) := -{ continuous_add := begin - apply continuous_of_continuous_eval, - intros z, - have h : continuous (λ p : 𝕜 × 𝕜, p.1 + p.2) := continuous_add, - exact h.comp ((eval_continuous 𝕜 E z).prod_map (eval_continuous 𝕜 E z)), - end, } - -/-- If the scalars `𝕜` are a commutative semiring, then `weak_dual 𝕜 E` is a module over `𝕜`. -/ -instance (𝕜 : Type u) [topological_space 𝕜] [comm_semiring 𝕜] - [has_continuous_add 𝕜] [has_continuous_mul 𝕜] - (E : Type*) [topological_space E] [add_comm_group E] [module 𝕜 E] : - module 𝕜 (weak_dual 𝕜 E) := +⟨continuous_induced_rng $ ((coe_fn_continuous 𝕜 E).comp continuous_fst).add + ((coe_fn_continuous 𝕜 E).comp continuous_snd)⟩ + +/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with +multiplication on `𝕜`, then it acts on `weak_dual 𝕜 E`. -/ +instance (M : Type*) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] + [topological_space M] [has_continuous_smul M 𝕜] : + mul_action M (weak_dual 𝕜 E) := +continuous_linear_map.mul_action + +/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with +multiplication on `𝕜`, then it acts distributively on `weak_dual 𝕜 E`. -/ +instance (M : Type*) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] + [topological_space M] [has_continuous_smul M 𝕜] [has_continuous_add 𝕜] : + distrib_mul_action M (weak_dual 𝕜 E) := +continuous_linear_map.distrib_mul_action + +/-- If `𝕜` is a topological module over a semiring `R` and scalar multiplication commutes with the +multiplication on `𝕜`, then `weak_dual 𝕜 E` is a module over `R`. -/ +instance (R : Type*) [semiring R] [module R 𝕜] [smul_comm_class 𝕜 R 𝕜] + [topological_space R] [has_continuous_smul R 𝕜] [has_continuous_add 𝕜] : + module R (weak_dual 𝕜 E) := continuous_linear_map.module -/-- Scalar multiplication in `weak_dual 𝕜 E` is continuous (when `𝕜` is a commutative -semiring). -/ -instance (𝕜 : Type u) [topological_space 𝕜] [comm_semiring 𝕜] - [has_continuous_add 𝕜] [has_continuous_mul 𝕜] - (E : Type*) [topological_space E] [add_comm_group E] - [module 𝕜 E] : - has_continuous_smul 𝕜 (weak_dual 𝕜 E) := -{ continuous_smul := begin - apply continuous_of_continuous_eval, - intros z, - have h : continuous (λ p : 𝕜 × 𝕜, p.1 * p.2) := continuous_mul, - exact h.comp ((continuous_id').prod_map (eval_continuous 𝕜 E z)), - end, } +/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with +multiplication on `𝕜`, then it continuously acts on `weak_dual 𝕜 E`. -/ +instance (M : Type*) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] + [topological_space M] [has_continuous_smul M 𝕜] : + has_continuous_smul M (weak_dual 𝕜 E) := +⟨continuous_induced_rng $ continuous_fst.smul ((coe_fn_continuous 𝕜 E).comp continuous_snd)⟩ end weak_dual diff --git a/src/topology/maps.lean b/src/topology/maps.lean index 365d4ec463b70..b9f80f6d3702f 100644 --- a/src/topology/maps.lean +++ b/src/topology/maps.lean @@ -127,6 +127,12 @@ structure embedding [tα : topological_space α] [tβ : topological_space β] (f extends inducing f : Prop := (inj : function.injective f) +lemma function.injective.embedding_induced [t : topological_space β] + {f : α → β} (hf : function.injective f) : + @embedding α β (t.induced f) t f := +{ induced := rfl, + inj := hf } + variables [topological_space α] [topological_space β] [topological_space γ] lemma embedding.mk' (f : α → β) (inj : function.injective f)