refactor(algebra/*): move commute below ring in imports (#2973)

Fixes #1865

API changes:

* drop lemmas about unbundled `center`;
* add `to_additive` to `semiconj_by` and `commute`;
* drop `inv_comm_of_comm` in favor of `commute.left_inv`,
  same with `inv_comm_of_comm` and `commute.left_inv'`;
* rename `monoid_hom.map_commute` to `commute.map`, same with
  `semiconj_by`;
* drop `commute.cast_*_*` and `nat/int/rat.mul_cast_comm`, add
  `nat/int/rat.cast_commute` and `nat.int.rat.commute_cast`;
* add `commute.mul_fpow`.

Author: urkud

src/algebra/commute.lean

@@ -5,8 +5,8 @@ Authors: Neil Strickland
 
 Sums of finite geometric series
 -/
-import algebra.commute
 import algebra.group_with_zero_power
+import algebra.big_operators
 
 universe u
 variable {α : Type u}

src/algebra/geom_sum.lean

@@ -194,14 +194,6 @@ by rw [mul_eq_one_iff_eq_inv, inv_inv]
 theorem inv_mul_eq_one : a⁻¹ * b = 1 ↔ a = b :=
 by rw [mul_eq_one_iff_eq_inv, inv_inj']
 
-@[to_additive]
-theorem inv_comm_of_comm (H : a * b = b * a) : a⁻¹ * b = b * a⁻¹ :=
-begin
-  have : a⁻¹ * (b * a) * a⁻¹ = a⁻¹ * (a * b) * a⁻¹ :=
-    congr_arg (λ x:G, a⁻¹ * x * a⁻¹) H.symm,
-  rwa [inv_mul_cancel_left, mul_assoc, mul_inv_cancel_right] at this
-end
-
 @[simp, to_additive]
 lemma mul_left_eq_self : a * b = b ↔ a = 1 :=
 ⟨λ h, @mul_right_cancel _ _ a b 1 (by simp [h]), λ h, by simp [h]⟩

src/algebra/group/basic.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2019 Neil Strickland. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Neil Strickland, Yury Kudryashov
+-/
+import algebra.group.semiconj
+
+/-!
+# Commuting pairs of elements in monoids
+
+We define the predicate `commute a b := a * b = b * a` and provide some operations on terms `(h :
+commute a b)`. E.g., if `a`, `b`, and c are elements of a semiring, and that `hb : commute a b` and
+`hc : commute a c`.  Then `hb.pow_left 5` proves `commute (a ^ 5) b` and `(hb.pow_right 2).add_right
+(hb.mul_right hc)` proves `commute a (b ^ 2 + b * c)`.
+
+Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like
+`rw [(hb.pow_left 5).eq]` rather than just `rw [hb.pow_left 5]`.
+
+This file defines only a few operations (`mul_left`, `inv_right`, etc).  Other operations
+(`pow_right`, field inverse etc) are in the files that define corresponding notions.
+
+## Implementation details
+
+Most of the proofs come from the properties of `semiconj_by`.
+-/
+
+/-- Two elements commute if `a * b = b * a`. -/
+@[to_additive add_commute "Two elements additively commute if `a + b = b + a`"]
+def commute {S : Type*} [has_mul S] (a b : S) : Prop := semiconj_by a b b
+
+namespace commute
+
+section has_mul
+
+variables {S : Type*} [has_mul S]
+
+/-- Equality behind `commute a b`; useful for rewriting. -/
+@[to_additive] protected theorem eq {a b : S} (h : commute a b) : a * b = b * a := h
+
+/-- Any element commutes with itself. -/
+@[refl, simp, to_additive] protected theorem refl (a : S) : commute a a := eq.refl (a * a)
+
+/-- If `a` commutes with `b`, then `b` commutes with `a`. -/
+@[symm, to_additive] protected theorem symm {a b : S} (h : commute a b) : commute b a :=
+eq.symm h
+
+@[to_additive]
+protected theorem symm_iff {a b : S} : commute a b ↔ commute b a :=
+⟨commute.symm, commute.symm⟩
+
+end has_mul
+
+section semigroup
+
+variables {S : Type*} [semigroup S] {a b c : S}
+
+/-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
+@[simp, to_additive] theorem mul_right (hab : commute a b) (hac : commute a c) :
+  commute a (b * c) :=
+hab.mul_right hac
+
+/-- If both `a` and `b` commute with `c`, then their product commutes with `c`. -/
+@[simp, to_additive] theorem mul_left (hac : commute a c) (hbc : commute b c) :
+  commute (a * b) c :=
+hac.mul_left hbc
+
+@[to_additive] protected lemma right_comm (h : commute b c) (a : S) :
+  a * b * c = a * c * b :=
+by simp only [mul_assoc, h.eq]
+
+@[to_additive] protected lemma left_comm (h : commute a b) (c) :
+  a * (b * c) = b * (a * c) :=
+by simp only [← mul_assoc, h.eq]
+
+end semigroup
+
+@[to_additive]
+protected theorem all {S : Type*} [comm_semigroup S] (a b : S) : commute a b := mul_comm a b
+
+section monoid
+
+variables {M : Type*} [monoid M]
+
+@[simp, to_additive] theorem one_right (a : M) : commute a 1 := semiconj_by.one_right a
+@[simp, to_additive] theorem one_left (a : M) : commute 1 a := semiconj_by.one_left a
+
+@[to_additive] theorem units_inv_right {a : M} {u : units M} : commute a u → commute a ↑u⁻¹ :=
+semiconj_by.units_inv_right
+
+@[simp, to_additive] theorem units_inv_right_iff {a : M} {u : units M} :
+  commute a ↑u⁻¹ ↔ commute a u :=
+semiconj_by.units_inv_right_iff
+
+@[to_additive] theorem units_inv_left {u : units M} {a : M} : commute ↑u a → commute ↑u⁻¹ a :=
+semiconj_by.units_inv_symm_left
+
+@[simp, to_additive]
+theorem units_inv_left_iff {u : units M} {a : M}: commute ↑u⁻¹ a ↔ commute ↑u a :=
+semiconj_by.units_inv_symm_left_iff
+
+variables {u₁ u₂ : units M}
+
+@[to_additive]
+theorem units_coe : commute u₁ u₂ → commute (u₁ : M) u₂ := semiconj_by.units_coe
+@[to_additive]
+theorem units_of_coe : commute (u₁ : M) u₂ → commute u₁ u₂ := semiconj_by.units_of_coe
+@[simp, to_additive]
+theorem units_coe_iff : commute (u₁ : M) u₂ ↔ commute u₁ u₂ := semiconj_by.units_coe_iff
+
+end monoid
+
+section group
+
+variables {G : Type*} [group G] {a b : G}
+
+@[to_additive]
+theorem inv_right : commute a b → commute a b⁻¹ := semiconj_by.inv_right
+@[simp, to_additive]
+theorem inv_right_iff : commute a b⁻¹ ↔ commute a b := semiconj_by.inv_right_iff
+
+@[to_additive] theorem inv_left :  commute a b → commute a⁻¹ b := semiconj_by.inv_symm_left
+@[simp, to_additive]
+theorem inv_left_iff : commute a⁻¹ b ↔ commute a b := semiconj_by.inv_symm_left_iff
+
+@[to_additive]
+theorem inv_inv : commute a b → commute a⁻¹ b⁻¹ := semiconj_by.inv_inv_symm
+@[simp, to_additive]
+theorem inv_inv_iff : commute a⁻¹ b⁻¹ ↔ commute a b := semiconj_by.inv_inv_symm_iff
+
+end group
+
+end commute

src/algebra/group/commute.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
   Johannes Hölzl, Yury Kudryashov
 -/
-import algebra.group.basic
+import algebra.group.commute
 import tactic.ext
 
 /-!
@@ -294,3 +294,17 @@ namespace add_monoid_hom
   f (g - h) = (f g) - (f h) := f.map_add_neg g h
 
 end add_monoid_hom
+
+section commute
+
+variables [monoid M] [monoid N] {a x y : M}
+
+@[simp, to_additive]
+protected lemma semiconj_by.map (h : semiconj_by a x y) (f : M →* N) :
+  semiconj_by (f a) (f x) (f y) :=
+by simpa only [semiconj_by, f.map_mul] using congr_arg f h
+
+@[simp, to_additive]
+protected lemma commute.map (h : commute x y) (f : M →* N) : commute (f x) (f y) := h.map f
+
+end commute

src/algebra/group/hom.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+Some proofs and docs came from `algebra/commute` (c) Neil Strickland
+-/
+import algebra.group.units
+import tactic.rewrite
+
+/-!
+# Semiconjugate elements of a semigroup
+
+## Main definitions
+
+We say that `x` is semiconjugate to `y` by `a` (`semiconj_by a x y`), if `a * x = y * a`.
+In this file we  provide operations on `semiconj_by _ _ _`.
+
+In the names of these operations, we treat `a` as the “left” argument, and both `x` and `y` as
+“right” arguments. This way most names in this file agree with the names of the corresponding lemmas
+for `commute a b = semiconj_by a b b`. As a side effect, some lemmas have only `_right` version.
+
+Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like
+`rw [(h.pow_right 5).eq]` rather than just `rw [h.pow_right 5]`.
+
+This file provides only basic operations (`mul_left`, `mul_right`, `inv_right` etc). Other
+operations (`pow_right`, field inverse etc) are in the files that define corresponding notions.
+-/
+
+universes u v
+
+/-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/
+@[to_additive add_semiconj_by "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"]
+def semiconj_by {M : Type u} [has_mul M] (a x y : M) : Prop := a * x = y * a
+
+namespace semiconj_by
+
+/-- Equality behind `semiconj_by a x y`; useful for rewriting. -/
+@[to_additive]
+protected lemma eq {S : Type u} [has_mul S] {a x y : S} (h : semiconj_by a x y) :
+  a * x = y * a := h
+
+section semigroup
+
+variables {S : Type u} [semigroup S] {a b x y z x' y' : S}
+
+/-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
+then it semiconjugates `x * x'` to `y * y'`. -/
+@[to_additive, simp] lemma mul_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
+  semiconj_by a (x * x') (y * y') :=
+by unfold semiconj_by; assoc_rw [h.eq, h'.eq]
+
+/-- If both `a` and `b` semiconjugate `x` to `y`, then so does `a * b`. -/
+@[to_additive]
+lemma mul_left (ha : semiconj_by a y z) (hb : semiconj_by b x y) :
+  semiconj_by (a * b) x z :=
+by unfold semiconj_by; assoc_rw [hb.eq, ha.eq, mul_assoc]
+
+end semigroup
+
+section monoid
+
+variables {M : Type u} [monoid M]
+
+/-- Any element semiconjugates `1` to `1`. -/
+@[simp, to_additive]
+lemma one_right (a : M) : semiconj_by a 1 1 := by rw [semiconj_by, mul_one, one_mul]
+
+/-- One semiconjugates any element to itself. -/
+@[simp, to_additive]
+lemma one_left (x : M) : semiconj_by 1 x x := eq.symm $ one_right x
+
+/-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `x⁻¹` to `y⁻¹`. -/
+@[to_additive] lemma units_inv_right {a : M} {x y : units M} (h : semiconj_by a x y) :
+  semiconj_by a ↑x⁻¹ ↑y⁻¹ :=
+calc a * ↑x⁻¹ = ↑y⁻¹ * (y * a) * ↑x⁻¹ : by rw [units.inv_mul_cancel_left]
+          ... = ↑y⁻¹ * a              : by rw [← h.eq, mul_assoc, units.mul_inv_cancel_right]
+
+@[simp, to_additive] lemma units_inv_right_iff {a : M} {x y : units M} :
+  semiconj_by a ↑x⁻¹ ↑y⁻¹ ↔ semiconj_by a x y :=
+⟨units_inv_right, units_inv_right⟩
+
+/-- If a unit `a` semiconjugates `x` to `y`, then `a⁻¹` semiconjugates `y` to `x`. -/
+@[to_additive] lemma units_inv_symm_left {a : units M} {x y : M} (h : semiconj_by ↑a x y) :
+  semiconj_by ↑a⁻¹ y x :=
+calc ↑a⁻¹ * y = ↑a⁻¹ * (y * a * ↑a⁻¹) : by rw [units.mul_inv_cancel_right]
+          ... = x * ↑a⁻¹              : by rw [← h.eq, ← mul_assoc, units.inv_mul_cancel_left]
+
+@[simp, to_additive] lemma units_inv_symm_left_iff {a : units M} {x y : M} :
+  semiconj_by ↑a⁻¹ y x ↔ semiconj_by ↑a x y :=
+⟨units_inv_symm_left, units_inv_symm_left⟩
+
+@[to_additive] theorem units_coe {a x y : units M} (h : semiconj_by a x y) :
+  semiconj_by (a : M) x y :=
+congr_arg units.val h
+
+@[to_additive] theorem units_of_coe {a x y : units M} (h : semiconj_by (a : M) x y) :
+  semiconj_by a x y :=
+units.ext h
+
+@[simp, to_additive] theorem units_coe_iff {a x y : units M} :
+  semiconj_by (a : M) x y ↔ semiconj_by a x y :=
+⟨units_of_coe, units_coe⟩
+
+end monoid
+
+section group
+
+variables {G : Type u} [group G] {a x y : G}
+
+@[simp, to_additive] lemma inv_right_iff : semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y :=
+@units_inv_right_iff G _ a ⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩
+  ⟨y, y⁻¹, mul_inv_self y, inv_mul_self y⟩
+
+@[to_additive] lemma inv_right : semiconj_by a x y → semiconj_by a x⁻¹ y⁻¹ :=
+inv_right_iff.2
+
+@[simp, to_additive] lemma inv_symm_left_iff : semiconj_by a⁻¹ y x ↔ semiconj_by a x y :=
+@units_inv_symm_left_iff G _ ⟨a, a⁻¹, mul_inv_self a, inv_mul_self a⟩ _ _
+
+@[to_additive] lemma inv_symm_left : semiconj_by a x y → semiconj_by a⁻¹ y x :=
+inv_symm_left_iff.2
+
+@[to_additive] lemma inv_inv_symm (h : semiconj_by a x y) : semiconj_by a⁻¹ y⁻¹ x⁻¹ :=
+h.inv_right.inv_symm_left
+
+-- this is not a simp lemma because it can be deduced from other simp lemmas
+@[to_additive] lemma inv_inv_symm_iff : semiconj_by a⁻¹ y⁻¹ x⁻¹ ↔ semiconj_by a x y :=
+inv_right_iff.trans inv_symm_left_iff
+
+/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
+@[to_additive] lemma conj_mk (a x : G) : semiconj_by a x (a * x * a⁻¹) :=
+by unfold semiconj_by; rw [mul_assoc, inv_mul_self, mul_one]
+
+end group
+
+end semiconj_by
+
+/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
+@[to_additive]
+lemma units.mk_semiconj_by {M : Type u} [monoid M] (u : units M) (x : M) :
+  semiconj_by ↑u x (u * x * ↑u⁻¹) :=
+by unfold semiconj_by; rw [units.inv_mul_cancel_right]