From f9c339ecf5efb4cf0d911bb3501bd57ca2ef2507 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 20 Jun 2022 09:15:57 +0000
Subject: [PATCH] feat(group_theory/group_action/sigma): Scalar action on a
 sigma type (#14825)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`(Π i, has_scalar α (β i)) → has_scalar α (Σ i, β i)` and similar.
---
 src/group_theory/group_action/pi.lean    |  8 +++-
 src/group_theory/group_action/prod.lean  |  6 +++
 src/group_theory/group_action/sigma.lean | 58 ++++++++++++++++++++++++
 src/group_theory/group_action/sum.lean   |  6 +++
 4 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100644 src/group_theory/group_action/sigma.lean

diff --git a/src/group_theory/group_action/pi.lean b/src/group_theory/group_action/pi.lean
index 80c3950cf1936..c9463ee8976d3 100644
--- a/src/group_theory/group_action/pi.lean
+++ b/src/group_theory/group_action/pi.lean
@@ -9,7 +9,13 @@ import group_theory.group_action.defs
 /-!
 # Pi instances for multiplicative actions
 
-This file defines instances for mul_action and related structures on Pi Types
+This file defines instances for mul_action and related structures on Pi types.
+
+## See also
+
+* `group_theory.group_action.prod`
+* `group_theory.group_action.sigma`
+* `group_theory.group_action.sum`
 -/
 
 universes u v w
diff --git a/src/group_theory/group_action/prod.lean b/src/group_theory/group_action/prod.lean
index 14ee50a876e0b..a0ec0978c38fd 100644
--- a/src/group_theory/group_action/prod.lean
+++ b/src/group_theory/group_action/prod.lean
@@ -16,6 +16,12 @@ scalar multiplication as a homomorphism from `α × β` to `β`.
 
 * `smul_mul_hom`/`smul_monoid_hom`: Scalar multiplication bundled as a multiplicative/monoid
   homomorphism.
+
+## See also
+
+* `group_theory.group_action.pi`
+* `group_theory.group_action.sigma`
+* `group_theory.group_action.sum`
 -/
 
 variables {M N P α β : Type*}
diff --git a/src/group_theory/group_action/sigma.lean b/src/group_theory/group_action/sigma.lean
new file mode 100644
index 0000000000000..2e2d0b285bf1a
--- /dev/null
+++ b/src/group_theory/group_action/sigma.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import group_theory.group_action.defs
+
+/-!
+# Sigma instances for additive and multiplicative actions
+
+This file defines instances for arbitrary sum of additive and multiplicative actions.
+
+## See also
+
+* `group_theory.group_action.pi`
+* `group_theory.group_action.prod`
+* `group_theory.group_action.sum`
+-/
+
+variables {ι : Type*} {M N : Type*} {α : ι → Type*}
+
+namespace sigma
+
+section has_scalar
+variables [Π i, has_scalar M (α i)] [Π i, has_scalar N (α i)] (a : M) (i : ι) (b : α i)
+  (x : Σ i, α i)
+
+@[to_additive sigma.has_vadd] instance : has_scalar M (Σ i, α i) := ⟨λ a, sigma.map id $ λ i, (•) a⟩
+
+@[to_additive] lemma smul_def : a • x = x.map id (λ i, (•) a) := rfl
+@[simp, to_additive] lemma smul_mk : a • mk i b = ⟨i, a • b⟩ := rfl
+
+instance [has_scalar M N] [Π i, is_scalar_tower M N (α i)] : is_scalar_tower M N (Σ i, α i) :=
+⟨λ a b x, by { cases x, rw [smul_mk, smul_mk, smul_mk, smul_assoc] }⟩
+
+@[to_additive] instance [Π i, smul_comm_class M N (α i)] : smul_comm_class M N (Σ i, α i) :=
+⟨λ a b x, by { cases x, rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm] }⟩
+
+instance [Π i, has_scalar Mᵐᵒᵖ (α i)] [Π i, is_central_scalar M (α i)] :
+  is_central_scalar M (Σ i, α i) :=
+⟨λ a x, by { cases x, rw [smul_mk, smul_mk, op_smul_eq_smul] }⟩
+
+/-- This is not an instance because `i` becomes a metavariable. -/
+@[to_additive "This is not an instance because `i` becomes a metavariable."]
+protected lemma has_faithful_smul' [has_faithful_smul M (α i)] : has_faithful_smul M (Σ i, α i) :=
+⟨λ x y h, eq_of_smul_eq_smul $ λ a : α i, heq_iff_eq.1 (ext_iff.1 $ h $ mk i a).2⟩
+
+@[to_additive] instance [nonempty ι] [Π i, has_faithful_smul M (α i)] :
+  has_faithful_smul M (Σ i, α i) :=
+nonempty.elim ‹_› $ λ i, sigma.has_faithful_smul' i
+
+end has_scalar
+
+@[to_additive] instance {m : monoid M} [Π i, mul_action M (α i)] : mul_action M (Σ i, α i) :=
+{ mul_smul := λ a b x, by { cases x, rw [smul_mk, smul_mk, smul_mk, mul_smul] },
+  one_smul := λ x, by { cases x, rw [smul_mk, one_smul] } }
+
+end sigma
diff --git a/src/group_theory/group_action/sum.lean b/src/group_theory/group_action/sum.lean
index 3193abf53809d..33adaddc0456e 100644
--- a/src/group_theory/group_action/sum.lean
+++ b/src/group_theory/group_action/sum.lean
@@ -9,6 +9,12 @@ import group_theory.group_action.defs
 # Sum instances for additive and multiplicative actions
 
 This file defines instances for additive and multiplicative actions on the binary `sum` type.
+
+## See also
+
+* `group_theory.group_action.pi`
+* `group_theory.group_action.prod`
+* `group_theory.group_action.sigma`
 -/
 
 variables {M N P α β γ : Type*}