feat(algebra/*/pi, topology/continuous_function/algebra): homomorphism induced by left-composition (#7984)

Given a monoid homomorphism from `α` to `β`, there is an induced monoid homomorphism from `I → α` to `I → β`, by left-composition.

Same result for semirings, modules, algebras.

Same result for topological monoids, topological semirings, etc, and the function spaces `C(I, α)`, `C(I, β)`, if the homomorphism is continuous.

Of these eight constructions, the only one I particularly want is the last one (topological algebras).  If reviewers feel it is better not to clog mathlib up with unused constructions, I am happy to cut the other seven from this PR.

Author: hrmacbeth

src/algebra/algebra/basic.lean

@@ -1537,3 +1537,19 @@ begin
 end
 
 end submodule
+
+namespace alg_hom
+
+variables {R : Type u} {A : Type v} {B : Type w} {I : Type*}
+
+variables [comm_semiring R] [semiring A] [semiring B]
+variables [algebra R A] [algebra R B]
+
+/-- `R`-algebra homomorphism between the function spaces `I → A` and `I → B`, induced by an
+`R`-algebra homomorphism `f` between `A` and `B`. -/
+@[simps] protected def comp_left (f : A →ₐ[R] B) (I : Type*) : (I → A) →ₐ[R] (I → B) :=
+{ to_fun := λ h, f ∘ h,
+  commutes' := λ c, by { ext, exact f.commutes' c },
+  .. f.to_ring_hom.comp_left I }
+
+end alg_hom

src/algebra/group/pi.lean

@@ -165,6 +165,17 @@ def monoid_hom.coe_fn (α β : Type*) [mul_one_class α] [comm_monoid β] : (α
   map_one' := rfl,
   map_mul' := λ x y, rfl, }
 
+/-- Monoid homomorphism between the function spaces `I → α` and `I → β`, induced by a monoid
+homomorphism `f` between `α` and `β`. -/
+@[to_additive "Additive monoid homomorphism between the function spaces `I → α` and `I → β`,
+induced by an additive monoid homomorphism `f` between `α` and `β`", simps]
+protected def monoid_hom.comp_left {α β : Type*} [mul_one_class α] [mul_one_class β] (f : α →* β)
+  (I : Type*) :
+  (I → α) →* (I → β) :=
+{ to_fun := λ h, f ∘ h,
+  map_one' := by ext; simp,
+  map_mul' := λ _ _, by ext; simp }
+
 end monoid_hom
 
 section single

src/algebra/ring/pi.lean

@@ -75,17 +75,28 @@ protected def ring_hom
   pi.ring_hom f g a = f a g :=
 rfl
 
+end pi
+
 section ring_hom
 
-variables [Π i, non_assoc_semiring (f i)] (f)
+universes u v
+variable {I : Type u}
 
 /-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
 homomorphism. This is `function.eval` as a `ring_hom`. -/
 @[simps]
-def eval_ring_hom (i : I) : (Π i, f i) →+* f i :=
-{ ..(eval_monoid_hom f i),
-  ..(eval_add_monoid_hom f i) }
+def pi.eval_ring_hom (f : I → Type v) [Π i, non_assoc_semiring (f i)] (i : I) :
+  (Π i, f i) →+* f i :=
+{ ..(pi.eval_monoid_hom f i),
+  ..(pi.eval_add_monoid_hom f i) }
+
+/-- Ring homomorphism between the function spaces `I → α` and `I → β`, induced by a ring
+homomorphism `f` between `α` and `β`. -/
+@[simps] protected def ring_hom.comp_left {α β : Type*} [non_assoc_semiring α]
+  [non_assoc_semiring β] (f : α →+* β) (I : Type*) :
+  (I → α) →+* (I → β) :=
+{ to_fun := λ h, f ∘ h,
+  .. f.to_monoid_hom.comp_left I,
+  .. f.to_add_monoid_hom.comp_left I }
 
 end ring_hom
-
-end pi

src/linear_algebra/bilinear_form.lean

@@ -727,7 +727,7 @@ end
 
 lemma bilin_form.to_matrix'_comp_left (B : bilin_form R₃ (n → R₃)) (f : (n → R₃) →ₗ[R₃] (n → R₃)) :
   (B.comp_left f).to_matrix' = f.to_matrix'ᵀ ⬝ B.to_matrix' :=
-by simp only [comp_left, bilin_form.to_matrix'_comp, to_matrix'_id, matrix.mul_one]
+by simp only [bilin_form.comp_left, bilin_form.to_matrix'_comp, to_matrix'_id, matrix.mul_one]
 
 lemma bilin_form.to_matrix'_comp_right (B : bilin_form R₃ (n → R₃)) (f : (n → R₃) →ₗ[R₃] (n → R₃)) :
   (B.comp_right f).to_matrix' = B.to_matrix' ⬝ f.to_matrix' :=

src/linear_algebra/pi.lean

@@ -56,7 +56,10 @@ by ext; refl
 lemma pi_comp (f : Πi, M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) : (pi f).comp g = pi (λi, (f i).comp g) :=
 rfl
 
-/-- The projections from a family of modules are linear maps. -/
+/-- The projections from a family of modules are linear maps.
+
+Note:  known here as `linear_map.proj`, this construction is in other categories called `eval`, for
+example `pi.eval_monoid_hom`, `pi.eval_ring_hom`. -/
 def proj (i : ι) : (Πi, φ i) →ₗ[R] φ i :=
 ⟨ λa, a i, assume f g, rfl, assume c f, rfl ⟩
 
@@ -74,6 +77,13 @@ begin
   exact (mem_bot _).2 (funext $ assume i, h i)
 end
 
+/-- Linear map between the function spaces `I → M₂` and `I → M₃`, induced by a linear map `f`
+between `M₂` and `M₃`. -/
+@[simps] protected def comp_left (f : M₂ →ₗ[R] M₃) (I : Type*) : (I → M₂) →ₗ[R] (I → M₃) :=
+{ to_fun := λ h, f ∘ h,
+  map_smul' := λ c h, by { ext x, exact f.map_smul' c (h x) },
+  .. f.to_add_monoid_hom.comp_left I }
+
 lemma apply_single [add_comm_monoid M] [module R M] [decidable_eq ι]
   (f : Π i, φ i →ₗ[R] M) (i j : ι) (x : φ i) :
   f j (pi.single i x j) = pi.single i (f i x) j :=

src/topology/continuous_function/algebra.lean

@@ -123,7 +123,19 @@ def coe_fn_monoid_hom {α : Type*} {β : Type*} [topological_space α] [topologi
   [monoid β] [has_continuous_mul β] : C(α, β) →* (α → β) :=
 { to_fun := coe_fn, map_one' := coe_one, map_mul' := coe_mul }
 
-/-- Composition on the right as an `monoid_hom`. Similar to `monoid_hom.comp_hom'`. -/
+/-- Composition on the left by a (continuous) homomorphism of topological monoids, as a
+`monoid_hom`. Similar to `monoid_hom.comp_left`. -/
+@[to_additive "Composition on the left by a (continuous) homomorphism of topological `add_monoid`s,
+as an `add_monoid_hom`. Similar to `add_monoid_hom.comp_left`.", simps]
+protected def _root_.monoid_hom.comp_left_continuous (α : Type*) {β : Type*} {γ : Type*}
+  [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β]
+  [topological_space γ] [monoid γ] [has_continuous_mul γ] (g : β →* γ) (hg : continuous g)  :
+  C(α, β) →* C(α, γ) :=
+{ to_fun := λ f, (⟨g, hg⟩ : C(β, γ)).comp f,
+  map_one' := ext $ λ x, g.map_one,
+  map_mul' := λ f₁ f₂, ext $ λ x, g.map_mul _ _ }
+
+/-- Composition on the right as a `monoid_hom`. Similar to `monoid_hom.comp_hom'`. -/
 @[to_additive "Composition on the right as an `add_monoid_hom`. Similar to
 `add_monoid_hom.comp_hom'`.", simps]
 def comp_monoid_hom' {α : Type*} {β : Type*} {γ : Type*}
@@ -255,6 +267,15 @@ instance {α : Type*} {β : Type*} [topological_space α]
   ..continuous_map.add_comm_group,
   ..continuous_map.comm_monoid,}
 
+/-- Composition on the left by a (continuous) homomorphism of topological rings, as a `ring_hom`.
+Similar to `ring_hom.comp_left`. -/
+@[simps] protected def _root_.ring_hom.comp_left_continuous (α : Type*) {β : Type*} {γ : Type*}
+  [topological_space α] [topological_space β] [semiring β] [topological_semiring β]
+  [topological_space γ] [semiring γ] [topological_semiring γ] (g : β →+* γ) (hg : continuous g) :
+  C(α, β) →+* C(α, γ) :=
+{ .. g.to_monoid_hom.comp_left_continuous α hg,
+  .. g.to_add_monoid_hom.comp_left_continuous α hg }
+
 /-- Coercion to a function as a `ring_hom`. -/
 @[simps]
 def coe_fn_ring_hom {α : Type*} {β : Type*} [topological_space α] [topological_space β]
@@ -307,6 +328,7 @@ namespace continuous_map
 variables {α : Type*} [topological_space α]
   {R : Type*} [semiring R] [topological_space R]
   {M : Type*} [topological_space M] [add_comm_monoid M]
+  {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂]
 
 instance
   [module R M] [has_continuous_smul R M] :
@@ -328,6 +350,7 @@ by simp
 by { ext, simp, }
 
 variables [has_continuous_add M] [module R M] [has_continuous_smul R M]
+variables [has_continuous_add M₂] [module R M₂] [has_continuous_smul R M₂]
 
 instance module : module R C(α, M) :=
 { smul     := (•),
@@ -340,6 +363,14 @@ instance module : module R C(α, M) :=
 
 variables (R)
 
+/-- Composition on the left by a continuous linear map, as a `linear_map`.
+Similar to `linear_map.comp_left`. -/
+@[simps] protected def _root_.continuous_linear_map.comp_left_continuous (α : Type*)
+  [topological_space α] (g : M →L[R] M₂) :
+  C(α, M) →ₗ[R] C(α, M₂) :=
+{ map_smul' := λ c f, ext $ λ x, g.map_smul' c _,
+  .. g.to_linear_map.to_add_monoid_hom.comp_left_continuous α g.continuous }
+
 /-- Coercion to a function as a `linear_map`. -/
 @[simps]
 def coe_fn_linear_map : C(α, M) →ₗ[R] (α → M) :=
@@ -401,6 +432,8 @@ variables {α : Type*} [topological_space α]
 {R : Type*} [comm_semiring R]
 {A : Type*} [topological_space A] [semiring A]
 [algebra R A] [topological_semiring A]
+{A₂ : Type*} [topological_space A₂] [semiring A₂]
+[algebra R A₂] [topological_semiring A₂]
 
 /-- Continuous constant functions as a `ring_hom`. -/
 def continuous_map.C : R →+* C(α, A) :=
@@ -413,7 +446,7 @@ 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 [topological_space R] [has_continuous_smul R A]
+variables [topological_space R] [has_continuous_smul R A] [has_continuous_smul R A₂]
 
 instance continuous_map.algebra : algebra R C(α, A) :=
 { to_ring_hom := continuous_map.C,
@@ -422,6 +455,14 @@ instance continuous_map.algebra : algebra R C(α, A) :=
 
 variables (R)
 
+/-- Composition on the left by a (continuous) homomorphism of topological `R`-algebras, as an
+`alg_hom`. Similar to `alg_hom.comp_left`. -/
+@[simps] protected def alg_hom.comp_left_continuous {α : Type*} [topological_space α]
+  (g : A →ₐ[R] A₂) (hg : continuous g) :
+  C(α, A) →ₐ[R] C(α, A₂) :=
+{ commutes' := λ c, continuous_map.ext $ λ _, g.commutes' _,
+  .. g.to_ring_hom.comp_left_continuous α hg }
+
 /-- Coercion to a function as an `alg_hom`. -/
 @[simps]
 def continuous_map.coe_fn_alg_hom : C(α, A) →ₐ[R] (α → A) :=