feat(algebra/monoid_algebra): adjointness for the functor `G ↦ monoid…

…_algebra k G` when `G` carries only `has_mul` (#7932)




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

src/algebra/group_action_hom.lean

@@ -69,6 +69,8 @@ f.map_smul' m x
 theorem ext_iff {f g : X →[M'] Y} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ H x, by rw H, ext⟩
 
+protected lemma congr_fun {f g : X →[M'] Y} (h : f = g) (x : X) : f x = g x := h ▸ rfl
+
 variables (M M') {X}
 
 /-- The identity map as an equivariant map. -/
@@ -150,6 +152,16 @@ variables {M A B}
 theorem ext_iff {f g : A →+[M] B} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ H x, by rw H, ext⟩
 
+protected lemma congr_fun {f g : A →+[M] B} (h : f = g) (x : A) : f x = g x := h ▸ rfl
+
+lemma to_mul_action_hom_injective {f g : A →+[M] B}
+  (h : (f : A →[M] B) = (g : A →[M] B)) : f = g :=
+by { ext a, exact mul_action_hom.congr_fun h a, }
+
+lemma to_add_monoid_hom_injective {f g : A →+[M] B}
+  (h : (f : A →+ B) = (g : A →+ B)) : f = g :=
+by { ext a, exact add_monoid_hom.congr_fun h a, }
+
 @[simp] lemma map_zero (f : A →+[M] B) : f 0 = 0 :=
 f.map_zero'
 
@@ -212,6 +224,19 @@ ext $ λ x, by rw [comp_apply, id_apply]
   .. (f : A →+ B).inverse g h₁ h₂,
   .. (f : A →[M] B).inverse g h₁ h₂ }
 
+section semiring
+
+variables {R M'} [add_monoid M'] [distrib_mul_action R M']
+
+@[ext] lemma ext_ring
+  {f g : R →+[R] M'} (h : f 1 = g 1) : f = g :=
+by { ext x, rw [← mul_one x, ← smul_eq_mul R, f.map_smul, g.map_smul, h], }
+
+lemma ext_ring_iff {f g : R →+[R] M'} : f = g ↔ f 1 = g 1 :=
+⟨λ h, h ▸ rfl, ext_ring⟩
+
+end semiring
+
 end distrib_mul_action_hom
 
 /-- Equivariant ring homomorphisms. -/

src/algebra/module/linear_map.lean

@@ -286,6 +286,29 @@ end add_comm_group
 
 end linear_map
 
+namespace distrib_mul_action_hom
+
+variables [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂]
+
+/-- A `distrib_mul_action_hom` between two modules is a linear map. -/
+def to_linear_map (f : M →+[R] M₂) : M →ₗ[R] M₂ := { ..f }
+
+instance : has_coe (M →+[R] M₂) (M →ₗ[R] M₂) := ⟨to_linear_map⟩
+
+@[simp] lemma to_linear_map_eq_coe (f : M →+[R] M₂) :
+  f.to_linear_map = ↑f :=
+rfl
+
+@[simp, norm_cast] lemma coe_to_linear_map (f : M →+[R] M₂) :
+  ((f : M →ₗ[R] M₂) : M → M₂) = f :=
+rfl
+
+lemma to_linear_map_injective {f g : M →+[R] M₂} (h : (f : M →ₗ[R] M₂) = (g : M →ₗ[R] M₂)) :
+  f = g :=
+by { ext m, exact linear_map.congr_fun h m, }
+
+end distrib_mul_action_hom
+
 namespace is_linear_map
 
 section add_comm_monoid

src/algebra/monoid_algebra.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 import algebra.algebra.basic
 import algebra.big_operators.finsupp
 import linear_algebra.finsupp
+import algebra.non_unital_alg_hom
 
 /-!
 # Monoid algebras
@@ -15,6 +16,12 @@ a convolution product. To mathematicians this structure is known as the "monoid
 i.e. the finite formal linear combinations over a given semiring of elements of the monoid.
 The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.
 
+In fact the construction of the "monoid algebra" makes sense when `G` is not even a monoid, but
+merely a magma, i.e., when `G` carries a multiplication which is not required to satisfy any
+conditions at all. In this case the construction yields a not-necessarily-unital,
+not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such
+algebras to magmas, and we prove this as `monoid_algebra.lift_magma`.
+
 In this file we define `monoid_algebra k G := G →₀ k`, and `add_monoid_algebra k G`
 in the same way, and then define the convolution product on these.
 
@@ -82,7 +89,7 @@ instance : non_unital_non_assoc_semiring (monoid_algebra k G) :=
   add           := (+),
   left_distrib  := assume f g h, by simp only [mul_def, sum_add_index, mul_add, mul_zero,
     single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add],
-  right_distrib := assume f g h, by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul,
+  right_distrib := assume f g h, by simp only [mul_def, sum_add_index, add_mul, zero_mul,
     single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero,
     sum_add],
   zero_mul  := assume f, by simp only [mul_def, sum_zero_index],
@@ -315,18 +322,21 @@ begin
   { simp [add_mul] }
 end
 
-variables (k G) [mul_one_class G]
+variables (k G)
+
+/-- The embedding of a magma into its magma algebra. -/
+@[simps] def of_magma [has_mul G] : mul_hom G (monoid_algebra k G) :=
+{ to_fun   := λ a, single a 1,
+  map_mul' := λ a b, by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero], }
 
-/-- Embedding of a monoid into its monoid algebra. -/
-def of : G →* monoid_algebra k G :=
+/-- The embedding of a unital magma into its magma algebra. -/
+@[simps] def of [mul_one_class G] : G →* monoid_algebra k G :=
 { to_fun := λ a, single a 1,
   map_one' := rfl,
-  map_mul' := λ a b, by rw [single_mul_single, one_mul] }
+  .. of_magma k G }
 
 end
 
-@[simp] lemma of_apply [mul_one_class G] (a : G) : of k G a = single a 1 := rfl
-
 lemma of_injective [mul_one_class G] [nontrivial k] : function.injective (of k G) :=
 λ a b h, by simpa using (single_eq_single_iff _ _ _ _).mp h
 
@@ -373,6 +383,86 @@ end
 
 end misc_theorems
 
+/-! #### Non-unital, non-associative algebra structure -/
+section non_unital_non_assoc_algebra
+
+variables {R : Type*} (k) [semiring R] [semiring k] [distrib_mul_action R k] [has_mul G]
+
+instance is_scalar_tower_self [is_scalar_tower R k k] :
+  is_scalar_tower R (monoid_algebra k G) (monoid_algebra k G) :=
+⟨λ t a b,
+begin
+  ext m,
+  simp only [mul_apply, finsupp.smul_sum, smul_ite, smul_mul_assoc, sum_smul_index', zero_mul,
+     if_t_t, implies_true_iff, eq_self_iff_true, sum_zero, coe_smul, smul_eq_mul, pi.smul_apply,
+     smul_zero],
+end⟩
+
+/-- Note that if `k` is a `comm_semiring` then we have `smul_comm_class k k k` and so we can take
+`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
+also commute with the algebra multiplication. -/
+instance smul_comm_class_self [smul_comm_class R k k] :
+  smul_comm_class R (monoid_algebra k G) (monoid_algebra k G) :=
+⟨λ t a b,
+begin
+  ext m,
+  simp only [mul_apply, finsupp.sum, finset.smul_sum, smul_ite, mul_smul_comm, sum_smul_index',
+    implies_true_iff, eq_self_iff_true, coe_smul, ite_eq_right_iff, smul_eq_mul, pi.smul_apply,
+    mul_zero, smul_zero],
+end⟩
+
+instance smul_comm_class_symm_self [smul_comm_class k R k] :
+  smul_comm_class (monoid_algebra k G) R (monoid_algebra k G) :=
+⟨λ t a b, by { haveI := smul_comm_class.symm k R k, rw ← smul_comm, } ⟩
+
+variables {A : Type u₃} [non_unital_non_assoc_semiring A]
+
+/-- A non_unital `k`-algebra homomorphism from `monoid_algebra k G` is uniquely defined by its
+values on the functions `single a 1`. -/
+lemma non_unital_alg_hom_ext [distrib_mul_action k A]
+  {φ₁ φ₂ : non_unital_alg_hom k (monoid_algebra k G) A}
+  (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
+non_unital_alg_hom.to_distrib_mul_action_hom_injective $
+  finsupp.distrib_mul_action_hom_ext' $
+  λ a, distrib_mul_action_hom.ext_ring (h a)
+
+/-- See note [partially-applied ext lemmas]. -/
+@[ext] lemma non_unital_alg_hom_ext' [distrib_mul_action k A]
+  {φ₁ φ₂ : non_unital_alg_hom k (monoid_algebra k G) A}
+  (h : φ₁.to_mul_hom.comp (of_magma k G) = φ₂.to_mul_hom.comp (of_magma k G)) : φ₁ = φ₂ :=
+non_unital_alg_hom_ext k $ mul_hom.congr_fun h
+
+/-- The functor `G ↦ monoid_algebra k G`, from the category of magmas to the category of non-unital,
+non-associative algebras over `k` is adjoint to the forgetful functor in the other direction. -/
+@[simps] def lift_magma [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] :
+  mul_hom G A ≃ non_unital_alg_hom k (monoid_algebra k G) A :=
+{ to_fun    := λ f,
+    { to_fun    := λ a, a.sum (λ m t, t • f m),
+      map_smul' :=  λ t' a,
+        begin
+          rw [finsupp.smul_sum, sum_smul_index'],
+          { simp_rw smul_assoc, },
+          { intros m, exact zero_smul k (f m), },
+        end,
+      map_mul'  := λ a₁ a₂,
+        begin
+          let g : G → k → A := λ m t, t • f m,
+          have h₁ : ∀ m, g m 0 = 0, { intros, exact zero_smul k (f m), },
+          have h₂ : ∀ m (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂, { intros, rw ← add_smul, },
+          simp_rw [finsupp.mul_sum, finsupp.sum_mul, smul_mul_smul, ← f.map_mul, mul_def,
+            sum_comm a₂ a₁, sum_sum_index h₁ h₂, sum_single_index (h₁ _)],
+        end,
+      .. lift_add_hom (λ x, (smul_add_hom k A).flip (f x)) },
+  inv_fun   := λ F, F.to_mul_hom.comp (of_magma k G),
+  left_inv  := λ f, by { ext m, simp only [non_unital_alg_hom.coe_mk, of_magma_apply,
+    non_unital_alg_hom.to_mul_hom_eq_coe, sum_single_index, function.comp_app, one_smul, zero_smul,
+    mul_hom.coe_comp, non_unital_alg_hom.coe_to_mul_hom], },
+  right_inv := λ F, by { ext m, simp only [non_unital_alg_hom.coe_mk, of_magma_apply,
+    non_unital_alg_hom.to_mul_hom_eq_coe, sum_single_index, function.comp_app, one_smul, zero_smul,
+    mul_hom.coe_comp, non_unital_alg_hom.coe_to_mul_hom], }, }
+
+end non_unital_non_assoc_algebra
+
 /-! #### Algebra structure -/
 section algebra
 
@@ -882,13 +972,18 @@ section
 
 variables (k G)
 
-/-- Embedding of a monoid into its monoid algebra. -/
+/-- The embedding of an additive magma into its additive magma algebra. -/
+@[simps] def of_magma [has_add G] : mul_hom (multiplicative G) (add_monoid_algebra k G) :=
+{ to_fun   := λ a, single a 1,
+  map_mul' := λ a b, by simpa only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero], }
+
+/-- Embedding of a magma with zero into its magma algebra. -/
 def of [add_zero_class G] : multiplicative G →* add_monoid_algebra k G :=
 { to_fun := λ a, single a 1,
   map_one' := rfl,
-  map_mul' := λ a b, by { rw [single_mul_single, one_mul], refl } }
+  .. of_magma k G }
 
-/-- Embedding of a monoid into its monoid algebra, having `G` as source. -/
+/-- Embedding of a magma with zero `G`, into its magma algebra, having `G` as source. -/
 def of' : G → add_monoid_algebra k G := λ a, single a 1
 
 end
@@ -996,6 +1091,54 @@ namespace add_monoid_algebra
 
 variables {k G}
 
+/-! #### Non-unital, non-associative algebra structure -/
+
+section non_unital_non_assoc_algebra
+
+variables {R : Type*} (k) [semiring R] [semiring k] [distrib_mul_action R k] [has_add G]
+
+instance is_scalar_tower_self [is_scalar_tower R k k] :
+  is_scalar_tower R (add_monoid_algebra k G) (add_monoid_algebra k G) :=
+@monoid_algebra.is_scalar_tower_self k (multiplicative G) R _ _ _ _ _
+
+/-- Note that if `k` is a `comm_semiring` then we have `smul_comm_class k k k` and so we can take
+`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
+also commute with the algebra multiplication. -/
+instance smul_comm_class_self [smul_comm_class R k k] :
+  smul_comm_class R (add_monoid_algebra k G) (add_monoid_algebra k G) :=
+@monoid_algebra.smul_comm_class_self k (multiplicative G) R _ _ _ _ _
+
+instance smul_comm_class_symm_self [smul_comm_class k R k] :
+  smul_comm_class (add_monoid_algebra k G) R (add_monoid_algebra k G) :=
+@monoid_algebra.smul_comm_class_symm_self k (multiplicative G) R _ _ _ _ _
+
+variables {A : Type u₃} [non_unital_non_assoc_semiring A]
+
+/-- A non_unital `k`-algebra homomorphism from `add_monoid_algebra k G` is uniquely defined by its
+values on the functions `single a 1`. -/
+lemma non_unital_alg_hom_ext [distrib_mul_action k A]
+  {φ₁ φ₂ : non_unital_alg_hom k (add_monoid_algebra k G) A}
+  (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
+@monoid_algebra.non_unital_alg_hom_ext k (multiplicative G) _ _ _ _ _ φ₁ φ₂ h
+
+/-- See note [partially-applied ext lemmas]. -/
+@[ext] lemma non_unital_alg_hom_ext' [distrib_mul_action k A]
+  {φ₁ φ₂ : non_unital_alg_hom k (add_monoid_algebra k G) A}
+  (h : φ₁.to_mul_hom.comp (of_magma k G) = φ₂.to_mul_hom.comp (of_magma k G)) : φ₁ = φ₂ :=
+@monoid_algebra.non_unital_alg_hom_ext' k (multiplicative G) _ _ _ _ _ φ₁ φ₂ h
+
+/-- The functor `G ↦ add_monoid_algebra k G`, from the category of magmas to the category of
+non-unital, non-associative algebras over `k` is adjoint to the forgetful functor in the other
+direction. -/
+@[simps] def lift_magma [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] :
+  mul_hom (multiplicative G) A ≃ non_unital_alg_hom k (add_monoid_algebra k G) A :=
+{ to_fun := λ f, { to_fun := λ a, sum a (λ m t, t • f (multiplicative.of_add m)),
+                   .. (monoid_algebra.lift_magma k f : _)},
+  inv_fun := λ F, F.to_mul_hom.comp (of_magma k G),
+  .. (monoid_algebra.lift_magma k : mul_hom (multiplicative G) A ≃ non_unital_alg_hom k _ A) }
+
+end non_unital_non_assoc_algebra
+
 /-! #### Algebra structure -/
 section algebra
 

src/algebra/non_unital_alg_hom.lean

@@ -57,11 +57,9 @@ structure non_unital_alg_hom [monoid R]
 attribute [nolint doc_blame] non_unital_alg_hom.to_distrib_mul_action_hom
 attribute [nolint doc_blame] non_unital_alg_hom.to_mul_hom
 
-initialize_simps_projections non_unital_alg_hom (to_fun → apply)
-
 namespace non_unital_alg_hom
 
-variables {R A B C} [semiring R]
+variables {R A B C} [monoid R]
 variables [non_unital_non_assoc_semiring A] [distrib_mul_action R A]
 variables [non_unital_non_assoc_semiring B] [distrib_mul_action R B]
 variables [non_unital_non_assoc_semiring C] [distrib_mul_action R C]
@@ -71,6 +69,8 @@ instance : has_coe_to_fun (non_unital_alg_hom R A B) := ⟨_, to_fun⟩
 
 @[simp] lemma to_fun_eq_coe (f : non_unital_alg_hom R A B) : f.to_fun = ⇑f := rfl
 
+initialize_simps_projections non_unital_alg_hom (to_fun → apply)
+
 lemma coe_injective :
   @function.injective (non_unital_alg_hom R A B) (A → B) coe_fn :=
 by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr
@@ -109,6 +109,14 @@ rfl
   ((f : mul_hom A B) : A → B) = f :=
 rfl
 
+lemma to_distrib_mul_action_hom_injective {f g : non_unital_alg_hom R A B}
+  (h : (f : A →+[R] B) = (g : A →+[R] B)) : f = g :=
+by { ext a, exact distrib_mul_action_hom.congr_fun h a, }
+
+lemma to_mul_hom_injective {f g : non_unital_alg_hom R A B}
+  (h : (f : mul_hom A B) = (g : mul_hom A B)) : f = g :=
+by { ext a, exact mul_hom.congr_fun h a, }
+
 @[norm_cast] lemma coe_distrib_mul_action_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) :
   ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A →+[R] B) =
   ⟨f, h₁, h₂, h₃⟩ :=

src/data/finsupp/basic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Scott Morrison
 -/
 import data.finset.preimage
 import algebra.indicator_function
+import algebra.group_action_hom
 
 /-!
 # Type of functions with finite support
@@ -2172,6 +2173,33 @@ instance [semiring R] [add_comm_monoid M] [module R M] {ι : Type*}
 ⟨λ c f h, or_iff_not_imp_left.mpr (λ hc, finsupp.ext
   (λ i, (smul_eq_zero.mp (finsupp.ext_iff.mp h i)).resolve_left hc))⟩
 
+section distrib_mul_action_hom
+
+variables [semiring R]
+variables [add_comm_monoid M] [add_comm_monoid N] [distrib_mul_action R M] [distrib_mul_action R N]
+
+/-- `finsupp.single` as a `distrib_mul_action_hom`.
+
+See also `finsupp.lsingle` for the version as a linear map. -/
+def distrib_mul_action_hom.single (a : α) : M →+[R] (α →₀ M) :=
+{ map_smul' :=
+    λ k m, by simp only [add_monoid_hom.to_fun_eq_coe, single_add_hom_apply, smul_single],
+  .. single_add_hom a }
+
+lemma distrib_mul_action_hom_ext {f g : (α →₀ M) →+[R] N}
+  (h : ∀ (a : α) (m : M), f (single a m) = g (single a m)) :
+  f = g :=
+distrib_mul_action_hom.to_add_monoid_hom_injective $ add_hom_ext h
+
+/-- See note [partially-applied ext lemmas]. -/
+@[ext] lemma distrib_mul_action_hom_ext' {f g : (α →₀ M) →+[R] N}
+  (h : ∀ (a : α), f.comp (distrib_mul_action_hom.single a) =
+                  g.comp (distrib_mul_action_hom.single a)) :
+  f = g :=
+distrib_mul_action_hom_ext $ λ a, distrib_mul_action_hom.congr_fun (h a)
+
+end distrib_mul_action_hom
+
 section
 variables [has_zero R]