feat(group_action/defs): generalize faithful actions (#8555)

This generalizes the `faithful_mul_semiring_action` typeclass to a mixin typeclass `has_faithful_scalar`, and provides instances for some simple actions:

* `has_faithful_scalar α α` (on cancellative monoids and monoids with zero)
* `has_faithful_scalar (opposite α) α`
* `has_faithful_scalar α (Π i, f i)`
* `has_faithful_scalar (units A) B`
* `has_faithful_scalar (equiv.perm α) α`
* `has_faithful_scalar M (α × β)`
* `has_faithful_scalar R (α →₀ M)`
* `has_faithful_scalar S (polynomial R)` (generalized from an existing instance)
* `has_faithful_scalar R (mv_polynomial σ S₁)`
* `has_faithful_scalar R (monoid_algebra k G)`
* `has_faithful_scalar R (add_monoid_algebra k G)`

As well as retaining the one other existing instance

* `faithful_mul_semiring_action ↥H E` where `H : subgroup (E ≃ₐ[F] E)`

The lemmas taking `faithful_mul_semiring_action` as a typeclass argument have been converted to use the new typeclass, but no attempt has been made to weaken their other hypotheses.

src/algebra/group_ring_action.lean

@@ -38,11 +38,6 @@ class mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R]
 
 export mul_semiring_action (smul_one)
 
-/-- Typeclass for faithful multiplicative actions by monoids on semirings. -/
-class faithful_mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R]
-  extends mul_semiring_action M R :=
-(eq_of_smul_eq_smul' : ∀ {m₁ m₂ : M}, (∀ r : R, m₁ • r = m₂ • r) → m₁ = m₂)
-
 section semiring
 
 variables (M G : Type u) [monoid M] [group G]
@@ -53,11 +48,6 @@ lemma smul_mul' [mul_semiring_action M R] (g : M) (x y : R) :
   g • (x * y) = (g • x) * (g • y) :=
 mul_semiring_action.smul_mul g x y
 
-variables {M} (R)
-theorem eq_of_smul_eq_smul [faithful_mul_semiring_action M R] {m₁ m₂ : M} :
-  (∀ r : R, m₁ • r = m₂ • r) → m₁ = m₂ :=
-faithful_mul_semiring_action.eq_of_smul_eq_smul'
-
 variables (M R)
 
 /-- Each element of the monoid defines a additive monoid homomorphism. -/
@@ -83,9 +73,9 @@ def mul_semiring_action.to_ring_hom [mul_semiring_action M R] (x : M) : R →+*
   map_mul' := smul_mul' x,
   .. distrib_mul_action.to_add_monoid_hom M R x }
 
-theorem to_ring_hom_injective [faithful_mul_semiring_action M R] :
+theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_scalar M R] :
   function.injective (mul_semiring_action.to_ring_hom M R) :=
-λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ r, ring_hom.ext_iff.1 h r
+λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, ring_hom.ext_iff.1 h r
 
 /-- Each element of the group defines a semiring isomorphism. -/
 def mul_semiring_action.to_semiring_equiv [mul_semiring_action G R] (x : G) : R ≃+* R :=

src/algebra/module/pi.lean

@@ -64,6 +64,22 @@ 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)⟩
 
+/-- 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. -/
+lemma has_faithful_scalar_at {α : Type*}
+  [Π i, has_scalar α $ f i] [Π i, nonempty (f i)] (i : I) [has_faithful_scalar α (f i)] :
+  has_faithful_scalar α (Π i, f i) :=
+⟨λ x y h, eq_of_smul_eq_smul $ λ a : f i, begin
+  classical,
+  have := congr_fun (h $ function.update (λ j, classical.choice (‹Π i, nonempty (f i)› j)) i a) i,
+  simpa using this,
+end⟩
+
+instance has_faithful_scalar {α : Type*}
+  [nonempty I] [Π i, has_scalar α $ f i] [Π i, nonempty (f i)] [Π i, has_faithful_scalar α (f i)] :
+  has_faithful_scalar α (Π i, f i) :=
+let ⟨i⟩ := ‹nonempty I› in has_faithful_scalar_at i
+
 instance mul_action (α) {m : monoid α} [Π i, mul_action α $ f i] :
   @mul_action α (Π i : I, f i) m :=
 { smul := (•),

src/algebra/monoid_algebra.lean

@@ -241,6 +241,10 @@ instance [semiring R] [semiring k] [module R k] :
   module R (monoid_algebra k G) :=
 finsupp.module G k
 
+instance [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_scalar R k] [nonempty G] :
+  has_faithful_scalar R (monoid_algebra k G) :=
+finsupp.has_faithful_scalar
+
 instance [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action S k]
   [has_scalar R S] [is_scalar_tower R S k] :
   is_scalar_tower R S (monoid_algebra k G) :=
@@ -902,6 +906,10 @@ instance [monoid R] [semiring k] [distrib_mul_action R k] :
   distrib_mul_action R (add_monoid_algebra k G) :=
 finsupp.distrib_mul_action G k
 
+instance [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_scalar R k] [nonempty G] :
+  has_faithful_scalar R (add_monoid_algebra k G) :=
+finsupp.has_faithful_scalar
+
 instance [semiring R] [semiring k] [module R k] : module R (add_monoid_algebra k G) :=
 finsupp.module G k
 

src/algebra/opposites.lean

@@ -126,9 +126,21 @@ instance [mul_one_class α] : mul_one_class (opposite α) :=
 instance [monoid α] : monoid (opposite α) :=
 { .. opposite.semigroup α, .. opposite.mul_one_class α }
 
+instance [right_cancel_monoid α] : left_cancel_monoid (opposite α) :=
+{ .. opposite.left_cancel_semigroup α, ..opposite.monoid α }
+
+instance [left_cancel_monoid α] : right_cancel_monoid (opposite α) :=
+{ .. opposite.right_cancel_semigroup α, ..opposite.monoid α }
+
+instance [cancel_monoid α] : cancel_monoid (opposite α) :=
+{ .. opposite.right_cancel_monoid α, ..opposite.left_cancel_monoid α }
+
 instance [comm_monoid α] : comm_monoid (opposite α) :=
 { .. opposite.monoid α, .. opposite.comm_semigroup α }
 
+instance [cancel_comm_monoid α] : cancel_comm_monoid (opposite α) :=
+{ .. opposite.cancel_monoid α, ..opposite.comm_monoid α }
+
 instance [has_inv α] : has_inv (opposite α) :=
 { inv := λ x, op $ (unop x)⁻¹ }
 
@@ -211,7 +223,7 @@ instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] :
   ..opposite.mul_action α R }
 
 /-- Like `monoid.to_mul_action`, but multiplies on the right. -/
-instance monoid.to_opposite_mul_action [monoid α] : mul_action (opposite α) α :=
+instance _root_.monoid.to_opposite_mul_action [monoid α] : mul_action (opposite α) α :=
 { smul := λ c x, x * c.unop,
   one_smul := mul_one,
   mul_smul := λ x y r, (mul_assoc _ _ _).symm }
@@ -222,6 +234,16 @@ example [monoid α] : monoid.to_mul_action (opposite α) = opposite.mul_action 
 
 lemma op_smul_eq_mul [monoid α] {a a' : α} : op a • a' = a' * a := rfl
 
+/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/
+instance left_cancel_monoid.to_has_faithful_scalar [left_cancel_monoid α] :
+  has_faithful_scalar (opposite α) α :=
+⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩
+
+/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/
+instance cancel_monoid_with_zero.to_has_faithful_opposite_scalar
+  [cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar (opposite α) α :=
+⟨λ x y h, unop_injective $ mul_left_cancel' one_ne_zero (h 1)⟩
+
 @[simp] lemma op_zero [has_zero α] : op (0 : α) = 0 := rfl
 @[simp] lemma unop_zero [has_zero α] : unop (0 : αᵒᵖ) = 0 := rfl
 

src/algebra/polynomial/group_ring_action.lean

@@ -43,15 +43,6 @@ noncomputable instance [mul_semiring_action M R] : mul_semiring_action M (polyno
   smul_mul := λ m p q, (smul_eq_map R m).symm ▸ map_mul (mul_semiring_action.to_ring_hom M R m),
   ..polynomial.distrib_mul_action }
 
-noncomputable instance [faithful_mul_semiring_action M R] :
-  faithful_mul_semiring_action M (polynomial R) :=
-{ eq_of_smul_eq_smul' := λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ s, C_inj.1 $
-    calc  C (m₁ • s)
-        = m₁ • C s : (smul_C _ _).symm
-    ... = m₂ • C s : h (C s)
-    ... = C (m₂ • s) : smul_C _ _,
-  .. polynomial.mul_semiring_action M R }
-
 variables {M R}
 
 variables [mul_semiring_action M R]

src/data/finsupp/basic.lean

@@ -2082,6 +2082,11 @@ Throughout this section, some `monoid` and `semiring` arguments are specified wi
 lemma smul_apply {_ : monoid R} [add_monoid M] [distrib_mul_action R M]
   (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • (v a) := rfl
 
+instance [monoid R] [nonempty α] [add_monoid M] [distrib_mul_action R M] [has_faithful_scalar R M] :
+  has_faithful_scalar R (α →₀ M) :=
+{ eq_of_smul_eq_smul := λ r₁ r₂ h, let ⟨a⟩ := ‹nonempty α› in eq_of_smul_eq_smul $ λ m : M,
+    by simpa using congr_fun (h (single a m)) a }
+
 variables (α M)
 
 instance [monoid R] [add_monoid M] [distrib_mul_action R M] : distrib_mul_action R (α →₀ M) :=

src/data/mv_polynomial/basic.lean

@@ -104,6 +104,9 @@ instance [comm_semiring R] : inhabited (mv_polynomial σ R) := ⟨0⟩
 instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] :
   distrib_mul_action R (mv_polynomial σ S₁) :=
 add_monoid_algebra.distrib_mul_action
+instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] [has_faithful_scalar R S₁] :
+  has_faithful_scalar R (mv_polynomial σ S₁) :=
+add_monoid_algebra.has_faithful_scalar
 instance [semiring R] [comm_semiring S₁] [module R S₁] : module R (mv_polynomial σ S₁) :=
 add_monoid_algebra.module
 instance [monoid R] [monoid S₁] [comm_semiring S₂]

src/data/polynomial/basic.lean

@@ -132,6 +132,10 @@ instance {S} [monoid S] [distrib_mul_action S R] : distrib_mul_action S (polynom
   smul_add := by { rintros _ ⟨⟩ ⟨⟩, simp [smul_to_finsupp, add_to_finsupp] },
   smul_zero := by { rintros _, simp [← zero_to_finsupp, smul_to_finsupp] } }
 
+instance {S} [monoid S] [distrib_mul_action S R] [has_faithful_scalar S R] :
+  has_faithful_scalar S (polynomial R) :=
+{ eq_of_smul_eq_smul := λ s₁ s₂ h, eq_of_smul_eq_smul $ λ a : ℕ →₀ R, congr_arg to_finsupp (h ⟨a⟩) }
+
 instance {S} [semiring S] [module S R] : module S (polynomial R) :=
 { smul := (•),
   add_smul := by { rintros _ _ ⟨⟩, simp [smul_to_finsupp, add_to_finsupp, add_smul] },

src/field_theory/fixed.lean

@@ -295,18 +295,18 @@ namespace fixed_points
 /-- Embedding produced from a faithful action. -/
 @[simps apply {fully_applied := ff}]
 def to_alg_hom (G : Type u) (F : Type v) [group G] [field F]
-  [faithful_mul_semiring_action G F] : G ↪ (F →ₐ[fixed_points.subfield G F] F) :=
+  [mul_semiring_action G F] [has_faithful_scalar G F] : G ↪ (F →ₐ[fixed_points.subfield G F] F) :=
 { to_fun := λ g, { commutes' := λ x, x.2 g,
     .. mul_semiring_action.to_ring_hom G F g },
   inj' := λ g₁ g₂ hg, to_ring_hom_injective G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, }
 
 lemma to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F]
-  [faithful_mul_semiring_action G F] (g : G) (x : F) :
+  [mul_semiring_action G F] [has_faithful_scalar G F] (g : G) (x : F) :
   to_alg_hom G F g x = g • x :=
 rfl
 
 theorem finrank_eq_card (G : Type u) (F : Type v) [group G] [field F]
-  [fintype G] [faithful_mul_semiring_action G F] :
+  [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] :
   finrank (fixed_points.subfield G F) F = fintype.card G :=
 le_antisymm (fixed_points.finrank_le_card G F) $
 calc  fintype.card G
@@ -316,7 +316,7 @@ calc  fintype.card G
 ... = finrank (fixed_points.subfield G F) F : finrank_linear_map' _ _ _
 
 theorem to_alg_hom_bijective (G : Type u) (F : Type v) [group G] [field F]
-  [fintype G] [faithful_mul_semiring_action G F] :
+  [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] :
   function.bijective (to_alg_hom G F) :=
 begin
   rw fintype.bijective_iff_injective_and_card,
@@ -330,7 +330,8 @@ end
 
 /-- Bijection between G and algebra homomorphisms that fix the fixed points -/
 def to_alg_hom_equiv (G : Type u) (F : Type v) [group G] [field F]
-  [fintype G] [faithful_mul_semiring_action G F] : G ≃ (F →ₐ[fixed_points.subfield G F] F) :=
+  [fintype G] [mul_semiring_action G F] [has_faithful_scalar G F] :
+    G ≃ (F →ₐ[fixed_points.subfield G F] F) :=
 function.embedding.equiv_of_surjective (to_alg_hom G F) (to_alg_hom_bijective G F).2
 
 end fixed_points

src/field_theory/galois.lean

@@ -170,15 +170,17 @@ variables (H : subgroup (E ≃ₐ[F] E)) (K : intermediate_field F E)
 
 namespace intermediate_field
 
-instance subgroup_action : faithful_mul_semiring_action H E :=
+instance subgroup_action : mul_semiring_action H E :=
 { smul := λ h x, h x,
   smul_zero := λ _, map_zero _,
   smul_add := λ _, map_add _,
   one_smul := λ _, rfl,
   smul_one := λ _, map_one _,
   mul_smul := λ _ _ _, rfl,
-  smul_mul := λ _, map_mul _,
-  eq_of_smul_eq_smul' := λ x y z, subtype.ext (alg_equiv.ext z) }
+  smul_mul := λ _, map_mul _ }
+
+instance : has_faithful_scalar H E :=
+{ eq_of_smul_eq_smul := λ x y z, subtype.ext (alg_equiv.ext z) }
 
 /-- The intermediate_field fixed by a subgroup -/
 def fixed_field : intermediate_field F E :=

src/group_theory/group_action/defs.lean

@@ -56,6 +56,22 @@ class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α)
 infix ` +ᵥ `:65 := has_vadd.vadd
 infixr ` • `:73 := has_scalar.smul
 
+/-- Typeclass for faithful actions. -/
+class has_faithful_vadd (G : Type*) (P : Type*) [has_vadd G P] : Prop :=
+(eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ p : P, g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂)
+
+/-- Typeclass for faithful actions. -/
+@[to_additive has_faithful_vadd]
+class has_faithful_scalar (M : Type*) (α : Type*) [has_scalar M α] : Prop :=
+(eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ a : α, m₁ • a = m₂ • a) → m₁ = m₂)
+
+export has_faithful_scalar (eq_of_smul_eq_smul) has_faithful_vadd (eq_of_vadd_eq_vadd)
+
+@[to_additive]
+lemma smul_left_injective' [has_scalar M α] [has_faithful_scalar M α] :
+  function.injective ((•) : M → α → α) :=
+λ m₁ m₂ h, has_faithful_scalar.eq_of_smul_eq_smul (congr_fun h)
+
 /-- See also `monoid.to_mul_action` and `mul_zero_class.to_smul_with_zero`. -/
 @[priority 910, to_additive] -- see Note [lower instance priority]
 instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := ⟨(*)⟩

src/group_theory/group_action/group.lean

@@ -22,6 +22,12 @@ variables {α : Type u} {β : Type v} {γ : Type w}
 
 section mul_action
 
+/-- `monoid.to_mul_action` is faithful on cancellative monoids. -/
+@[to_additive /-" `add_monoid.to_add_action` is faithful on additive cancellative monoids. "-/]
+instance right_cancel_monoid.to_has_faithful_scalar [right_cancel_monoid α] :
+  has_faithful_scalar α α :=
+⟨λ x y h, mul_right_cancel (h 1)⟩
+
 section group
 variables [group α] [mul_action α β]
 
@@ -62,6 +68,10 @@ instance mul_action.perm (α : Type*) : mul_action (equiv.perm α) α :=
 
 @[simp] lemma equiv.perm.smul_def {α : Type*} (f : equiv.perm α) (a : α) : f • a = f a := rfl
 
+/-- `mul_action.perm` is faithful. -/
+instance equiv.perm.has_faithful_scalar (α : Type*) : has_faithful_scalar (equiv.perm α) α :=
+⟨λ x y, equiv.ext⟩
+
 variables {α} {β}
 
 @[to_additive] lemma inv_smul_eq_iff {a : α} {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
@@ -92,6 +102,11 @@ mul_action.injective g h
 
 end group
 
+/-- `monoid.to_mul_action` is faithful on nontrivial cancellative monoids with zero. -/
+instance cancel_monoid_with_zero.to_has_faithful_scalar [cancel_monoid_with_zero α] [nontrivial α] :
+  has_faithful_scalar α α :=
+⟨λ x y h, mul_left_injective' one_ne_zero (h 1)⟩
+
 section gwz
 variables [group_with_zero α] [mul_action α β]
 

src/group_theory/group_action/prod.lean

@@ -34,6 +34,16 @@ 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 _ _ _⟩ }
 
+@[to_additive has_faithful_vadd_left]
+instance has_faithful_scalar_left [has_faithful_scalar M α] [nonempty β] :
+  has_faithful_scalar M (α × β) :=
+⟨λ x y h, let ⟨b⟩ := ‹nonempty β› in eq_of_smul_eq_smul $ λ a : α, by injection h (a, b)⟩
+
+@[to_additive has_faithful_vadd_right]
+instance has_faithful_scalar_right [nonempty α] [has_faithful_scalar M β] :
+  has_faithful_scalar M (α × β) :=
+⟨λ x y h, let ⟨a⟩ := ‹nonempty α› in eq_of_smul_eq_smul $ λ b : β, by injection h (a, b)⟩
+
 end
 
 @[to_additive] instance {m : monoid M} [mul_action M α] [mul_action M β] : mul_action M (α × β) :=

src/group_theory/group_action/units.lean

@@ -32,6 +32,10 @@ instance [monoid M] [has_scalar M α] : has_scalar (units M) α :=
 lemma smul_def [monoid M] [has_scalar M α] (m : units M) (a : α) :
   m • a = (m : M) • a := rfl
 
+@[to_additive]
+instance [monoid M] [has_scalar M α] [has_faithful_scalar M α] : has_faithful_scalar (units M) α :=
+{ eq_of_smul_eq_smul := λ u₁ u₂ h, units.ext $ eq_of_smul_eq_smul h, }
+
 @[to_additive]
 instance [monoid M] [mul_action M α] : mul_action (units M) α :=
 { one_smul := (one_smul M : _),