refactor(algebra/opposites): use mul_opposite for multiplicative oppo…

…site (#10302)

Split out `mul_opposite` from `opposite`, to leave room for an `add_opposite` in future.

Multiplicative opposites are now spelt `Aᵐᵒᵖ` instead of `Aᵒᵖ`. `Aᵒᵖ` now refers to the categorical opposite.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/algebra/basic.lean

@@ -381,20 +381,20 @@ end field
 
 end no_zero_smul_divisors
 
-namespace opposite
+namespace mul_opposite
 
 variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
 
-instance : algebra R Aᵒᵖ :=
+instance : algebra R Aᵐᵒᵖ :=
 { to_ring_hom := (algebra_map R A).to_opposite $ λ x y, algebra.commutes _ _,
   smul_def' := λ c x, unop_injective $
     by { dsimp, simp only [op_mul, algebra.smul_def, algebra.commutes, op_unop] },
-  commutes' := λ r, opposite.rec $ λ x, by dsimp; simp only [← op_mul, algebra.commutes],
-  ..opposite.has_scalar A R }
+  commutes' := λ r, mul_opposite.rec $ λ x, by dsimp; simp only [← op_mul, algebra.commutes],
+  .. mul_opposite.has_scalar A R }
 
-@[simp] lemma algebra_map_apply (c : R) : algebra_map R Aᵒᵖ c = op (algebra_map R A c) := rfl
+@[simp] lemma algebra_map_apply (c : R) : algebra_map R Aᵐᵒᵖ c = op (algebra_map R A c) := rfl
 
-end opposite
+end mul_opposite
 
 namespace module
 variables (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M]

src/algebra/big_operators/basic.lean

@@ -126,8 +126,8 @@ lemma ring_hom.map_list_sum [non_assoc_semiring β] [non_assoc_semiring γ]
 f.to_add_monoid_hom.map_list_sum l
 
 /-- A morphism into the opposite ring acts on the product by acting on the reversed elements -/
-lemma ring_hom.unop_map_list_prod [semiring β] [semiring γ] (f : β →+* γᵒᵖ) (l : list β) :
-  opposite.unop (f l.prod) = (l.map (opposite.unop ∘ f)).reverse.prod :=
+lemma ring_hom.unop_map_list_prod [semiring β] [semiring γ] (f : β →+* γᵐᵒᵖ) (l : list β) :
+  mul_opposite.unop (f l.prod) = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
 f.to_monoid_hom.unop_map_list_prod l
 
 lemma ring_hom.map_multiset_prod [comm_semiring β] [comm_semiring γ] (f : β →+* γ)
@@ -1216,16 +1216,16 @@ end
 
 section opposite
 
-open opposite
+open mul_opposite
 
 /-- Moving to the opposite additive commutative monoid commutes with summing. -/
 @[simp] lemma op_sum [add_comm_monoid β] {s : finset α} (f : α → β) :
   op (∑ x in s, f x) = ∑ x in s, op (f x) :=
-(op_add_equiv : β ≃+ βᵒᵖ).map_sum _ _
+(op_add_equiv : β ≃+ βᵐᵒᵖ).map_sum _ _
 
-@[simp] lemma unop_sum [add_comm_monoid β] {s : finset α} (f : α → βᵒᵖ) :
+@[simp] lemma unop_sum [add_comm_monoid β] {s : finset α} (f : α → βᵐᵒᵖ) :
   unop (∑ x in s, f x) = ∑ x in s, unop (f x) :=
-(op_add_equiv : β ≃+ βᵒᵖ).symm.map_sum _ _
+(op_add_equiv : β ≃+ βᵐᵒᵖ).symm.map_sum _ _
 
 end opposite
 

src/algebra/free_algebra.lean

@@ -413,7 +413,7 @@ end
 
 /-- The star ring formed by reversing the elements of products -/
 instance : star_ring (free_algebra R X) :=
-{ star := opposite.unop ∘ lift R (opposite.op ∘ ι R),
+{ star := mul_opposite.unop ∘ lift R (mul_opposite.op ∘ ι R),
   star_involutive := λ x, by
   { unfold has_star.star,
     simp only [function.comp_apply],
@@ -430,7 +430,7 @@ lemma star_algebra_map (r : R) : star (algebra_map R (free_algebra R X) r) = (al
 by simp [star, has_star.star]
 
 /-- `star` as an `alg_equiv` -/
-def star_hom : free_algebra R X ≃ₐ[R] (free_algebra R X)ᵒᵖ :=
+def star_hom : free_algebra R X ≃ₐ[R] (free_algebra R X)ᵐᵒᵖ :=
 { commutes' := λ r, by simp [star_algebra_map],
   ..star_ring_equiv }
 

src/algebra/geom_sum.lean

@@ -37,7 +37,7 @@ are recorded.
 universe u
 variable {α : Type u}
 
-open finset opposite
+open finset mul_opposite
 
 open_locale big_operators
 
@@ -152,7 +152,7 @@ end
 lemma commute.mul_neg_geom_sum₂ [ring α] {x y : α} (h : commute x y) (n : ℕ) :
   (y - x) * (geom_sum₂ x y n) = y ^ n - x ^ n :=
 begin
-  rw ← op_inj_iff,
+  apply op_injective,
   simp only [op_mul, op_sub, op_geom_sum₂, op_pow],
   exact (commute.op h.symm).geom_sum₂_mul n
 end
@@ -175,10 +175,7 @@ end
 
 lemma mul_geom_sum [ring α] (x : α) (n : ℕ) :
   (x - 1) * (geom_sum x n) = x ^ n - 1 :=
-begin
-  rw ← op_inj_iff,
-  simpa using geom_sum_mul (op x) n,
-end
+op_injective $ by simpa using geom_sum_mul (op x) n
 
 theorem geom_sum_mul_neg [ring α] (x : α) (n : ℕ) :
   (geom_sum x n) * (1 - x) = 1 - x ^ n :=
@@ -190,10 +187,7 @@ end
 
 lemma mul_neg_geom_sum [ring α] (x : α) (n : ℕ) :
   (1 - x) * (geom_sum x n) = 1 - x ^ n :=
-begin
-  rw ← op_inj_iff,
-  simpa using geom_sum_mul_neg (op x) n,
-end
+op_injective $ by simpa using geom_sum_mul_neg (op x) n
 
 protected theorem commute.geom_sum₂ [division_ring α] {x y : α} (h' : commute x y) (h : x ≠ y)
   (n : ℕ) : (geom_sum₂ x y n) = (x ^ n - y ^ n) / (x - y) :=
@@ -256,7 +250,7 @@ protected theorem commute.geom_sum₂_Ico_mul [ring α] {x y : α} (h : commute
   (hmn : m ≤ n) :
   (∑ i in finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n -  y ^ (n - m) * x ^ m :=
 begin
-  rw ← op_inj_iff,
+  apply op_injective,
   simp only [op_sub, op_mul, op_pow, op_sum],
   have : ∑ k in Ico m n, op y ^ (n - 1 - k) * op x ^ k
     = ∑ k in Ico m n, op x ^ k * op y ^ (n - 1 - k),

src/algebra/group/prod.lean

@@ -337,11 +337,11 @@ end mul_equiv
 
 section units
 
-open opposite
+open mul_opposite
 
-/-- Canonical homomorphism of monoids from `units α` into `α × αᵒᵖ`.
+/-- Canonical homomorphism of monoids from `units α` into `α × αᵐᵒᵖ`.
 Used mainly to define the natural topology of `units α`. -/
-def embed_product (α : Type*) [monoid α] : units α →* α × αᵒᵖ :=
+def embed_product (α : Type*) [monoid α] : units α →* α × αᵐᵒᵖ :=
 { to_fun := λ x, ⟨x, op ↑x⁻¹⟩,
   map_one' := by simp only [one_inv, eq_self_iff_true, units.coe_one, op_one, prod.mk_eq_one,
     and_self],

src/algebra/group_power/lemmas.lean

@@ -915,14 +915,14 @@ lemma conj_pow' (u : units M) (x : M) (n : ℕ) : (↑(u⁻¹) * x * u)^n = ↑(
 
 end units
 
-namespace opposite
+namespace mul_opposite
 
 /-- Moving to the opposite monoid commutes with taking powers. -/
 @[simp] lemma op_pow [monoid M] (x : M) (n : ℕ) : op (x ^ n) = (op x) ^ n := rfl
-@[simp] lemma unop_pow [monoid M] (x : Mᵒᵖ) (n : ℕ) : unop (x ^ n) = (unop x) ^ n := rfl
+@[simp] lemma unop_pow [monoid M] (x : Mᵐᵒᵖ) (n : ℕ) : unop (x ^ n) = (unop x) ^ n := rfl
 
 /-- Moving to the opposite group or group_with_zero commutes with taking powers. -/
 @[simp] lemma op_zpow [div_inv_monoid M] (x : M) (z : ℤ) : op (x ^ z) = (op x) ^ z := rfl
-@[simp] lemma unop_zpow [div_inv_monoid M] (x : Mᵒᵖ) (z : ℤ) : unop (x ^ z) = (unop x) ^ z := rfl
+@[simp] lemma unop_zpow [div_inv_monoid M] (x : Mᵐᵒᵖ) (z : ℤ) : unop (x ^ z) = (unop x) ^ z := rfl
 
-end opposite
+end mul_opposite

src/algebra/hierarchy_design.lean

@@ -67,10 +67,10 @@ when applicable:
   ```
   instance pi.Z [∀ i, Z $ f i] : Z (Π i : I, f i) := ...
   ```
-* Instances transferred to `opposite M`, like `opposite.monoid`.
+* Instances transferred to `mul_opposite M`, like `mul_opposite.monoid`.
   See `algebra.opposites` for more examples.
   ```
-  instance opposite.Z [Z M] : Z (opposite M) := ...
+  instance mul_opposite.Z [Z M] : Z (mul_opposite M) := ...
   ```
 * Instances transferred to `ulift M`, like `ulift.monoid`.
   See `algebra.group.ulift` for more examples.

src/algebra/module/basic.lean

@@ -251,7 +251,7 @@ instance semiring.to_module [semiring R] : module R R :=
 
 /-- Like `semiring.to_module`, but multiplies on the right. -/
 @[priority 910] -- see Note [lower instance priority]
-instance semiring.to_opposite_module [semiring R] : module Rᵒᵖ R :=
+instance semiring.to_opposite_module [semiring R] : module Rᵐᵒᵖ R :=
 { smul_add := λ r x y, add_mul _ _ _,
   add_smul := λ r x y, mul_add _ _ _,
   ..monoid_with_zero.to_opposite_mul_action_with_zero R}

src/algebra/module/opposites.lean

@@ -7,40 +7,40 @@ import algebra.opposites
 import data.equiv.module
 
 /-!
-# Module operations on `Mᵒᵖ`
+# Module operations on `Mᵐᵒᵖ`
 
 This file contains definitions that could not be placed into `algebra.opposites` due to import
 cycles.
 -/
 
-namespace opposite
+namespace mul_opposite
 universes u v
 
 variables (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
 
-/-- `opposite.distrib_mul_action` extends to a `module` -/
-instance : module R (opposite M) :=
+/-- `mul_opposite.distrib_mul_action` extends to a `module` -/
+instance : module R (mul_opposite M) :=
 { add_smul := λ r₁ r₂ x, unop_injective $ add_smul r₁ r₂ (unop x),
   zero_smul := λ x, unop_injective $ zero_smul _ (unop x),
-  ..opposite.distrib_mul_action M R }
+  ..mul_opposite.distrib_mul_action M R }
 
 /-- The function `op` is a linear equivalence. -/
-def op_linear_equiv : M ≃ₗ[R] Mᵒᵖ :=
-{ map_smul' := opposite.op_smul, .. op_add_equiv }
+def op_linear_equiv : M ≃ₗ[R] Mᵐᵒᵖ :=
+{ map_smul' := mul_opposite.op_smul, .. op_add_equiv }
 
 @[simp] lemma coe_op_linear_equiv :
-  (op_linear_equiv R : M → Mᵒᵖ) = op := rfl
+  (op_linear_equiv R : M → Mᵐᵒᵖ) = op := rfl
 @[simp] lemma coe_op_linear_equiv_symm :
-  ((op_linear_equiv R).symm : Mᵒᵖ → M) = unop := rfl
+  ((op_linear_equiv R).symm : Mᵐᵒᵖ → M) = unop := rfl
 
 @[simp] lemma coe_op_linear_equiv_to_linear_map :
-  ((op_linear_equiv R).to_linear_map : M → Mᵒᵖ) = op := rfl
+  ((op_linear_equiv R).to_linear_map : M → Mᵐᵒᵖ) = op := rfl
 @[simp] lemma coe_op_linear_equiv_symm_to_linear_map :
-  ((op_linear_equiv R).symm.to_linear_map : Mᵒᵖ → M) = unop := rfl
+  ((op_linear_equiv R).symm.to_linear_map : Mᵐᵒᵖ → M) = unop := rfl
 
 @[simp] lemma op_linear_equiv_to_add_equiv :
-  (op_linear_equiv R : M ≃ₗ[R] Mᵒᵖ).to_add_equiv = op_add_equiv := rfl
+  (op_linear_equiv R : M ≃ₗ[R] Mᵐᵒᵖ).to_add_equiv = op_add_equiv := rfl
 @[simp] lemma op_linear_equiv_symm_to_add_equiv :
-  (op_linear_equiv R : M ≃ₗ[R] Mᵒᵖ).symm.to_add_equiv = op_add_equiv.symm := rfl
+  (op_linear_equiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm.to_add_equiv = op_add_equiv.symm := rfl
 
-end opposite
+end mul_opposite

src/algebra/monoid_algebra/basic.lean

@@ -739,28 +739,28 @@ end span
 
 section opposite
 
-open finsupp opposite
+open finsupp mul_opposite
 
 variables [semiring k]
 
 /-- The opposite of an `monoid_algebra R I` equivalent as a ring to
-the `monoid_algebra Rᵒᵖ Iᵒᵖ` over the opposite ring, taking elements to their opposite. -/
+the `monoid_algebra Rᵐᵒᵖ Iᵐᵒᵖ` over the opposite ring, taking elements to their opposite. -/
 @[simps {simp_rhs := tt}] protected noncomputable def op_ring_equiv [monoid G] :
-  (monoid_algebra k G)ᵒᵖ ≃+* monoid_algebra kᵒᵖ Gᵒᵖ :=
+  (monoid_algebra k G)ᵐᵒᵖ ≃+* monoid_algebra kᵐᵒᵖ Gᵐᵒᵖ :=
 { map_mul' := begin
     dsimp only [add_equiv.to_fun_eq_coe, ←add_equiv.coe_to_add_monoid_hom],
     rw add_monoid_hom.map_mul_iff,
     ext i₁ r₁ i₂ r₂ : 6,
     simp
   end,
-  ..op_add_equiv.symm.trans $ (finsupp.map_range.add_equiv (op_add_equiv : k ≃+ kᵒᵖ)).trans $
-    finsupp.dom_congr equiv_to_opposite }
+  ..op_add_equiv.symm.trans $ (finsupp.map_range.add_equiv (op_add_equiv : k ≃+ kᵐᵒᵖ)).trans $
+    finsupp.dom_congr op_equiv }
 
 @[simp] lemma op_ring_equiv_single [monoid G] (r : k) (x : G) :
   monoid_algebra.op_ring_equiv (op (single x r)) = single (op x) (op r) :=
 by simp
 
-@[simp] lemma op_ring_equiv_symm_single [monoid G] (r : kᵒᵖ) (x : Gᵒᵖ) :
+@[simp] lemma op_ring_equiv_symm_single [monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
   monoid_algebra.op_ring_equiv.symm (single x r) = op (single x.unop r.unop) :=
 by simp
 
@@ -1242,29 +1242,29 @@ ring_hom_ext (ring_hom.congr_fun h₁) (monoid_hom.congr_fun h_of)
 
 section opposite
 
-open finsupp opposite
+open finsupp mul_opposite
 
 variables [semiring k]
 
 /-- The opposite of an `add_monoid_algebra R I` is ring equivalent to
-the `add_monoid_algebra Rᵒᵖ I` over the opposite ring, taking elements to their opposite. -/
+the `add_monoid_algebra Rᵐᵒᵖ I` over the opposite ring, taking elements to their opposite. -/
 @[simps {simp_rhs := tt}] protected noncomputable def op_ring_equiv [add_comm_monoid G] :
-  (add_monoid_algebra k G)ᵒᵖ ≃+* add_monoid_algebra kᵒᵖ G :=
+  (add_monoid_algebra k G)ᵐᵒᵖ ≃+* add_monoid_algebra kᵐᵒᵖ G :=
 { map_mul' := begin
     dsimp only [add_equiv.to_fun_eq_coe, ←add_equiv.coe_to_add_monoid_hom],
     rw add_monoid_hom.map_mul_iff,
     ext i r i' r' : 6,
     dsimp,
     simp only [map_range_single, single_mul_single, ←op_mul, add_comm]
   end,
-  ..opposite.op_add_equiv.symm.trans
-    (finsupp.map_range.add_equiv (opposite.op_add_equiv : k ≃+ kᵒᵖ))}
+  ..mul_opposite.op_add_equiv.symm.trans
+    (finsupp.map_range.add_equiv (mul_opposite.op_add_equiv : k ≃+ kᵐᵒᵖ))}
 
 @[simp] lemma op_ring_equiv_single [add_comm_monoid G] (r : k) (x : G) :
   add_monoid_algebra.op_ring_equiv (op (single x r)) = single x (op r) :=
 by simp
 
-@[simp] lemma op_ring_equiv_symm_single [add_comm_monoid G] (r : kᵒᵖ) (x : Gᵒᵖ) :
+@[simp] lemma op_ring_equiv_symm_single [add_comm_monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
   add_monoid_algebra.op_ring_equiv.symm (single x r) = op (single x r.unop) :=
 by simp