chore: move MulDistribMulAction under Algebra.Group

Mathlib.lean

@@ -270,6 +270,7 @@ import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Action.Equidecomp
 import Mathlib.Algebra.Group.Action.Faithful
+import Mathlib.Algebra.Group.Action.Hom
 import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Action.Option
 import Mathlib.Algebra.Group.Action.Pi

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.Module.NatInt

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.Finprod
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Algebra.GroupWithZero.Action.Defs
-import Mathlib.Algebra.Order.Group.Multiset
-import Mathlib.Data.Finset.Basic
+import Mathlib.Algebra.Group.Action.Basic
 
 /-!
 # Lemmas about group actions on big operators

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -564,8 +564,8 @@ protected def counit' : coextendScalars f ⋙ restrictScalars f ⟶ 𝟭 (Module
         dsimp
         rw [CoextendScalars.smul_apply, one_mul, ← LinearMap.map_smul]
         congr
-        change f r = (f r) • (1 : S)
-        rw [smul_eq_mul (a := f r) (a' := 1), mul_one] }
+        change f r = f r • (1 : S)
+        rw [smul_eq_mul (f r) 1, mul_one] }
 
 end RestrictionCoextensionAdj
 

Mathlib/Algebra/GradedMonoid.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.BigOperators.Group.List.Lemmas
-import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Action.Hom
 import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Data.List.FinRange
 import Mathlib.Data.SetLike.Basic

Mathlib/Algebra/Group/Action/Basic.lean

@@ -5,7 +5,6 @@ Authors: Chris Hughes
 -/
 import Mathlib.Algebra.Group.Action.Units
 import Mathlib.Algebra.Group.Invertible.Basic
-import Mathlib.GroupTheory.Perm.Basic
 
 /-!
 # More lemmas about group actions
@@ -16,7 +15,7 @@ This file contains lemmas about group actions that require more imports than
 
 assert_not_exists MonoidWithZero
 
-variable {α β : Type*}
+variable {M N α β : Type*}
 
 section MulAction
 
@@ -38,21 +37,54 @@ lemma MulAction.toPerm_injective [FaithfulSMul α β] :
     Function.Injective (MulAction.toPerm : α → Equiv.Perm β) :=
   (show Function.Injective (Equiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp
 
-variable (α) (β)
+section
+variable [Monoid M] [MulAction M α]
+
+/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
+
+See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
+-/
+@[to_additive
+"Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`."]
+abbrev Function.Surjective.mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S]
+    [SMul S M] (f : R →* S) (hf : Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) :
+    MulAction S M where
+  smul := (· • ·)
+  one_smul b := by rw [← f.map_one, hsmul, one_smul]
+  mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]
+
+namespace MulAction
+
+variable (α)
+
+/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
+a multiplicative action of `N` on `α`.
+
+See note [reducible non-instances]. -/
+@[to_additive]
+abbrev compHom [Monoid N] (g : N →* M) : MulAction N α where
+  smul := SMul.comp.smul g
+  -- Porting note: was `by simp [g.map_one, MulAction.one_smul]`
+  one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
+  -- Porting note: was `by simp [g.map_mul, MulAction.mul_smul]`
+  mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..
+
+/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
+an additive action of `N` on `α`.
+
+See note [reducible non-instances]. -/
+add_decl_doc AddAction.compHom
+
+@[to_additive]
+lemma compHom_smul_def
+    {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
+    letI : MulAction E G := MulAction.compHom _ f
+    a • x = (f a) • x := rfl
+
+end MulAction
+end
 
-/-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
-@[simps]
-def MulAction.toPermHom : α →* Equiv.Perm β where
-  toFun := MulAction.toPerm
-  map_one' := Equiv.ext <| one_smul α
-  map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : α) u₂
-
-/-- Given an action of an additive group `α` on a set `β`, each `g : α` defines a permutation of
-`β`. -/
-@[simps!]
-def AddAction.toPermHom (α : Type*) [AddGroup α] [AddAction α β] :
-    α →+ Additive (Equiv.Perm β) :=
-  MonoidHom.toAdditive'' <| MulAction.toPermHom (Multiplicative α) β
+variable (α) (β)
 
 /-- The tautological action by `Equiv.Perm α` on `α`.
 

Mathlib/Algebra/Group/Action/Defs.lean

@@ -57,8 +57,23 @@ variable {M N G H α β γ δ : Type*}
 @[to_additive "See also `AddMonoid.toAddAction`"]
 instance (priority := 910) Mul.toSMul (α : Type*) [Mul α] : SMul α α := ⟨(· * ·)⟩
 
+/-- Like `Mul.toSMul`, but multiplies on the right.
+
+See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`. -/
+@[to_additive "Like `Add.toVAdd`, but adds on the right.
+
+  See also `AddMonoid.toOppositeAddAction`."]
+instance (priority := 910) Mul.toSMulMulOpposite (α : Type*) [Mul α] : SMul αᵐᵒᵖ α where
+  smul a b := b * a.unop
+
+@[to_additive (attr := simp)]
+lemma smul_eq_mul {α : Type*} [Mul α] (a b : α) : a • b = a * b := rfl
+
+@[to_additive]
+lemma op_smul_eq_mul {α : Type*} [Mul α] (a b : α) : MulOpposite.op a • b = b * a := rfl
+
 @[to_additive (attr := simp)]
-lemma smul_eq_mul (α : Type*) [Mul α] {a a' : α} : a • a' = a * a' := rfl
+lemma MulOpposite.smul_eq_mul_unop [Mul α] (a : αᵐᵒᵖ) (b : α) : a • b = b * a.unop := rfl
 
 /-- Type class for additive monoid actions. -/
 class AddAction (G : Type*) (P : Type*) [AddMonoid G] extends VAdd G P where
@@ -485,3 +500,22 @@ lemma SMulCommClass.of_mul_smul_one {M N} [Monoid N] [SMul M N]
   ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩
 
 end CompatibleScalar
+
+/-- Typeclass for multiplicative actions on multiplicative structures. This generalizes
+conjugation actions. -/
+@[ext]
+class MulDistribMulAction (M N : Type*) [Monoid M] [Monoid N] extends MulAction M N where
+  /-- Distributivity of `•` across `*` -/
+  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
+  /-- Multiplying `1` by a scalar gives `1` -/
+  smul_one : ∀ r : M, r • (1 : N) = 1
+
+export MulDistribMulAction (smul_one)
+
+section MulDistribMulAction
+variable [Monoid M] [Monoid N] [MulDistribMulAction M N]
+
+lemma smul_mul' (a : M) (b₁ b₂ : N) : a • (b₁ * b₂) = a • b₁ * a • b₂ :=
+  MulDistribMulAction.smul_mul ..
+
+end MulDistribMulAction

Mathlib/Algebra/Group/Action/End.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.Defs
+import Mathlib.Algebra.Group.Equiv.Defs
 import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.GroupTheory.Perm.Basic
 
 /-!
 # Endomorphisms, homomorphisms and group actions
@@ -31,52 +33,7 @@ assert_not_exists MonoidWithZero
 
 open Function (Injective Surjective)
 
-variable {M N α : Type*}
-
-section
-variable [Monoid M] [MulAction M α]
-
-/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
-
-See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
--/
-@[to_additive
-"Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`."]
-abbrev Function.Surjective.mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S]
-    [SMul S M] (f : R →* S) (hf : Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) :
-    MulAction S M where
-  smul := (· • ·)
-  one_smul b := by rw [← f.map_one, hsmul, one_smul]
-  mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]
-
-namespace MulAction
-
-variable (α)
-
-/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
-a multiplicative action of `N` on `α`.
-
-See note [reducible non-instances]. -/
-@[to_additive]
-abbrev compHom [Monoid N] (g : N →* M) : MulAction N α where
-  smul := SMul.comp.smul g
-  one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
-  mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..
-
-/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
-an additive action of `N` on `α`.
-
-See note [reducible non-instances]. -/
-add_decl_doc AddAction.compHom
-
-@[to_additive]
-lemma compHom_smul_def
-    {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
-    letI : MulAction E G := MulAction.compHom _ f
-    a • x = (f a) • x := rfl
-
-end MulAction
-end
+variable {G M N O α : Type*}
 
 section CompatibleScalar
 
@@ -105,8 +62,7 @@ def monoidHomEquivMulActionIsScalarTower (M N) [Monoid M] [Monoid N] :
 
 end CompatibleScalar
 
-variable (α)
-
+variable (α) in
 /-- The monoid of endomorphisms.
 
 Note that this is generalized by `CategoryTheory.End` to categories other than `Type u`. -/
@@ -123,8 +79,6 @@ instance : Monoid (Function.End α) where
 
 instance : Inhabited (Function.End α) := ⟨1⟩
 
-variable {α}
-
 /-- The tautological action by `Function.End α` on `α`.
 
 This is generalized to bundled endomorphisms by:
@@ -144,6 +98,9 @@ instance Function.End.applyMulAction : MulAction (Function.End α) α where
   one_smul _ := rfl
   mul_smul _ _ _ := rfl
 
+/-- The tautological additive action by `Additive (Function.End α)` on `α`. -/
+instance Function.End.applyAddAction : AddAction (Additive (Function.End α)) α := inferInstance
+
 @[simp] lemma Function.End.smul_def (f : Function.End α) (a : α) : f • a = f a := rfl
 
 --TODO - This statement should be somethting like `toFun (f * g) = toFun f ∘ toFun g`
@@ -152,6 +109,10 @@ lemma Function.End.mul_def (f g : Function.End α) : (f * g) = f ∘ g := rfl
 --TODO - This statement should be somethting like `toFun 1 = id`
 lemma Function.End.one_def : (1 : Function.End α) = id := rfl
 
+/-- `Function.End.applyMulAction` is faithful. -/
+instance Function.End.apply_FaithfulSMul : FaithfulSMul (Function.End α) α where
+  eq_of_smul_eq_smul := funext
+
 /-- The monoid hom representing a monoid action.
 
 When `M` is a group, see `MulAction.toPermHom`. -/
@@ -160,8 +121,88 @@ def MulAction.toEndHom [Monoid M] [MulAction M α] : M →* Function.End α wher
   map_one' := funext (one_smul M)
   map_mul' x y := funext (mul_smul x y)
 
+/-- The additive monoid hom representing an additive monoid action.
+
+When `M` is a group, see `AddAction.toPermHom`. -/
+def AddAction.toEndHom [AddMonoid M] [AddAction M α] : M →+ Additive (Function.End α) :=
+  MonoidHom.toAdditive'' MulAction.toEndHom
+
 /-- The monoid action induced by a monoid hom to `Function.End α`
 
 See note [reducible non-instances]. -/
-abbrev MulAction.ofEndHom [Monoid M] (f : M →* Function.End α) : MulAction M α :=
-  MulAction.compHom α f
+abbrev MulAction.ofEndHom [Monoid M] (f : M →* Function.End α) : MulAction M α := .compHom α f
+
+/-- Given an action of an additive group `α` on a set `β`, each `g : α` defines a permutation of
+`β`. -/
+@[simps!]
+def AddAction.toPermHom (α : Type*) [AddGroup α] [AddAction α β] :
+    α →+ Additive (Equiv.Perm β) :=
+  MonoidHom.toAdditive'' <| MulAction.toPermHom (Multiplicative α) β
+
+/-- Given an action of a group `G` on a type `α`, each `g : G` defines a permutation of `α`. -/
+@[simps]
+def MulAction.toPermHom [Group G] [MulAction G α] : G →* Equiv.Perm α where
+  toFun := MulAction.toPerm
+  map_one' := Equiv.ext <| one_smul α
+  map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : α) u₂
+
+section MulDistribMulAction
+variable [Monoid M] [Monoid N] [Monoid O] [MulDistribMulAction M N] [MulDistribMulAction N O]
+
+/-- Pullback a multiplicative distributive multiplicative action along an injective monoid
+homomorphism.
+See note [reducible non-instances]. -/
+protected abbrev Function.Injective.mulDistribMulAction [SMul M O] (f : O →* N) (hf : Injective f)
+  (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M O where
+  __ := hf.mulAction f smul
+  smul_mul c x y := hf <| by simp only [smul, f.map_mul, smul_mul']
+  smul_one c := hf <| by simp only [smul, f.map_one, smul_one]
+
+/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
+homomorphism.
+See note [reducible non-instances]. -/
+protected abbrev Function.Surjective.mulDistribMulAction [SMul M O] (f : N →* O) (hf : Surjective f)
+    (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M O where
+  __ := hf.mulAction f smul
+  smul_mul c := by simp only [hf.forall, smul_mul', ← smul, ← f.map_mul, implies_true]
+  smul_one c := by rw [← f.map_one, ← smul, smul_one]
+
+variable (N) in
+/-- Scalar multiplication by `r` as a `MonoidHom`. -/
+def MulDistribMulAction.toMonoidHom (r : M) : N →* N where
+  toFun := (r • ·)
+  map_one' := smul_one r
+  map_mul' := smul_mul' r
+
+@[simp]
+lemma MulDistribMulAction.toMonoidHom_apply (r : M) (x : N) : toMonoidHom N r x = r • x := rfl
+
+@[simp] lemma smul_pow' (r : M) (x : N) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
+  (MulDistribMulAction.toMonoidHom ..).map_pow ..
+
+end MulDistribMulAction
+
+section MulDistribMulAction
+variable [Monoid M] [Group G] [MulDistribMulAction M G]
+
+@[simp]
+lemma smul_inv' (r : M) (x : G) : r • x⁻¹ = (r • x)⁻¹ :=
+  (MulDistribMulAction.toMonoidHom G r).map_inv x
+
+lemma smul_div' (r : M) (x y : G) : r • (x / y) = r • x / r • y :=
+  map_div (MulDistribMulAction.toMonoidHom G r) x y
+
+end MulDistribMulAction
+
+section MulDistribMulAction
+variable [Group G] [Monoid M] [MulDistribMulAction G M]
+variable (M)
+
+/-- Each element of the group defines a multiplicative monoid isomorphism.
+
+This is a stronger version of `MulAction.toPerm`. -/
+@[simps (config := { simpRhs := true })]
+def MulDistribMulAction.toMulEquiv (x : G) : M ≃* M :=
+  { MulDistribMulAction.toMonoidHom M x, MulAction.toPermHom G M x with }
+
+end MulDistribMulAction