Merge master into nightly-testing

Mathlib.lean

@@ -319,6 +319,8 @@ import Mathlib.Algebra.Group.ZeroOne
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Action.End
+import Mathlib.Algebra.GroupWithZero.Action.Faithful
 import Mathlib.Algebra.GroupWithZero.Action.Opposite
 import Mathlib.Algebra.GroupWithZero.Action.Pi
 import Mathlib.Algebra.GroupWithZero.Action.Prod

Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
-import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Action.End
 
 /-!
 # Distributive actions by submonoids

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

@@ -3,35 +3,26 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Action.Units
-import Mathlib.Algebra.Group.Equiv.Basic
-import Mathlib.Algebra.GroupWithZero.Units.Basic
+import Mathlib.Algebra.Group.Action.Defs
+import Mathlib.Algebra.Group.Hom.Defs
 
 /-!
 # Definitions of group actions
 
 This file defines a hierarchy of group action type-classes on top of the previously defined
 notation classes `SMul` and its additive version `VAdd`:
 
-* `MulAction M α` and its additive version `AddAction G P` are typeclasses used for
-  actions of multiplicative and additive monoids and groups; they extend notation classes
-  `SMul` and `VAdd` that are defined in `Algebra.Group.Defs`;
+* `SMulZeroClass` is a typeclass for an action that preserves zero
+* `DistribSMul M A` is a typeclass for an action on an additive monoid (`AddZeroClass`) that
+  preserves addition and zero
 * `DistribMulAction M A` is a typeclass for an action of a multiplicative monoid on
   an additive monoid such that `a • (b + c) = a • b + a • c` and `a • 0 = 0`.
 
 The hierarchy is extended further by `Module`, defined elsewhere.
 
-Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the
-interaction of different group actions,
-
-* `SMulCommClass M N α` and its additive version `VAddCommClass M N α`;
-* `IsScalarTower M N α` and its additive version `VAddAssocClass M N α`;
-* `IsCentralScalar M α` and its additive version `IsCentralVAdd M N α`.
-
 ## Notation
 
 - `a • b` is used as notation for `SMul.smul a b`.
-- `a +ᵥ b` is used as notation for `VAdd.vadd a b`.
 
 ## Implementation details
 
@@ -51,42 +42,6 @@ open Function
 
 variable {M N A B α β : Type*}
 
-/-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero. -/
-instance CancelMonoidWithZero.faithfulSMul [CancelMonoidWithZero α] [Nontrivial α] :
-    FaithfulSMul α α where eq_of_smul_eq_smul  h := mul_left_injective₀ one_ne_zero (h 1)
-
-section GroupWithZero
-variable [GroupWithZero α] [MulAction α β] {a : α}
-
-@[simp] lemma inv_smul_smul₀ (ha : a ≠ 0) (x : β) : a⁻¹ • a • x = x :=
-  inv_smul_smul (Units.mk0 a ha) x
-
-@[simp]
-lemma smul_inv_smul₀ (ha : a ≠ 0) (x : β) : a • a⁻¹ • x = x := smul_inv_smul (Units.mk0 a ha) x
-
-lemma inv_smul_eq_iff₀ (ha : a ≠ 0) {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
-  inv_smul_eq_iff (g := Units.mk0 a ha)
-
-lemma eq_inv_smul_iff₀ (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
-  eq_inv_smul_iff (g := Units.mk0 a ha)
-
-@[simp]
-lemma Commute.smul_right_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
-    (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y := Commute.smul_right_iff (g := Units.mk0 a ha)
-
-@[simp]
-lemma Commute.smul_left_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
-    (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y := Commute.smul_left_iff (g := Units.mk0 a ha)
-
-/-- Right scalar multiplication as an order isomorphism. -/
-@[simps] def Equiv.smulRight (ha : a ≠ 0) : β ≃ β where
-  toFun b := a • b
-  invFun b := a⁻¹ • b
-  left_inv := inv_smul_smul₀ ha
-  right_inv := smul_inv_smul₀ ha
-
-end GroupWithZero
-
 /-- Typeclass for scalar multiplication that preserves `0` on the right. -/
 class SMulZeroClass (M A : Type*) [Zero A] extends SMul M A where
   /-- Multiplying `0` by a scalar gives `0` -/
@@ -257,22 +212,8 @@ protected abbrev Function.Surjective.distribMulAction [AddMonoid B] [SMul M B] (
     (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : DistribMulAction M B :=
   { hf.distribSMul f smul, hf.mulAction f smul with }
 
-/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
-
-See also `Function.Surjective.mulActionLeft` and `Function.Surjective.moduleLeft`.
--/
-abbrev Function.Surjective.distribMulActionLeft {R S M : Type*} [Monoid R] [AddMonoid M]
-    [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective f)
-    (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribMulAction S M :=
-  { hf.distribSMulLeft f hsmul, hf.mulActionLeft f hsmul with }
-
 variable (A)
 
-/-- Compose a `DistribMulAction` with a `MonoidHom`, with action `f r' • m`.
-See note [reducible non-instances]. -/
-abbrev DistribMulAction.compHom [Monoid N] (f : N →* M) : DistribMulAction N A :=
-  { DistribSMul.compFun A f, MulAction.compHom A f with }
-
 /-- Each element of the monoid defines an additive monoid homomorphism. -/
 @[simps!]
 def DistribMulAction.toAddMonoidHom (x : M) : A →+ A :=
@@ -360,13 +301,6 @@ protected abbrev Function.Surjective.mulDistribMulAction [Monoid B] [SMul M B] (
 
 variable (A)
 
-/-- Compose a `MulDistribMulAction` with a `MonoidHom`, with action `f r' • m`.
-See note [reducible non-instances]. -/
-abbrev MulDistribMulAction.compHom [Monoid N] (f : N →* M) : MulDistribMulAction N A :=
-  { MulAction.compHom A f with
-    smul_one := fun x => smul_one (f x),
-    smul_mul := fun x => smul_mul' (f x) }
-
 /-- Scalar multiplication by `r` as a `MonoidHom`. -/
 def MulDistribMulAction.toMonoidHom (r : M) :
     A →* A where
@@ -384,16 +318,6 @@ theorem MulDistribMulAction.toMonoidHom_apply (r : M) (x : A) :
 @[simp] lemma smul_pow' (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
   (MulDistribMulAction.toMonoidHom _ _).map_pow _ _
 
-variable (M A)
-
-/-- Each element of the monoid defines a monoid homomorphism. -/
-@[simps]
-def MulDistribMulAction.toMonoidEnd :
-    M →* Monoid.End A where
-  toFun := MulDistribMulAction.toMonoidHom A
-  map_one' := MonoidHom.ext <| one_smul M
-  map_mul' x y := MonoidHom.ext <| mul_smul x y
-
 end
 
 section
@@ -409,36 +333,6 @@ theorem smul_div' (r : M) (x y : A) : r • (x / y) = r • x / r • y :=
 
 end
 
-/-- The tautological action by `AddMonoid.End α` on `α`.
-
-This generalizes `Function.End.applyMulAction`. -/
-instance AddMonoid.End.applyDistribMulAction [AddMonoid α] :
-    DistribMulAction (AddMonoid.End α) α where
-  smul := (· <| ·)
-  smul_zero := AddMonoidHom.map_zero
-  smul_add := AddMonoidHom.map_add
-  one_smul _ := rfl
-  mul_smul _ _ _ := rfl
-
-@[simp]
-theorem AddMonoid.End.smul_def [AddMonoid α] (f : AddMonoid.End α) (a : α) : f • a = f a :=
-  rfl
-
-/-- `AddMonoid.End.applyDistribMulAction` is faithful. -/
-instance AddMonoid.End.applyFaithfulSMul [AddMonoid α] :
-    FaithfulSMul (AddMonoid.End α) α :=
-  ⟨fun {_ _ h} => AddMonoidHom.ext h⟩
-
-/-- Each non-zero element of a `GroupWithZero` defines an additive monoid isomorphism of an
-`AddMonoid` on which it acts distributively.
-This is a stronger version of `DistribMulAction.toAddMonoidHom`. -/
-def DistribMulAction.toAddEquiv₀ {α : Type*} (β : Type*) [GroupWithZero α] [AddMonoid β]
-    [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β :=
-  { DistribMulAction.toAddMonoidHom β x with
-    invFun := fun b ↦ x⁻¹ • b
-    left_inv := fun b ↦ inv_smul_smul₀ hx b
-    right_inv := fun b ↦ smul_inv_smul₀ hx b }
-
 section Group
 variable [Group α] [AddMonoid β] [DistribMulAction α β]
 

Mathlib/Algebra/GroupWithZero/Action/End.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Yury Kudryashov
+-/
+import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Equiv.Basic
+import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Action.Units
+
+/-!
+# Group actions and (endo)morphisms
+-/
+
+assert_not_exists Equiv.Perm.equivUnitsEnd
+assert_not_exists Prod.fst_mul
+assert_not_exists Ring
+
+open Function
+
+variable {M N A B α β : Type*}
+
+/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
+
+See also `Function.Surjective.mulActionLeft` and `Function.Surjective.moduleLeft`.
+-/
+abbrev Function.Surjective.distribMulActionLeft {R S M : Type*} [Monoid R] [AddMonoid M]
+    [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective f)
+    (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribMulAction S M :=
+  { hf.distribSMulLeft f hsmul, hf.mulActionLeft f hsmul with }
+
+section AddMonoid
+
+variable (A) [AddMonoid A] [Monoid M] [DistribMulAction M A]
+
+/-- Compose a `DistribMulAction` with a `MonoidHom`, with action `f r' • m`.
+See note [reducible non-instances]. -/
+abbrev DistribMulAction.compHom [Monoid N] (f : N →* M) : DistribMulAction N A :=
+  { DistribSMul.compFun A f, MulAction.compHom A f with }
+
+end AddMonoid
+
+section Monoid
+
+variable (A) [Monoid A] [Monoid M] [MulDistribMulAction M A]
+
+/-- Compose a `MulDistribMulAction` with a `MonoidHom`, with action `f r' • m`.
+See note [reducible non-instances]. -/
+abbrev MulDistribMulAction.compHom [Monoid N] (f : N →* M) : MulDistribMulAction N A :=
+  { MulAction.compHom A f with
+    smul_one := fun x => smul_one (f x),
+    smul_mul := fun x => smul_mul' (f x) }
+
+end Monoid
+
+/-- The tautological action by `AddMonoid.End α` on `α`.
+
+This generalizes `Function.End.applyMulAction`. -/
+instance AddMonoid.End.applyDistribMulAction [AddMonoid α] :
+    DistribMulAction (AddMonoid.End α) α where
+  smul := (· <| ·)
+  smul_zero := AddMonoidHom.map_zero
+  smul_add := AddMonoidHom.map_add
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+
+@[simp]
+theorem AddMonoid.End.smul_def [AddMonoid α] (f : AddMonoid.End α) (a : α) : f • a = f a :=
+  rfl
+
+/-- `AddMonoid.End.applyDistribMulAction` is faithful. -/
+instance AddMonoid.End.applyFaithfulSMul [AddMonoid α] :
+    FaithfulSMul (AddMonoid.End α) α :=
+  ⟨fun {_ _ h} => AddMonoidHom.ext h⟩
+
+/-- Each non-zero element of a `GroupWithZero` defines an additive monoid isomorphism of an
+`AddMonoid` on which it acts distributively.
+This is a stronger version of `DistribMulAction.toAddMonoidHom`. -/
+def DistribMulAction.toAddEquiv₀ {α : Type*} (β : Type*) [GroupWithZero α] [AddMonoid β]
+    [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β :=
+  { DistribMulAction.toAddMonoidHom β x with
+    invFun := fun b ↦ x⁻¹ • b
+    left_inv := fun b ↦ inv_smul_smul₀ hx b
+    right_inv := fun b ↦ smul_inv_smul₀ hx b }
+
+variable (M A) in
+/-- Each element of the monoid defines a monoid homomorphism. -/
+@[simps]
+def MulDistribMulAction.toMonoidEnd [Monoid M] [Monoid A] [MulDistribMulAction M A] :
+    M →* Monoid.End A where
+  toFun := MulDistribMulAction.toMonoidHom A
+  map_one' := MonoidHom.ext <| one_smul M
+  map_mul' x y := MonoidHom.ext <| mul_smul x y

Mathlib/Algebra/GroupWithZero/Action/Faithful.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Yury Kudryashov
+-/
+import Mathlib.Algebra.Group.Action.Faithful
+import Mathlib.Algebra.GroupWithZero.NeZero
+
+/-!
+# Faithful actions involving groups with zero
+-/
+
+assert_not_exists Equiv.Perm.equivUnitsEnd
+assert_not_exists Prod.fst_mul
+assert_not_exists Ring
+
+open Function
+
+variable {M N A B α β : Type*}
+
+/-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero. -/
+instance CancelMonoidWithZero.faithfulSMul [CancelMonoidWithZero α] [Nontrivial α] :
+    FaithfulSMul α α where eq_of_smul_eq_smul  h := mul_left_injective₀ one_ne_zero (h 1)

Mathlib/Algebra/GroupWithZero/Action/Prod.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import Mathlib.Algebra.Group.Action.Prod
-import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Action.End
 
 /-!
 # Prod instances for multiplicative actions with zero

Mathlib/Algebra/GroupWithZero/Action/Units.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Action.Units
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Units.Basic
 
 /-!
 # Multiplicative actions with zero on and by `Mˣ`
@@ -23,7 +24,39 @@ admits a `MulDistribMulAction G Mˣ` structure, again with the obvious definitio
 * `Algebra.GroupWithZero.Action.Prod`
 -/
 
-variable {G M α : Type*}
+variable {G M α β : Type*}
+
+section GroupWithZero
+variable [GroupWithZero α] [MulAction α β] {a : α}
+
+@[simp] lemma inv_smul_smul₀ (ha : a ≠ 0) (x : β) : a⁻¹ • a • x = x :=
+  inv_smul_smul (Units.mk0 a ha) x
+
+@[simp]
+lemma smul_inv_smul₀ (ha : a ≠ 0) (x : β) : a • a⁻¹ • x = x := smul_inv_smul (Units.mk0 a ha) x
+
+lemma inv_smul_eq_iff₀ (ha : a ≠ 0) {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
+  inv_smul_eq_iff (g := Units.mk0 a ha)
+
+lemma eq_inv_smul_iff₀ (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
+  eq_inv_smul_iff (g := Units.mk0 a ha)
+
+@[simp]
+lemma Commute.smul_right_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
+    (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y := Commute.smul_right_iff (g := Units.mk0 a ha)
+
+@[simp]
+lemma Commute.smul_left_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
+    (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y := Commute.smul_left_iff (g := Units.mk0 a ha)
+
+/-- Right scalar multiplication as an order isomorphism. -/
+@[simps] def Equiv.smulRight (ha : a ≠ 0) : β ≃ β where
+  toFun b := a • b
+  invFun b := a⁻¹ • b
+  left_inv := inv_smul_smul₀ ha
+  right_inv := smul_inv_smul₀ ha
+
+end GroupWithZero
 
 namespace Units
 

Mathlib/Algebra/Module/Defs.lean

@@ -3,6 +3,8 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
+import Mathlib.Algebra.GroupWithZero.Action.End
+import Mathlib.Algebra.GroupWithZero.Action.Units
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Int.Cast.Lemmas
 

Mathlib/Algebra/Ring/Action/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Ring.Hom.Defs
 
 /-!

Mathlib/Data/NNRat/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Group.Indicator
+import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Order.Field.Rat
 
 /-!