refactor(group_theory/group_action/defs): rename has_faithful_scalar (#14515)

This is the first scalar -> smul renaming transition.

Discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/scalar.20smul.20naming.20discrepancy

Author: berndlosert

scripts/nolints.txt

@@ -413,7 +413,7 @@ apply_nolint monoid.to_opposite_mul_action to_additive_doc
 -- group_theory/group_action/pi.lean
 apply_nolint function.has_scalar to_additive_doc
 apply_nolint function.smul_comm_class to_additive_doc
-apply_nolint pi.has_faithful_scalar_at to_additive_doc
+apply_nolint pi.has_faithful_smul_at to_additive_doc
 
 -- group_theory/group_action/sub_mul_action.lean
 apply_nolint sub_mul_action.has_zero fails_quickly

src/algebra/algebra/basic.lean

@@ -1157,7 +1157,7 @@ instance apply_mul_semiring_action : mul_semiring_action (A₁ ≃ₐ[R] A₁) A
 
 @[simp] protected lemma smul_def (f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = f a := rfl
 
-instance apply_has_faithful_scalar : has_faithful_scalar (A₁ ≃ₐ[R] A₁) A₁ :=
+instance apply_has_faithful_smul : has_faithful_smul (A₁ ≃ₐ[R] A₁) A₁ :=
 ⟨λ _ _, alg_equiv.ext⟩
 
 instance apply_smul_comm_class : smul_comm_class R (A₁ ≃ₐ[R] A₁) A₁ :=
@@ -1228,7 +1228,7 @@ This is a stronger version of `mul_semiring_action.to_ring_hom` and
 def to_alg_hom (m : M) : A →ₐ[R] A :=
 alg_hom.mk' (mul_semiring_action.to_ring_hom _ _ m) (smul_comm _)
 
-theorem to_alg_hom_injective [has_faithful_scalar M A] :
+theorem to_alg_hom_injective [has_faithful_smul M A] :
   function.injective (mul_semiring_action.to_alg_hom R A : M → A →ₐ[R] A) :=
 λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, alg_hom.ext_iff.1 h r
 
@@ -1246,7 +1246,7 @@ def to_alg_equiv (g : G) : A ≃ₐ[R] A :=
 { .. mul_semiring_action.to_ring_equiv _ _ g,
   .. mul_semiring_action.to_alg_hom R A g }
 
-theorem to_alg_equiv_injective [has_faithful_scalar G A] :
+theorem to_alg_equiv_injective [has_faithful_smul G A] :
   function.injective (mul_semiring_action.to_alg_equiv R A : G → A ≃ₐ[R] A) :=
 λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, alg_equiv.ext_iff.1 h r
 

src/algebra/algebra/subalgebra/basic.lean

@@ -934,9 +934,9 @@ instance is_scalar_tower_left
   is_scalar_tower S α β :=
 S.to_subsemiring.is_scalar_tower
 
-instance [has_scalar A α] [has_faithful_scalar A α] (S : subalgebra R A) :
-  has_faithful_scalar S α :=
-S.to_subsemiring.has_faithful_scalar
+instance [has_scalar A α] [has_faithful_smul A α] (S : subalgebra R A) :
+  has_faithful_smul S α :=
+S.to_subsemiring.has_faithful_smul
 
 /-- The action by a subalgebra is the action by the underlying algebra. -/
 instance [mul_action A α] (S : subalgebra R A) : mul_action S α :=

src/algebra/group_ring_action.lean

@@ -55,7 +55,7 @@ def mul_semiring_action.to_ring_hom [mul_semiring_action M R] (x : M) : R →+*
 { .. mul_distrib_mul_action.to_monoid_hom R x,
   .. distrib_mul_action.to_add_monoid_hom R x }
 
-theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_scalar M R] :
+theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_smul M R] :
   function.injective (mul_semiring_action.to_ring_hom M R) :=
 λ m₁ m₂ h, eq_of_smul_eq_smul $ λ r, ring_hom.ext_iff.1 h r
 

src/algebra/hom/aut.lean

@@ -83,7 +83,7 @@ instance apply_mul_distrib_mul_action {M} [monoid M] : mul_distrib_mul_action (m
 @[simp] protected lemma smul_def {M} [monoid M] (f : mul_aut M) (a : M) : f • a = f a := rfl
 
 /-- `mul_aut.apply_mul_action` is faithful. -/
-instance apply_has_faithful_scalar {M} [monoid M] : has_faithful_scalar (mul_aut M) M :=
+instance apply_has_faithful_smul {M} [monoid M] : has_faithful_smul (mul_aut M) M :=
 ⟨λ _ _, mul_equiv.ext⟩
 
 /-- Group conjugation, `mul_aut.conj g h = g * h * g⁻¹`, as a monoid homomorphism
@@ -159,7 +159,7 @@ instance apply_distrib_mul_action {A} [add_monoid A] : distrib_mul_action (add_a
 @[simp] protected lemma smul_def {A} [add_monoid A] (f : add_aut A) (a : A) : f • a = f a := rfl
 
 /-- `add_aut.apply_distrib_mul_action` is faithful. -/
-instance apply_has_faithful_scalar {A} [add_monoid A] : has_faithful_scalar (add_aut A) A :=
+instance apply_has_faithful_smul {A} [add_monoid A] : has_faithful_smul (add_aut A) A :=
 ⟨λ _ _, add_equiv.ext⟩
 
 /-- Additive group conjugation, `add_aut.conj g h = g + h - g`, as an additive monoid

src/algebra/module/basic.lean

@@ -297,7 +297,7 @@ instance ring_hom.apply_distrib_mul_action [semiring R] : distrib_mul_action (R
   f • a = f a := rfl
 
 /-- `ring_hom.apply_distrib_mul_action` is faithful. -/
-instance ring_hom.apply_has_faithful_scalar [semiring R] : has_faithful_scalar (R →+* R) R :=
+instance ring_hom.apply_has_faithful_smul [semiring R] : has_faithful_smul (R →+* R) R :=
 ⟨ring_hom.ext⟩
 
 section add_comm_monoid

src/algebra/module/equiv.lean

@@ -481,7 +481,7 @@ instance apply_distrib_mul_action : distrib_mul_action (M ≃ₗ[R] M) M :=
   f • a = f a := rfl
 
 /-- `linear_equiv.apply_distrib_mul_action` is faithful. -/
-instance apply_has_faithful_scalar : has_faithful_scalar (M ≃ₗ[R] M) M :=
+instance apply_has_faithful_smul : has_faithful_smul (M ≃ₗ[R] M) M :=
 ⟨λ _ _, linear_equiv.ext⟩
 
 instance apply_smul_comm_class : smul_comm_class R (M ≃ₗ[R] M) M :=

src/algebra/module/linear_map.lean

@@ -847,7 +847,7 @@ instance apply_module : module (module.End R M) M :=
 @[simp] protected lemma smul_def (f : module.End R M) (a : M) : f • a = f a := rfl
 
 /-- `linear_map.apply_module` is faithful. -/
-instance apply_has_faithful_scalar : has_faithful_scalar (module.End R M) M :=
+instance apply_has_faithful_smul : has_faithful_smul (module.End R M) M :=
 ⟨λ _ _, linear_map.ext⟩
 
 instance apply_smul_comm_class : smul_comm_class R (module.End R M) M :=

src/algebra/monoid_algebra/basic.lean

@@ -270,9 +270,9 @@ 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] [semiring k] [distrib_mul_action R k] [has_faithful_smul R k] [nonempty G] :
+  has_faithful_smul R (monoid_algebra k G) :=
+finsupp.has_faithful_smul
 
 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] :
@@ -1106,9 +1106,9 @@ 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 [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_smul R k] [nonempty G] :
+  has_faithful_smul R (add_monoid_algebra k G) :=
+finsupp.has_faithful_smul
 
 instance [semiring R] [semiring k] [module R k] : module R (add_monoid_algebra k G) :=
 finsupp.module G k

src/analysis/normed_space/M_structure.lean

@@ -90,7 +90,7 @@ lemma Lcomplement {P : M} (h: is_Lprojection X P) : is_Lprojection X (1 - P) :=
 lemma Lcomplement_iff (P : M) : is_Lprojection X P ↔ is_Lprojection X (1 - P) :=
 ⟨Lcomplement, λ h, sub_sub_cancel 1 P ▸ h.Lcomplement⟩
 
-lemma commute [has_faithful_scalar M X] {P Q : M} (h₁ : is_Lprojection X P)
+lemma commute [has_faithful_smul M X] {P Q : M} (h₁ : is_Lprojection X P)
   (h₂ : is_Lprojection X Q) : commute P Q :=
 begin
   have PR_eq_RPR : ∀ R : M, is_Lprojection X R → P * R = R * P * R := λ R h₃,
@@ -130,7 +130,7 @@ begin
   show P * Q = Q * P, by rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
 end
 
-lemma mul [has_faithful_scalar M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :
+lemma mul [has_faithful_smul M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :
   is_Lprojection X (P * Q) :=
 begin
   refine ⟨is_idempotent_elem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, _⟩,
@@ -151,7 +151,7 @@ begin
       mul_smul] }
 end
 
-lemma join [has_faithful_scalar M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :
+lemma join [has_faithful_smul M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :
   is_Lprojection X (P + Q - P * Q) :=
 begin
   convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1,
@@ -164,31 +164,31 @@ instance : has_compl { f : M // is_Lprojection X f } :=
 @[simp] lemma coe_compl (P : {P : M // is_Lprojection X P}) :
   ↑(Pᶜ) = (1 : M) - ↑P := rfl
 
-instance [has_faithful_scalar M X] : has_inf {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : has_inf {P : M // is_Lprojection X P} :=
 ⟨λ P Q, ⟨P * Q, P.prop.mul Q.prop⟩ ⟩
 
-@[simp] lemma coe_inf [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+@[simp] lemma coe_inf [has_faithful_smul M X] (P Q : {P : M // is_Lprojection X P}) :
   ↑(P ⊓ Q) = ((↑P : (M)) * ↑Q) := rfl
 
-instance [has_faithful_scalar M X] : has_sup {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : has_sup {P : M // is_Lprojection X P} :=
 ⟨λ P Q, ⟨P + Q - P * Q, P.prop.join Q.prop⟩ ⟩
 
-@[simp] lemma coe_sup [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+@[simp] lemma coe_sup [has_faithful_smul M X] (P Q : {P : M // is_Lprojection X P}) :
   ↑(P ⊔ Q) = ((↑P : M) + ↑Q - ↑P * ↑Q) := rfl
 
-instance [has_faithful_scalar M X] : has_sdiff {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : has_sdiff {P : M // is_Lprojection X P} :=
 ⟨λ P Q, ⟨P * (1 - Q), by exact P.prop.mul Q.prop.Lcomplement ⟩⟩
 
-@[simp] lemma coe_sdiff [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+@[simp] lemma coe_sdiff [has_faithful_smul M X] (P Q : {P : M // is_Lprojection X P}) :
   ↑(P \ Q) = (↑P : M) * (1 - ↑Q) := rfl
 
-instance [has_faithful_scalar M X] : partial_order {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : partial_order {P : M // is_Lprojection X P} :=
 { le := λ P Q, (↑P : M) = ↑(P ⊓ Q),
   le_refl := λ P, by simpa only [coe_inf, ←sq] using (P.prop.proj.eq).symm,
   le_trans := λ P Q R h₁ h₂, by { simp only [coe_inf] at ⊢ h₁ h₂, rw [h₁, mul_assoc, ←h₂] },
   le_antisymm := λ P Q h₁ h₂, subtype.eq (by convert (P.prop.commute Q.prop).eq) }
 
-lemma le_def [has_faithful_scalar M X] (P Q : {P : M // is_Lprojection X P}) :
+lemma le_def [has_faithful_smul M X] (P Q : {P : M // is_Lprojection X P}) :
   P ≤ Q ↔ (P : M) = ↑(P ⊓ Q) :=
 iff.rfl
 
@@ -206,16 +206,16 @@ instance : has_one {P : M // is_Lprojection X P} :=
 @[simp] lemma coe_one : ↑(1 : {P : M // is_Lprojection X P}) = (1 : M) :=
 rfl
 
-instance [has_faithful_scalar M X] : bounded_order {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : bounded_order {P : M // is_Lprojection X P} :=
 { top := 1,
   le_top := λ P, (mul_one (P : M)).symm,
   bot := 0,
   bot_le := λ P, (zero_mul (P : M)).symm, }
 
-@[simp] lemma coe_bot [has_faithful_scalar M X] :
+@[simp] lemma coe_bot [has_faithful_smul M X] :
   ↑(bounded_order.bot : {P : M // is_Lprojection X P}) = (0 : M) := rfl
 
-@[simp] lemma coe_top [has_faithful_scalar M X] :
+@[simp] lemma coe_top [has_faithful_smul M X] :
   ↑(bounded_order.top : {P : M // is_Lprojection X P}) = (1 : M) := rfl
 
 lemma compl_mul {P : {P : M // is_Lprojection X P}} {Q : M} :
@@ -225,7 +225,7 @@ lemma mul_compl_self {P : {P : M // is_Lprojection X P}} :
   (↑P : M) * (↑Pᶜ) = 0 :=
 by rw [coe_compl, mul_sub, mul_one, P.prop.proj.eq, sub_self]
 
-lemma distrib_lattice_lemma [has_faithful_scalar M X] {P Q R : {P : M // is_Lprojection X P}} :
+lemma distrib_lattice_lemma [has_faithful_smul M X] {P Q R : {P : M // is_Lprojection X P}} :
   ((↑P : M) + ↑Pᶜ * R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = (↑P + ↑Q * ↑R * ↑Pᶜ) :=
 by rw [add_mul, mul_add, mul_add, mul_assoc ↑Pᶜ ↑R (↑Q * ↑R * ↑Pᶜ), ← mul_assoc ↑R (↑Q * ↑R) ↑Pᶜ,
     ← coe_inf Q, (Pᶜ.prop.commute R.prop).eq, ((Q ⊓ R).prop.commute Pᶜ.prop).eq,
@@ -235,7 +235,7 @@ by rw [add_mul, mul_add, mul_add, mul_assoc ↑Pᶜ ↑R (↑Q * ↑R * ↑Pᶜ)
     P.prop.proj.eq, R.prop.proj.eq, ← coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute Pᶜ.prop).eq,
     ← mul_assoc, Pᶜ.prop.proj.eq]
 
-instance [has_faithful_scalar M X] : distrib_lattice {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : distrib_lattice {P : M // is_Lprojection X P} :=
 { le_sup_left := λ P Q, by rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc,
     P.prop.proj.eq, sub_self, add_zero],
   le_sup_right := λ P Q,
@@ -277,7 +277,7 @@ instance [has_faithful_scalar M X] : distrib_lattice {P : M // is_Lprojection X
   .. is_Lprojection.subtype.has_sup,
   .. is_Lprojection.subtype.partial_order }
 
-instance [has_faithful_scalar M X] : boolean_algebra {P : M // is_Lprojection X P} :=
+instance [has_faithful_smul M X] : boolean_algebra {P : M // is_Lprojection X P} :=
 { sup_inf_sdiff := λ P Q, subtype.ext $
     by rw [coe_sup, coe_inf, coe_sdiff, mul_assoc, ← mul_assoc ↑Q,
     (Q.prop.commute P.prop).eq, mul_assoc ↑P ↑Q, ← coe_compl, mul_compl_self, mul_zero, mul_zero,