feat(algebra/{group,hom}/units): Units in division monoids (#14212)

Copy over `group_with_zero` lemmas to the more general setting of `division_monoid`.

src/algebra/group/units.lean

@@ -25,6 +25,8 @@ resembling the notation $R^{\times}$ for the units of a ring, which is common in
 
 -/
 
+open function
+
 universe u
 variable {α : Type u}
 
@@ -126,7 +128,15 @@ ext hv
   inv := has_inv.inv,
   mul_left_inv := λ u, ext u.inv_val }
 
-variables (a b : αˣ) {c : αˣ}
+@[to_additive] instance {α} [comm_monoid α] : comm_group αˣ :=
+{ mul_comm := λ u₁ u₂, ext $ mul_comm _ _, ..units.group }
+
+@[to_additive] instance : inhabited αˣ := ⟨1⟩
+
+@[to_additive] instance [has_repr α] : has_repr αˣ := ⟨repr ∘ val⟩
+
+variables (a b c : αˣ) {u : αˣ}
+
 @[simp, norm_cast, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
 
 @[simp, norm_cast, to_additive] lemma coe_one : ((1 : αˣ) : α) = 1 := rfl
@@ -143,11 +153,8 @@ by rw [←units.coe_one, eq_iff]
 @[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
 @[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _
 
-@[to_additive] lemma inv_mul_of_eq {u : αˣ} {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1 :=
-by { rw [←h, u.inv_mul], }
-
-@[to_additive] lemma mul_inv_of_eq {u : αˣ} {a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1 :=
-by { rw [←h, u.mul_inv], }
+@[to_additive] lemma inv_mul_of_eq {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1 := by rw [←h, u.inv_mul]
+@[to_additive] lemma mul_inv_of_eq {a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1 := by rw [←h, u.mul_inv]
 
 @[simp, to_additive] lemma mul_inv_cancel_left (a : αˣ) (b : α) : (a:α) * (↑a⁻¹ * b) = b :=
 by rw [← mul_assoc, mul_inv, one_mul]
@@ -161,13 +168,6 @@ by rw [mul_assoc, mul_inv, mul_one]
 @[simp, to_additive] lemma inv_mul_cancel_right (a : α) (b : αˣ) : a * ↑b⁻¹ * b = a :=
 by rw [mul_assoc, inv_mul, mul_one]
 
-@[to_additive] instance : inhabited αˣ := ⟨1⟩
-
-@[to_additive] instance {α} [comm_monoid α] : comm_group αˣ :=
-{ mul_comm := λ u₁ u₂, ext $ mul_comm _ _, ..units.group }
-
-@[to_additive] instance [has_repr α] : has_repr αˣ := ⟨repr ∘ val⟩
-
 @[simp, to_additive] theorem mul_right_inj (a : αˣ) {b c : α} : (a:α) * b = a * c ↔ b = c :=
 ⟨λ h, by simpa only [inv_mul_cancel_left] using congr_arg ((*) ↑(a⁻¹ : αˣ)) h, congr_arg _⟩
 
@@ -186,16 +186,34 @@ by rw [mul_assoc, inv_mul, mul_one]
 @[to_additive] theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
 ⟨λ h, by rw [← h, inv_mul_cancel_right], λ h, by rw [h, mul_inv_cancel_right]⟩
 
-@[to_additive] lemma inv_eq_of_mul_eq_one_right {u : αˣ} {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
+@[to_additive] protected lemma inv_eq_of_mul_eq_one_left {a : α} (h : a * u = 1) : ↑u⁻¹ = a :=
+calc ↑u⁻¹ = 1 * ↑u⁻¹ : by rw one_mul
+      ... = a : by rw [←h, mul_inv_cancel_right]
+
+@[to_additive] protected lemma inv_eq_of_mul_eq_one_right {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
 calc ↑u⁻¹ = ↑u⁻¹ * 1 : by rw mul_one
-      ... = ↑u⁻¹ * ↑u * a : by rw [←h, ←mul_assoc]
-      ... = a : by rw [u.inv_mul, one_mul]
+      ... = a : by rw [←h, inv_mul_cancel_left]
+
+@[to_additive] protected lemma eq_inv_of_mul_eq_one_left {a : α} (h : ↑u * a = 1) : a = ↑u⁻¹ :=
+(units.inv_eq_of_mul_eq_one_right h).symm
+
+@[to_additive] protected lemma eq_inv_of_mul_eq_one_right {a : α} (h : a * u = 1) : a = ↑u⁻¹ :=
+(units.inv_eq_of_mul_eq_one_left h).symm
+
+@[simp, to_additive] lemma mul_inv_eq_one {a : α} : a * ↑u⁻¹ = 1 ↔ a = u :=
+⟨inv_inv u ▸ units.eq_inv_of_mul_eq_one_right, λ h, mul_inv_of_eq h.symm⟩
+
+@[simp, to_additive] lemma inv_mul_eq_one {a : α} : ↑u⁻¹ * a = 1 ↔ ↑u = a :=
+⟨inv_inv u ▸ units.inv_eq_of_mul_eq_one_right, inv_mul_of_eq⟩
 
-@[to_additive] lemma eq_iff_inv_mul {u : αˣ} {a : α} : ↑u = a ↔ ↑u⁻¹ * a = 1 :=
-⟨inv_mul_of_eq, inv_inv u ▸ inv_eq_of_mul_eq_one_right⟩
+@[to_additive] lemma mul_eq_one_iff_eq_inv {a : α} : a * u = 1 ↔ a = ↑u⁻¹ :=
+by rw [←mul_inv_eq_one, inv_inv]
+
+@[to_additive] lemma mul_eq_one_iff_inv_eq {a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a :=
+by rw [←inv_mul_eq_one, inv_inv]
 
 lemma inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
-inv_eq_of_mul_eq_one_right $ by rw [h, u₂.mul_inv]
+units.inv_eq_of_mul_eq_one_right $ by rw [h, u₂.mul_inv]
 
 end units
 
@@ -368,17 +386,11 @@ lemma is_unit.mul_iff [comm_monoid M] {x y : M} : is_unit (x * y) ↔ is_unit x
 ⟨λ h, ⟨is_unit_of_mul_is_unit_left h, is_unit_of_mul_is_unit_right h⟩,
   λ h, is_unit.mul h.1 h.2⟩
 
-@[to_additive] theorem is_unit.mul_right_inj [monoid M] {a b c : M} (ha : is_unit a) :
-  a * b = a * c ↔ b = c :=
-by cases ha with a ha; rw [←ha, units.mul_right_inj]
-
-@[to_additive] theorem is_unit.mul_left_inj [monoid M] {a b c : M} (ha : is_unit a) :
-  b * a = c * a ↔ b = c :=
-by cases ha with a ha; rw [←ha, units.mul_left_inj]
-
-/-- The element of the group of units, corresponding to an element of a monoid which is a unit. -/
+/-- The element of the group of units, corresponding to an element of a monoid which is a unit. When
+`α` is a `division_monoid`, use `is_unit.unit'` instead. -/
 @[to_additive "The element of the additive group of additive units, corresponding to an element of
-an additive monoid which is an additive unit."]
+an additive monoid which is an additive unit. When `α` is a `subtraction_monoid`, use
+`is_add_unit.add_unit'` instead."]
 noncomputable def is_unit.unit [monoid M] {a : M} (h : is_unit a) : Mˣ :=
 (classical.some h).copy a (classical.some_spec h).symm _ rfl
 
@@ -403,6 +415,28 @@ begin
   simp [h.unit_spec]
 end
 
+section monoid
+variables [monoid M] {a b c : M}
+
+@[to_additive] lemma is_unit.mul_left_inj (h : is_unit a) : b * a = c * a ↔ b = c :=
+let ⟨u, hu⟩ := h in hu ▸ u.mul_left_inj
+
+@[to_additive] lemma is_unit.mul_right_inj (h : is_unit a) : a * b = a * c ↔ b = c :=
+let ⟨u, hu⟩ := h in hu ▸ u.mul_right_inj
+
+@[to_additive] protected lemma is_unit.mul_left_cancel (h : is_unit a) : a * b = a * c → b = c :=
+h.mul_right_inj.1
+
+@[to_additive] protected lemma is_unit.mul_right_cancel (h : is_unit b) : a * b = c * b → a = c :=
+h.mul_left_inj.1
+
+@[to_additive] protected lemma is_unit.mul_right_injective (h : is_unit a) : injective ((*) a) :=
+λ _ _, h.mul_left_cancel
+
+@[to_additive] protected lemma is_unit.mul_left_injective (h : is_unit b) : injective (* b) :=
+λ _ _, h.mul_right_cancel
+
+end monoid
 end is_unit
 
 section noncomputable_defs

src/algebra/group_with_zero/basic.lean

@@ -790,9 +790,6 @@ by rw [inv_eq_iff_inv_eq, inv_zero, eq_comm]
 @[simp] lemma zero_eq_inv {a : G₀} : 0 = a⁻¹ ↔ 0 = a :=
 eq_comm.trans $ inv_eq_zero.trans eq_comm
 
-theorem divp_eq_div (a : G₀) (u : G₀ˣ) : a /ₚ u = a / u :=
-by simpa only [div_eq_mul_inv] using congr_arg ((*) a) u.coe_inv'
-
 @[simp] theorem divp_mk0 (a : G₀) {b : G₀} (hb : b ≠ 0) :
   a /ₚ units.mk0 b hb = a / b :=
 divp_eq_div _ _

src/algebra/hom/units.lean

@@ -6,9 +6,25 @@ Authors: Johan Commelin, Chris Hughes, Kevin Buzzard
 import algebra.hom.group
 
 /-!
-# Lift monoid homomorphisms to group homomorphisms of their units subgroups.
+# Monoid homomorphisms and units
+
+This file allows to lift monoid homomorphisms to group homomorphisms of their units subgroups. It
+also contains unrelated results about `units` that depend on `monoid_hom`.
+
+## Main declarations
+
+* `units.map`: Turn an homomorphism from `α` to `β` monoids into an homomorphism from `αˣ` to `βˣ`.
+* `monoid_hom.to_hom_units`: Turn an homomorphism from a group `α` to `β` into an homomorphism from
+  `α` to `βˣ`.
+
+## TODO
+
+The results that don't mention homomorphisms should be proved (earlier?) in a different file and be
+used to golf the basic `group` lemmas.
 -/
 
+open function
+
 universes u v w
 
 namespace units
@@ -57,6 +73,9 @@ variables [division_monoid α]
 @[simp, norm_cast, to_additive] lemma coe_zpow : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = u ^ n :=
 (units.coe_hom α).map_zpow
 
+lemma _root_.divp_eq_div (a : α) (u : αˣ) : a /ₚ u = a / u :=
+by rw [div_eq_mul_inv, divp, u.coe_inv]
+
 end division_monoid
 
 /-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then
@@ -103,31 +122,166 @@ def to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) : G →* Mˣ
 
 end monoid_hom
 
-section is_unit
-variables {M : Type*} {N : Type*}
+namespace is_unit
+variables {F α M N : Type*}
 
-@[to_additive] lemma is_unit.map {F : Type*} [monoid M] [monoid N] [monoid_hom_class F M N]
-  (f : F) {x : M} (h : is_unit x) : is_unit (f x) :=
+section monoid
+variables [monoid M] [monoid N]
+
+@[to_additive] lemma map [monoid_hom_class F M N] (f : F) {x : M} (h : is_unit x) : is_unit (f x) :=
 by rcases h with ⟨y, rfl⟩; exact (units.map (f : M →* N) y).is_unit
 
 /-- If a homomorphism `f : M →* N` sends each element to an `is_unit`, then it can be lifted
 to `f : M →* Nˣ`. See also `units.lift_right` for a computable version. -/
 @[to_additive "If a homomorphism `f : M →+ N` sends each element to an `is_add_unit`, then it can be
 lifted to `f : M →+ add_units N`. See also `add_units.lift_right` for a computable version."]
-noncomputable def is_unit.lift_right [monoid M] [monoid N] (f : M →* N)
-  (hf : ∀ x, is_unit (f x)) : M →* Nˣ :=
+noncomputable def lift_right (f : M →* N) (hf : ∀ x, is_unit (f x)) : M →* Nˣ :=
 units.lift_right f (λ x, (hf x).unit) $ λ x, rfl
 
-@[to_additive] lemma is_unit.coe_lift_right [monoid M] [monoid N] (f : M →* N)
-  (hf : ∀ x, is_unit (f x)) (x) :
+@[to_additive] lemma coe_lift_right (f : M →* N) (hf : ∀ x, is_unit (f x)) (x) :
   (is_unit.lift_right f hf x : N) = f x := rfl
 
-@[simp, to_additive] lemma is_unit.mul_lift_right_inv [monoid M] [monoid N] (f : M →* N)
-  (h : ∀ x, is_unit (f x)) (x) : f x * ↑(is_unit.lift_right f h x)⁻¹ = 1 :=
+@[simp, to_additive] lemma mul_lift_right_inv (f : M →* N) (h : ∀ x, is_unit (f x)) (x) :
+  f x * ↑(is_unit.lift_right f h x)⁻¹ = 1 :=
 units.mul_lift_right_inv (λ y, rfl) x
 
-@[simp, to_additive] lemma is_unit.lift_right_inv_mul [monoid M] [monoid N] (f : M →* N)
-  (h : ∀ x, is_unit (f x)) (x) : ↑(is_unit.lift_right f h x)⁻¹ * f x = 1 :=
+@[simp, to_additive] lemma lift_right_inv_mul (f : M →* N) (h : ∀ x, is_unit (f x)) (x) :
+  ↑(is_unit.lift_right f h x)⁻¹ * f x = 1 :=
 units.lift_right_inv_mul (λ y, rfl) x
 
+end monoid
+
+section division_monoid
+variables [division_monoid α] {a b c : α}
+
+@[simp, to_additive] protected lemma inv_mul_cancel : is_unit a → a⁻¹ * a = 1 :=
+by { rintro ⟨u, rfl⟩, rw [←units.coe_inv, units.inv_mul] }
+
+@[simp, to_additive] protected lemma mul_inv_cancel : is_unit a → a * a⁻¹ = 1 :=
+by { rintro ⟨u, rfl⟩, rw [←units.coe_inv, units.mul_inv] }
+
+/-- The element of the group of units, corresponding to an element of a monoid which is a unit. As
+opposed to `is_unit.unit`, the inverse is computable and comes from the inversion on `α`. This is
+useful to transfer properties of inversion in `units α` to `α`. See also `to_units`. -/
+@[to_additive "The element of the additive group of additive units, corresponding to an element of
+an additive monoid which is an additive unit. As opposed to `is_add_unit.add_unit`, the negation is
+computable and comes from the negation on `α`. This is useful to transfer properties of negation in
+`add_units α` to `α`. See also `to_add_units`.", simps]
+def unit' (h : is_unit a) : αˣ := ⟨a, a⁻¹, h.mul_inv_cancel, h.inv_mul_cancel⟩
+
+@[simp, to_additive] protected lemma mul_inv_cancel_left (h : is_unit a) : ∀ b, a * (a⁻¹ * b) = b :=
+h.unit'.mul_inv_cancel_left
+
+@[simp, to_additive] protected lemma inv_mul_cancel_left (h : is_unit a) : ∀ b, a⁻¹ * (a * b) = b :=
+h.unit'.inv_mul_cancel_left
+
+@[simp, to_additive] protected lemma mul_inv_cancel_right (h : is_unit b) (a : α) :
+  a * b * b⁻¹ = a :=
+h.unit'.mul_inv_cancel_right _
+
+@[simp, to_additive] protected lemma inv_mul_cancel_right (h : is_unit b) (a : α) :
+  a * b⁻¹ * b = a :=
+h.unit'.inv_mul_cancel_right _
+
+@[to_additive] protected lemma div_self (h : is_unit a) : a / a = 1 :=
+by rw [div_eq_mul_inv, h.mul_inv_cancel]
+
+@[to_additive] protected lemma eq_mul_inv_iff_mul_eq (h : is_unit c) : a = b * c⁻¹ ↔ a * c = b :=
+h.unit'.eq_mul_inv_iff_mul_eq
+
+@[to_additive] protected lemma eq_inv_mul_iff_mul_eq (h : is_unit b) : a = b⁻¹ * c ↔ b * a = c :=
+h.unit'.eq_inv_mul_iff_mul_eq
+
+@[to_additive] protected lemma inv_mul_eq_iff_eq_mul (h : is_unit a) : a⁻¹ * b = c ↔ b = a * c :=
+h.unit'.inv_mul_eq_iff_eq_mul
+
+@[to_additive] protected lemma mul_inv_eq_iff_eq_mul (h : is_unit b) : a * b⁻¹ = c ↔ a = c * b :=
+h.unit'.mul_inv_eq_iff_eq_mul
+
+@[to_additive] protected lemma mul_inv_eq_one (h : is_unit b) : a * b⁻¹ = 1 ↔ a = b :=
+@units.mul_inv_eq_one _ _ h.unit' _
+
+@[to_additive] protected lemma inv_mul_eq_one (h : is_unit a) : a⁻¹ * b = 1 ↔ a = b :=
+@units.inv_mul_eq_one _ _ h.unit' _
+
+@[to_additive] protected lemma mul_eq_one_iff_eq_inv (h : is_unit b) : a * b = 1 ↔ a = b⁻¹ :=
+@units.mul_eq_one_iff_eq_inv _ _ h.unit' _
+
+@[to_additive] protected lemma mul_eq_one_iff_inv_eq (h : is_unit a) : a * b = 1 ↔ a⁻¹ = b :=
+@units.mul_eq_one_iff_inv_eq _ _ h.unit' _
+
+@[simp, to_additive] protected lemma div_mul_cancel (h : is_unit b) (a : α) : a / b * b = a :=
+by rw [div_eq_mul_inv, h.inv_mul_cancel_right]
+
+@[simp, to_additive] protected lemma mul_div_cancel (h : is_unit b) (a : α) : a * b / b = a :=
+by rw [div_eq_mul_inv, h.mul_inv_cancel_right]
+
+@[to_additive] protected lemma mul_one_div_cancel (h : is_unit a) : a * (1 / a) = 1 := by simp [h]
+@[to_additive] protected lemma one_div_mul_cancel (h : is_unit a) : (1 / a) * a = 1 := by simp [h]
+
+@[to_additive] lemma inv : is_unit a → is_unit a⁻¹ :=
+by { rintro ⟨u, rfl⟩, rw ←units.coe_inv, exact units.is_unit _ }
+
+@[to_additive] lemma div (ha : is_unit a) (hb : is_unit b) : is_unit (a / b) :=
+by { rw div_eq_mul_inv, exact ha.mul hb.inv }
+
+@[to_additive] protected lemma div_left_inj (h : is_unit c) : a / c = b / c ↔ a = b :=
+by { simp_rw div_eq_mul_inv, exact units.mul_left_inj h.inv.unit' }
+
+@[to_additive] protected lemma div_eq_iff (h : is_unit b) : a / b = c ↔ a = c * b :=
+by rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]
+
+@[to_additive] protected lemma eq_div_iff (h : is_unit c) : a = b / c ↔ a * c = b :=
+by rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]
+
+@[to_additive] protected lemma div_eq_of_eq_mul (h : is_unit b) : a = c * b → a / b = c :=
+h.div_eq_iff.2
+
+@[to_additive] protected lemma eq_div_of_mul_eq (h : is_unit c) : a * c = b → a = b / c :=
+h.eq_div_iff.2
+
+@[to_additive] protected lemma div_eq_one_iff_eq (h : is_unit b) : a / b = 1 ↔ a = b :=
+⟨eq_of_div_eq_one, λ hab, hab.symm ▸ h.div_self⟩
+
+@[to_additive] protected lemma div_mul_left (h : is_unit b) : b / (a * b) = 1 / a :=
+by rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div]
+
+@[to_additive] protected lemma mul_div_mul_right (h : is_unit c) (a b : α) :
+  (a * c) / (b * c) = a / b :=
+by simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]
+
+@[to_additive] protected lemma mul_mul_div (a : α) (h : is_unit b) : a * b * (1 / b) = a :=
+by simp [h]
+
+end division_monoid
+
+section division_comm_monoid
+variables [division_comm_monoid α] {a b c d : α}
+
+@[to_additive] protected lemma div_mul_right (h : is_unit a) (b : α) : a / (a * b) = 1 / b :=
+by rw [mul_comm, h.div_mul_left]
+
+@[to_additive] protected lemma mul_div_cancel_left (h : is_unit a) (b : α) : a * b / a = b :=
+by rw [mul_comm, h.mul_div_cancel]
+
+@[to_additive] protected lemma mul_div_cancel' (h : is_unit a) (b : α) : a * (b / a) = b :=
+by rw [mul_comm, h.div_mul_cancel]
+
+@[to_additive] protected lemma mul_div_mul_left (h : is_unit c) (a b : α) :
+  (c * a) / (c * b) = a / b :=
+by rw [mul_comm c, mul_comm c, h.mul_div_mul_right]
+
+@[to_additive] protected lemma mul_eq_mul_of_div_eq_div (hb : is_unit b) (hd : is_unit d) (a c : α)
+  (h : a / b = c / d) : a * d = c * b :=
+by rw [←mul_one a, ←hb.div_self, ←mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]
+
+@[to_additive] protected lemma div_eq_div_iff (hb : is_unit b) (hd : is_unit d) :
+  a / b = c / d ↔ a * d = c * b :=
+by rw [←(hb.mul hd).mul_left_inj, ←mul_assoc, hb.div_mul_cancel, ←mul_assoc, mul_right_comm,
+  hd.div_mul_cancel]
+
+@[to_additive] protected lemma div_div_cancel (h : is_unit a) : a / (a / b) = b :=
+by rw [div_div_eq_mul_div, h.mul_div_cancel_left]
+
+end division_comm_monoid
 end is_unit

src/ring_theory/ideal/local_ring.lean

@@ -84,7 +84,7 @@ lemma is_unit_or_is_unit_of_is_unit_add {a b : R} (h : is_unit (a + b)) :
   is_unit a ∨ is_unit b :=
 begin
   rcases h with ⟨u, hu⟩,
-  rw [units.eq_iff_inv_mul, mul_add] at hu,
+  rw [←units.inv_mul_eq_one, mul_add] at hu,
   apply or.imp _ _ (is_unit_or_is_unit_of_add_one hu);
     exact is_unit_of_mul_is_unit_right,
 end