feat(group_theory/group_action/defs): add a typeclass to show that an…

… action is central (aka symmetric) (#10543)

This adds a new `is_central_scalar` typeclass to indicate that `op m • a = m • a` (or rather, to indicate that a type has the same right and left scalar action on another type).

The main instance for this is `comm_semigroup.is_central_scalar`, for when `m • a = m * a` and `op m • a = a * m`, and then all the other instances follow transitively when `has_scalar R (f M)` is derived from `has_scalar R M`:

* `prod`
* `pi`
* `ulift`
* `finsupp`
* `dfinsupp`
* `monoid_algebra`
* `add_monoid_algebra`
* `polynomial`
* `mv_polynomial`
* `matrix`
* `add_monoid_hom`
* `linear_map`
* `complex`
* `pointwise` instances on:
  * `set`
  * `submonoid`
  * `add_submonoid`
  * `subgroup`
  * `add_subgroup`
  * `subsemiring`
  * `subring`
  * `submodule`

src/algebra/module/hom.lean

@@ -41,6 +41,9 @@ instance [smul_comm_class R S B] : smul_comm_class R S (A →+ B) :=
 instance [has_scalar R S] [is_scalar_tower R S B] : is_scalar_tower R S (A →+ B) :=
 ⟨λ a b f, ext $ λ x, smul_assoc _ _ _⟩
 
+instance [distrib_mul_action Rᵐᵒᵖ B] [is_central_scalar R B] : is_central_scalar R (A →+ B) :=
+⟨λ a b, ext $ λ x, op_smul_eq_smul _ _⟩
+
 end
 
 instance [semiring R] [add_monoid A] [add_comm_monoid B] [module R B] :

src/algebra/module/linear_map.lean

@@ -635,6 +635,10 @@ instance [smul_comm_class S T M₂] : smul_comm_class S T (M →ₛₗ[σ₁₂]
 instance [has_scalar S T] [is_scalar_tower S T M₂] : is_scalar_tower S T (M →ₛₗ[σ₁₂] M₂) :=
 { smul_assoc := λ _ _ _, ext $ λ _, smul_assoc _ _ _ }
 
+instance [distrib_mul_action Sᵐᵒᵖ M₂] [smul_comm_class R₂ Sᵐᵒᵖ M₂] [is_central_scalar S M₂] :
+  is_central_scalar S (M →ₛₗ[σ₁₂] M₂) :=
+{ op_smul_eq_smul := λ a b, ext $ λ x, op_smul_eq_smul _ _ }
+
 instance : distrib_mul_action S (M →ₛₗ[σ₁₂] M₂) :=
 { one_smul := λ f, ext $ λ _, one_smul _ _,
   mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _,

src/algebra/module/submodule_pointwise.lean

@@ -68,6 +68,11 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
 
+instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ M] [smul_comm_class αᵐᵒᵖ R M]
+  [is_central_scalar α M] :
+  is_central_scalar α (submodule R M) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ linear_map.ext $ by exact op_smul_eq_smul _⟩
+
 @[simp] lemma smul_le_self_of_tower {α : Type*}
   [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M]
   (a : α) (S : submodule R M) : a • S ≤ S :=

src/algebra/module/ulift.lean

@@ -46,6 +46,10 @@ instance is_scalar_tower'' [has_scalar R M] [has_scalar M N] [has_scalar R N]
   [is_scalar_tower R M N] : is_scalar_tower R M (ulift N) :=
 ⟨λ x y z, show up ((x • y) • z.down) = ⟨x • y • z.down⟩, by rw smul_assoc⟩
 
+instance [has_scalar R M] [has_scalar Rᵐᵒᵖ M] [is_central_scalar R M] :
+  is_central_scalar R (ulift M) :=
+⟨λ r m, congr_arg up $ op_smul_eq_smul r m.down⟩
+
 instance mul_action [monoid R] [mul_action R M] :
   mul_action (ulift R) M :=
 { smul := (•),

src/algebra/monoid_algebra/basic.lean

@@ -257,6 +257,11 @@ instance [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mu
   smul_comm_class R S (monoid_algebra k G) :=
 finsupp.smul_comm_class G k
 
+instance [monoid R] [semiring k] [distrib_mul_action R k] [distrib_mul_action Rᵐᵒᵖ k]
+  [is_central_scalar R k] :
+  is_central_scalar R (monoid_algebra k G) :=
+finsupp.is_central_scalar G k
+
 instance comap_distrib_mul_action_self [group G] [semiring k] :
   distrib_mul_action G (monoid_algebra k G) :=
 finsupp.comap_distrib_mul_action_self
@@ -984,6 +989,11 @@ instance [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mu
   smul_comm_class R S (add_monoid_algebra k G) :=
 finsupp.smul_comm_class G k
 
+instance [monoid R] [semiring k] [distrib_mul_action R k] [distrib_mul_action Rᵐᵒᵖ k]
+  [is_central_scalar R k] :
+  is_central_scalar R (add_monoid_algebra k G) :=
+finsupp.is_central_scalar G k
+
 /-! It is hard to state the equivalent of `distrib_mul_action G (add_monoid_algebra k G)`
 because we've never discussed actions of additive groups. -/
 

src/algebra/pointwise.lean

@@ -564,6 +564,10 @@ instance is_scalar_tower'' {γ : Type*}
   is_scalar_tower (set α) (set β) (set γ) :=
 { smul_assoc := λ T T' T'', image2_assoc smul_assoc }
 
+instance is_central_scalar [has_scalar α β] [has_scalar αᵐᵒᵖ β] [is_central_scalar α β] :
+  is_central_scalar α (set β) :=
+⟨λ a S, congr_arg (λ f, f '' S) $ by exact funext (λ _, op_smul_eq_smul _ _)⟩
+
 section monoid
 
 /-! ### `set α` as a `(∪,*)`-semiring -/

src/data/complex/module.lean

@@ -62,6 +62,10 @@ instance [has_scalar R S] [has_scalar R ℝ] [has_scalar S ℝ] [is_scalar_tower
   is_scalar_tower R S ℂ :=
 { smul_assoc := λ r s x, by ext; simp [smul_re, smul_im, smul_assoc] }
 
+instance [has_scalar R ℝ] [has_scalar Rᵐᵒᵖ ℝ] [is_central_scalar R ℝ] :
+  is_central_scalar R ℂ :=
+{ op_smul_eq_smul := λ r x, by ext; simp [smul_re, smul_im, op_smul_eq_smul] }
+
 instance [monoid R] [mul_action R ℝ] : mul_action R ℂ :=
 { one_smul := λ x, by ext; simp [smul_re, smul_im, one_smul],
   mul_smul := λ r s x, by ext; simp [smul_re, smul_im, mul_smul] }

src/data/dfinsupp.lean

@@ -254,6 +254,11 @@ instance {δ : Type*} [monoid γ] [monoid δ]
   is_scalar_tower γ δ (Π₀ i, β i) :=
 { smul_assoc := λ r s m, ext $ λ i, by simp only [smul_apply, smul_assoc r s (m i)] }
 
+instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)]
+  [Π i, distrib_mul_action γᵐᵒᵖ (β i)] [∀ i, is_central_scalar γ (β i)] :
+  is_central_scalar γ (Π₀ i, β i) :=
+{ op_smul_eq_smul := λ r m, ext $ λ i, by simp only [smul_apply, op_smul_eq_smul r (m i)] }
+
 /-- Dependent functions with finite support inherit a `distrib_mul_action` structure from such a
 structure on each coordinate. -/
 instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)] :

src/data/finsupp/basic.lean

@@ -2300,6 +2300,10 @@ instance [monoid R] [monoid S] [add_monoid M] [distrib_mul_action R M] [distrib_
   smul_comm_class R S (α →₀ M) :=
 { smul_comm := λ r s a, ext $ λ _, smul_comm _ _ _ }
 
+instance [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M]
+  [is_central_scalar R M] : is_central_scalar R (α →₀ M) :=
+{ op_smul_eq_smul := λ r a, ext $ λ _, op_smul_eq_smul _ _ }
+
 instance [semiring R] [add_comm_monoid M] [module R M] : module R (α →₀ M) :=
 { smul      := (•),
   zero_smul := λ x, ext $ λ _, zero_smul _ _,

src/data/matrix/basic.lean

@@ -117,6 +117,8 @@ instance [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] :
   smul_comm_class R S (matrix m n α) := pi.smul_comm_class
 instance [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] :
   is_scalar_tower R S (matrix m n α) := pi.is_scalar_tower
+instance [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] :
+  is_central_scalar R (matrix m n α) := pi.is_central_scalar
 instance [monoid R] [mul_action R α] :
   mul_action R (matrix m n α) := pi.mul_action _
 instance [monoid R] [add_monoid α] [distrib_mul_action R α] :

src/data/mv_polynomial/basic.lean

@@ -119,6 +119,10 @@ instance [monoid R] [monoid S₁][comm_semiring S₂]
   [distrib_mul_action R S₂] [distrib_mul_action S₁ S₂] [smul_comm_class R S₁ S₂] :
   smul_comm_class R S₁ (mv_polynomial σ S₂) :=
 add_monoid_algebra.smul_comm_class
+instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] [distrib_mul_action Rᵐᵒᵖ S₁]
+  [is_central_scalar R S₁] :
+  is_central_scalar R (mv_polynomial σ S₁) :=
+add_monoid_algebra.is_central_scalar
 instance [comm_semiring R] [comm_semiring S₁] [algebra R S₁] : algebra R (mv_polynomial σ S₁) :=
 add_monoid_algebra.algebra
 -- TODO[gh-6025]: make this an instance once safe to do so

src/data/polynomial/basic.lean

@@ -150,6 +150,10 @@ instance {S₁ S₂} [has_scalar S₁ S₂] [monoid S₁] [monoid S₂] [distrib
   [distrib_mul_action S₂ R] [is_scalar_tower S₁ S₂ R] : is_scalar_tower S₁ S₂ (polynomial R) :=
 ⟨by { rintros _ _ ⟨⟩, simp [smul_to_finsupp] }⟩
 
+instance {S} [monoid S] [distrib_mul_action S R] [distrib_mul_action Sᵐᵒᵖ R]
+  [is_central_scalar S R] : is_central_scalar S (polynomial R) :=
+⟨by { rintros _ ⟨⟩, simp [smul_to_finsupp, op_smul_eq_smul] }⟩
+
 instance [subsingleton R] : unique (polynomial R) :=
 { uniq := by { rintros ⟨x⟩, change (⟨x⟩ : polynomial R) = 0, rw [← zero_to_finsupp], simp },
 .. polynomial.inhabited }

src/group_theory/group_action/defs.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes, Yury Kudryashov
 import algebra.group.defs
 import algebra.group.hom
 import algebra.group.type_tags
+import algebra.opposites
 import logic.embedding
 
 /-!
@@ -27,6 +28,7 @@ interaction of different group actions,
 
 * `smul_comm_class M N α` and its additive version `vadd_comm_class M N α`;
 * `is_scalar_tower M N α` (no additive version).
+* `is_central_scalar M α` (no additive version).
 
 ## Notation
 
@@ -181,6 +183,18 @@ is_scalar_tower.smul_assoc x y z
 
 instance semigroup.is_scalar_tower [semigroup α] : is_scalar_tower α α α := ⟨mul_assoc⟩
 
+/-- A typeclass indicating that the right (aka `mul_opposite`) and left actions by `M` on `α` are
+equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
+for `•`. -/
+class is_central_scalar (M α : Type*) [has_scalar M α] [has_scalar Mᵐᵒᵖ α] : Prop :=
+(op_smul_eq_smul : ∀ (m : M) (a : α), mul_opposite.op m • a = m • a)
+
+lemma is_central_scalar.unop_smul_eq_smul {M α : Type*} [has_scalar M α] [has_scalar Mᵐᵒᵖ α]
+  [is_central_scalar M α] (m : Mᵐᵒᵖ) (a : α) : (mul_opposite.unop m) • a = m • a :=
+mul_opposite.rec (by exact λ m, (is_central_scalar.op_smul_eq_smul _ _).symm) m
+
+export is_central_scalar (op_smul_eq_smul unop_smul_eq_smul)
+
 namespace has_scalar
 variables [has_scalar M α]
 

src/group_theory/group_action/opposite.lean

@@ -50,6 +50,18 @@ instance {M N} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
   smul_comm_class M N αᵐᵒᵖ :=
 ⟨λ x y z, unop_injective $ smul_comm _ _ _⟩
 
+instance (R : Type*) [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] :
+  is_central_scalar R αᵐᵒᵖ :=
+⟨λ r m, unop_injective $ op_smul_eq_smul _ _⟩
+
+lemma op_smul_eq_op_smul_op {R : Type*} [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α]
+  (r : R) (a : α) : op (r • a) = op r • op a :=
+(op_smul_eq_smul r (op a)).symm
+
+lemma unop_smul_eq_unop_smul_unop {R : Type*} [has_scalar R α] [has_scalar Rᵐᵒᵖ α]
+  [is_central_scalar R α] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) : unop (r • a) = unop r • unop a :=
+(unop_smul_eq_smul r (unop a)).symm
+
 end mul_opposite
 
 /-! ### Actions _by_ the opposite type (right actions)
@@ -83,6 +95,9 @@ instance semigroup.opposite_smul_comm_class' [semigroup α] :
   smul_comm_class α αᵐᵒᵖ α :=
 { smul_comm := λ x y z, (mul_assoc _ _ _).symm }
 
+instance comm_semigroup.is_central_scalar [comm_semigroup α] : is_central_scalar α α :=
+⟨λ r m, mul_comm _ _⟩
+
 /-- Like `monoid.to_mul_action`, but multiplies on the right. -/
 instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
 { smul := (•),

src/group_theory/group_action/pi.lean

@@ -71,6 +71,10 @@ instance smul_comm_class'' {g : I → Type*} {h : I → Type*}
   [∀ i, smul_comm_class (f i) (g i) (h i)] : smul_comm_class (Π i, f i) (Π i, g i) (Π i, h i) :=
 ⟨λ x y z, funext $ λ i, smul_comm (x i) (y i) (z i)⟩
 
+instance {α : Type*} [Π i, has_scalar α $ f i] [Π i, has_scalar αᵐᵒᵖ $ f i]
+  [∀ i, is_central_scalar α (f i)] : is_central_scalar α (Π i, f i) :=
+⟨λ r m, funext $ λ i, op_smul_eq_smul _ _⟩
+
 /-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is
 not an instance as `i` cannot be inferred. -/
 @[to_additive pi.has_faithful_vadd_at]

src/group_theory/group_action/prod.lean

@@ -35,6 +35,10 @@ instance [has_scalar M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
   smul_comm_class M N (α × β) :=
 { smul_comm := λ r s x, mk.inj_iff.mpr ⟨smul_comm _ _ _, smul_comm _ _ _⟩ }
 
+instance [has_scalar Mᵐᵒᵖ α] [has_scalar Mᵐᵒᵖ β] [is_central_scalar M α] [is_central_scalar M β] :
+  is_central_scalar M (α × β) :=
+⟨λ r m, prod.ext (op_smul_eq_smul _ _) (op_smul_eq_smul _ _)⟩
+
 @[to_additive has_faithful_vadd_left]
 instance has_faithful_scalar_left [has_faithful_scalar M α] [nonempty β] :
   has_faithful_scalar M (α × β) :=

src/group_theory/subgroup/pointwise.lean

@@ -53,6 +53,10 @@ lemma pointwise_smul_def {a : α} (S : subgroup G) :
 lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
 
+instance pointwise_central_scalar [mul_distrib_mul_action αᵐᵒᵖ G] [is_central_scalar α G] :
+  is_central_scalar α (subgroup G) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group
@@ -143,6 +147,10 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
+instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
+  is_central_scalar α (add_subgroup A) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ add_monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group

src/group_theory/submonoid/pointwise.lean

@@ -130,6 +130,10 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submonoid M) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
 
+instance pointwise_central_scalar [mul_distrib_mul_action αᵐᵒᵖ M] [is_central_scalar α M] :
+  is_central_scalar α (submonoid M) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group
@@ -220,6 +224,10 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_submonoid A) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
+instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
+  is_central_scalar α (add_submonoid A) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ add_monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group

src/ring_theory/subring/pointwise.lean

@@ -55,6 +55,10 @@ lemma pointwise_smul_def {a : M} (S : subring R) :
 lemma smul_mem_pointwise_smul (m : M) (r : R) (S : subring R) : r ∈ S → m • r ∈ m • S :=
 (set.smul_mem_smul_set : _ → _ ∈ m • (S : set R))
 
+instance pointwise_central_scalar [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
+  is_central_scalar M (subring R) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ ring_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 

src/ring_theory/subsemiring/pointwise.lean

@@ -51,6 +51,10 @@ lemma pointwise_smul_def {a : M} (S : subsemiring R) :
 lemma smul_mem_pointwise_smul (m : M) (r : R) (S : subsemiring R) : r ∈ S → m • r ∈ m • S :=
 (set.smul_mem_smul_set : _ → _ ∈ m • (S : set R))
 
+instance pointwise_central_scalar [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
+  is_central_scalar M (subsemiring R) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ ring_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group