feat(data/monoid_algebra): the distrib_mul_action (#2417)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Author: kim-em

src/data/finsupp.lean

@@ -918,6 +918,7 @@ def comap_domain {α₁ α₂ γ : Type*} [has_zero γ]
       exact l.mem_support_to_fun (f a),
     end }
 
+@[simp]
 lemma comap_domain_apply {α₁ α₂ γ : Type*} [has_zero γ]
   (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) (a : α₁) :
   comap_domain f l hf a = l (f a) :=
@@ -1323,7 +1324,65 @@ end
 end curry_uncurry
 
 section
+variables [group γ] [mul_action γ α] [add_comm_monoid β]
 
+/--
+Scalar multiplication by a group element g,
+given by precomposition with the action of g⁻¹ on the domain.
+-/
+def comap_has_scalar : has_scalar γ (α →₀ β) :=
+{ smul := λ g f, f.comap_domain (λ a, g⁻¹ • a)
+  (λ a a' m m' h, by simpa [←mul_smul] using (congr_arg (λ a, g • a) h)) }
+
+local attribute [instance] comap_has_scalar
+
+/--
+Scalar multiplication by a group element,
+given by precomposition with the action of g⁻¹ on the domain,
+is multiplicative in g.
+-/
+def comap_mul_action : mul_action γ (α →₀ β) :=
+{ one_smul := λ f, by { ext, dsimp [(•)], simp, },
+  mul_smul := λ g g' f, by { ext, dsimp [(•)], simp [mul_smul], }, }
+
+local attribute [instance] comap_mul_action
+
+/--
+Scalar multiplication by a group element,
+given by precomposition with the action of g⁻¹ on the domain,
+is additive in the second argument.
+-/
+def comap_distrib_mul_action :
+  distrib_mul_action γ (α →₀ β) :=
+{ smul_zero := λ g, by { ext, dsimp [(•)], simp, },
+  smul_add := λ g f f', by { ext, dsimp [(•)], simp, }, }
+
+/--
+Scalar multiplication by a group element on finitely supported functions on a group,
+given by precomposition with the action of g⁻¹. -/
+def comap_distrib_mul_action_self :
+  distrib_mul_action γ (γ →₀ β) :=
+@finsupp.comap_distrib_mul_action γ β γ _ (mul_action.regular γ) _
+
+@[simp]
+lemma comap_smul_single (g : γ) (a : α) (b : β) :
+  g • single a b = single (g • a) b :=
+begin
+  ext a',
+  dsimp [(•)],
+  by_cases h : g • a = a',
+  { subst h, simp [←mul_smul], },
+  { simp [single_eq_of_ne h], rw [single_eq_of_ne],
+    rintro rfl, simpa [←mul_smul] using h, }
+end
+
+@[simp]
+lemma comap_smul_apply (g : γ) (f : α →₀ β) (a : α) :
+  (g • f) a = f (g⁻¹ • a) := rfl
+
+end
+
+section
 instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : has_scalar γ (α →₀ β) :=
 ⟨λa v, v.map_range ((•) a) (smul_zero _)⟩
 

src/data/monoid_algebra.lean

@@ -159,6 +159,13 @@ finsupp.semimodule G k
 instance [ring k] : module k (monoid_algebra k G) :=
 finsupp.module G k
 
+instance [group G] [semiring k] :
+  distrib_mul_action G (monoid_algebra k G) :=
+finsupp.comap_distrib_mul_action_self
+
+-- TODO we should prove here that G and k commute;
+-- presumably a `linear_mul_action` typeclass is in order
+
 lemma single_mul_single [semiring k] [monoid G] {a₁ a₂ : G} {b₁ b₂ : k} :
   (single a₁ b₁ : monoid_algebra k G) * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) :=
 (sum_single_index (by simp only [_root_.zero_mul, single_zero, sum_zero])).trans
@@ -338,6 +345,9 @@ finsupp.semimodule G k
 instance [ring k] : module k (add_monoid_algebra k G) :=
 finsupp.module G k
 
+-- It is hard to state the equivalent of `distrib_mul_action G (monoid_algebra k G)`
+-- because we've never discussed actions of additive groups.
+
 lemma single_mul_single [semiring k] [add_monoid G] {a₁ a₂ : G} {b₁ b₂ : k}:
   (single a₁ b₁ : add_monoid_algebra k G) * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
 (sum_single_index (by simp only [_root_.zero_mul, single_zero, sum_zero])).trans

src/group_theory/group_action.lean

@@ -46,7 +46,15 @@ end
 
 namespace mul_action
 
-variables (α) [monoid α] [mul_action α β]
+variables (α) [monoid α]
+
+/-- The regular action of a monoid on itself by left multiplication. -/
+def regular : mul_action α α :=
+{ smul := λ a₁ a₂, a₁ * a₂,
+  one_smul := λ a, one_mul a,
+  mul_smul := λ a₁ a₂ a₃, mul_assoc _ _ _, }
+
+variables [mul_action α β]
 
 def orbit (b : β) := set.range (λ x : α, x • b)