feat(analysis/normed_space/basic): define inclusion `locally_constant…

… X G → C(X, G)` as various types of bundled morphism (#8448)

src/analysis/normed_space/basic.lean

@@ -9,6 +9,8 @@ import topology.algebra.group_completion
 import topology.instances.nnreal
 import topology.metric_space.completion
 import topology.sequences
+import topology.locally_constant.algebra
+import topology.continuous_function.algebra
 
 /-!
 # Normed spaces
@@ -1992,3 +1994,38 @@ instance [semi_normed_group V] : normed_group (completion V) :=
 
 end completion
 end uniform_space
+
+namespace locally_constant
+
+variables {X Y : Type*} [topological_space X] [topological_space Y] (f : locally_constant X Y)
+
+/-- The inclusion of locally-constant functions into continuous functions as a multiplicative
+monoid hom. -/
+@[to_additive "The inclusion of locally-constant functions into continuous functions as an
+additive monoid hom.", simps]
+def to_continuous_map_monoid_hom [monoid Y] [has_continuous_mul Y] :
+  locally_constant X Y →* C(X, Y) :=
+{ to_fun    := coe,
+  map_one' := by { ext, simp, },
+  map_mul'  := λ x y, by { ext, simp, }, }
+
+/-- The inclusion of locally-constant functions into continuous functions as a linear map. -/
+@[simps] def to_continuous_map_linear_map (R : Type*) [semiring R] [topological_space R]
+  [add_comm_monoid Y] [module R Y] [has_continuous_add Y] [has_continuous_smul R Y] :
+  locally_constant X Y →ₗ[R] C(X, Y) :=
+{ to_fun    := coe,
+  map_add'  := λ x y, by { ext, simp, },
+  map_smul' := λ x y, by { ext, simp, }, }
+
+/-- The inclusion of locally-constant functions into continuous functions as an algebra map. -/
+@[simps] def to_continuous_map_alg_hom (R : Type*) [comm_semiring R] [topological_space R]
+  [semiring Y] [algebra R Y] [topological_semiring Y] [has_continuous_smul R Y] :
+  locally_constant X Y →ₐ[R] C(X, Y) :=
+{ to_fun    := coe,
+  map_one'  := by { ext, simp, },
+  map_mul'  := λ x y, by { ext, simp, },
+  map_zero' := by { ext, simp, },
+  map_add'  := λ x y, by { ext, simp, },
+  commutes' := λ r, by { ext x, simp [algebra.smul_def], }, }
+
+end locally_constant

src/topology/locally_constant/algebra.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import topology.locally_constant.basic
+import topology.continuous_function.algebra
+import algebra.algebra.basic
 
 /-!
 # Algebraic structure on locally constant functions
@@ -55,6 +57,13 @@ def coe_fn_monoid_hom [mul_one_class Y] : locally_constant X Y →* (X → Y) :=
   map_one' := rfl,
   map_mul' := λ _ _, rfl }
 
+/-- The constant-function embedding, as a multiplicative monoid hom. -/
+@[to_additive "The constant-function embedding, as an additive monoid hom.", simps]
+def const_monoid_hom [mul_one_class Y] : Y →* locally_constant X Y :=
+{ to_fun   := const X,
+  map_one' := rfl,
+  map_mul' := λ _ _, rfl, }
+
 instance [mul_zero_class Y] : mul_zero_class (locally_constant X Y) :=
 { zero_mul := by { intros, ext, simp only [mul_apply, zero_apply, zero_mul] },
   mul_zero := by { intros, ext, simp only [mul_apply, zero_apply, mul_zero] },
@@ -115,6 +124,12 @@ instance [non_unital_semiring Y] : non_unital_semiring (locally_constant X Y) :=
 instance [non_assoc_semiring Y] : non_assoc_semiring (locally_constant X Y) :=
 { .. locally_constant.mul_one_class, .. locally_constant.non_unital_non_assoc_semiring }
 
+/-- The constant-function embedding, as a ring hom.  -/
+@[simps] def const_ring_hom [non_assoc_semiring Y] : Y →+* locally_constant X Y :=
+{ to_fun    := const X,
+  .. const_monoid_hom,
+  .. const_add_monoid_hom, }
+
 instance [semiring Y] : semiring (locally_constant X Y) :=
 { .. locally_constant.add_comm_monoid, .. locally_constant.monoid,
   .. locally_constant.distrib, .. locally_constant.mul_zero_class }
@@ -151,4 +166,19 @@ function.injective.distrib_mul_action coe_fn_add_monoid_hom coe_injective (λ _
 instance [semiring R] [add_comm_monoid Y] [module R Y] : module R (locally_constant X Y) :=
 function.injective.module R coe_fn_add_monoid_hom coe_injective (λ _ _, rfl)
 
+section algebra
+
+variables [comm_semiring R] [semiring Y] [algebra R Y]
+
+instance : algebra R (locally_constant X Y) :=
+{ to_ring_hom := const_ring_hom.comp $ algebra_map R Y,
+  commutes'   := by { intros, ext, exact algebra.commutes' _ _, },
+  smul_def'   := by { intros, ext, exact algebra.smul_def' _ _, }, }
+
+@[simp] lemma coe_algebra_map (r : R) :
+  ⇑(algebra_map R (locally_constant X Y) r) = algebra_map R (X → Y) r :=
+rfl
+
+end algebra
+
 end locally_constant

src/topology/locally_constant/basic.lean

@@ -250,6 +250,8 @@ def const (X : Type*) {Y : Type*} [topological_space X] (y : Y) :
   locally_constant X Y :=
 ⟨function.const X y, is_locally_constant.const _⟩
 
+@[simp] lemma coe_const (y : Y) : (const X y : X → Y) = function.const X y := rfl
+
 /-- The locally constant function to `fin 2` associated to a clopen set. -/
 def of_clopen {X : Type*} [topological_space X] {U : set X} [∀ x, decidable (x ∈ U)]
   (hU : is_clopen U) : locally_constant X (fin 2) :=