feat(algebra/group/pi): add pi.monoid_hom (#17757)

Add the `monoid` version of `pi.ring_hom`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: xroblot

src/algebra/group/pi.lean

@@ -147,6 +147,38 @@ end mul_hom
 
 section mul_hom
 
+/-- A family of mul_hom `f a : γ →ₙ* β a` defines a mul_hom `pi.mul_hom f : γ →ₙ* Π a, β a`
+given by `pi.mul_hom f x b = f b x`. -/
+@[to_additive "A family of add_hom `f a : γ → β a` defines a add_hom `pi.add_hom
+f : γ → Π a, β a` given by `pi.add_hom f x b = f b x`.", simps]
+def pi.mul_hom {γ : Type w} [Π i, has_mul (f i)] [has_mul γ]
+  (g : Π i, γ →ₙ* f i) : γ →ₙ* Π i, f i :=
+{ to_fun := λ x i, g i x,
+  map_mul' := λ x y, funext $ λ i, (g i).map_mul x y, }
+
+@[to_additive]
+lemma pi.mul_hom_injective {γ : Type w} [nonempty I]
+  [Π i, has_mul (f i)] [has_mul γ] (g : Π i, γ →ₙ* f i)
+  (hg : ∀ i, function.injective (g i)) : function.injective (pi.mul_hom g) :=
+λ x y h, let ⟨i⟩ := ‹nonempty I› in hg i ((function.funext_iff.mp h : _) i)
+
+/-- A family of monoid homomorphisms `f a : γ →* β a` defines a monoid homomorphism
+`pi.monoid_mul_hom f : γ →* Π a, β a` given by `pi.monoid_mul_hom f x b = f b x`. -/
+@[to_additive "A family of additive monoid homomorphisms `f a : γ →+ β a` defines a monoid
+homomorphism `pi.add_monoid_hom f : γ →+ Π a, β a` given by `pi.add_monoid_hom f x b
+= f b x`.", simps]
+def pi.monoid_hom {γ : Type w} [Π i, mul_one_class (f i)] [mul_one_class γ]
+  (g : Π i, γ →* f i) : γ →* Π i, f i :=
+{ to_fun := λ x i, g i x,
+  map_one' := funext $ λ i, (g i).map_one,
+  .. pi.mul_hom (λ i, (g i).to_mul_hom) }
+
+@[to_additive]
+lemma pi.monoid_hom_injective {γ : Type w} [nonempty I]
+  [Π i, mul_one_class (f i)] [mul_one_class γ] (g : Π i, γ →* f i)
+  (hg : ∀ i, function.injective (g i)) : function.injective (pi.monoid_hom g) :=
+pi.mul_hom_injective (λ i, (g i).to_mul_hom) hg
+
 variables (f) [Π i, has_mul (f i)]
 
 /-- Evaluation of functions into an indexed collection of semigroups at a point is a semigroup

src/algebra/ring/pi.lean

@@ -95,30 +95,27 @@ homomorphism `pi.non_unital_ring_hom f : γ →+* Π a, β a` given by
 protected def non_unital_ring_hom {γ : Type w} [Π i, non_unital_non_assoc_semiring (f i)]
   [non_unital_non_assoc_semiring γ] (g : Π i, γ →ₙ+* f i) : γ →ₙ+* Π i, f i :=
 { to_fun := λ x b, g b x,
-  map_add' := λ x y, funext $ λ z, map_add (g z) x y,
-  map_mul' := λ x y, funext $ λ z, map_mul (g z) x y,
-  map_zero' := funext $ λ z, map_zero (g z) }
+  .. pi.mul_hom (λ i, (g i).to_mul_hom),
+  .. pi.add_monoid_hom (λ i, (g i).to_add_monoid_hom) }
 
 lemma non_unital_ring_hom_injective {γ : Type w} [nonempty I]
   [Π i, non_unital_non_assoc_semiring (f i)] [non_unital_non_assoc_semiring γ] (g : Π i, γ →ₙ+* f i)
   (hg : ∀ i, function.injective (g i)) : function.injective (pi.non_unital_ring_hom g) :=
-λ x y h, let ⟨i⟩ := ‹nonempty I› in hg i ((function.funext_iff.mp h : _) i)
+mul_hom_injective (λ i, (g i).to_mul_hom) hg
 
 /-- A family of ring homomorphisms `f a : γ →+* β a` defines a ring homomorphism
 `pi.ring_hom f : γ →+* Π a, β a` given by `pi.ring_hom f x b = f b x`. -/
 @[simps]
 protected def ring_hom {γ : Type w} [Π i, non_assoc_semiring (f i)] [non_assoc_semiring γ]
   (g : Π i, γ →+* f i) : γ →+* Π i, f i :=
 { to_fun := λ x b, g b x,
-  map_add' := λ x y, funext $ λ z, (g z).map_add x y,
-  map_mul' := λ x y, funext $ λ z, (g z).map_mul x y,
-  map_one' := funext $ λ z, (g z).map_one,
-  map_zero' := funext $ λ z, (g z).map_zero }
+  .. pi.monoid_hom (λ i, (g i).to_monoid_hom),
+  .. pi.add_monoid_hom (λ i, (g i).to_add_monoid_hom) }
 
 lemma ring_hom_injective {γ : Type w} [nonempty I] [Π i, non_assoc_semiring (f i)]
   [non_assoc_semiring γ] (g : Π i, γ →+* f i) (hg : ∀ i, function.injective (g i)) :
   function.injective (pi.ring_hom g) :=
-λ x y h, let ⟨i⟩ := ‹nonempty I› in hg i ((function.funext_iff.mp h : _) i)
+monoid_hom_injective (λ i, (g i).to_monoid_hom) hg
 
 end pi
 

src/linear_algebra/pi.lean

@@ -39,10 +39,10 @@ variables [semiring R] [add_comm_monoid M₂] [module R M₂] [add_comm_monoid M
 
 /-- `pi` construction for linear functions. From a family of linear functions it produces a linear
 function into a family of modules. -/
-def pi (f : Πi, M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (Πi, φ i) :=
+def pi (f : Π i, M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (Π i, φ i) :=
 { to_fun := λ c i, f i c,
-  map_add' := λ c d, funext $ λ i, (f i).map_add _ _,
-  map_smul' := λ c d, funext $ λ i, (f i).map_smul _ _ }
+  map_smul' := λ c d, funext $ λ i, (f i).map_smul _ _,
+  .. pi.add_hom (λ i, (f i).to_add_hom) }
 
 @[simp] lemma pi_apply (f : Πi, M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
   pi f c i = f i c := rfl