refactor(algebra/associated): move is_unit def to algebra/group (#…

…2015)

* refactor(algebra/associated): move `is_unit` def to `algebra/group`

I think it makes sense to have it near `units`.

* Add a docstring to `units`, mention `is_unit` there.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/associated.lean

@@ -2,28 +2,18 @@
 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
+-/
+import algebra.group algebra.group.is_unit data.multiset
 
-Associated and irreducible elements.
+/-!
+# Associated, prime, and irreducible elements.
 -/
-import algebra.group data.multiset
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 open lattice
 
-/-- is unit -/
-def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u
-
-@[simp] lemma is_unit_unit [monoid α] (u : units α) : is_unit (u : α) := ⟨u, rfl⟩
-
 theorem is_unit.mk0 [division_ring α] (x : α) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
 
-lemma is_unit.map [monoid α] [monoid β] (f : α →* β) {x : α} (h : is_unit x) : is_unit (f x) :=
-by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
-
-lemma is_unit.map' [monoid α] [monoid β] (f : α → β) {x : α} (h : is_unit x) [is_monoid_hom f] :
-  is_unit (f x) :=
-h.map (monoid_hom.of f)
-
 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
  λ h, begin
@@ -34,38 +24,9 @@ h.map (monoid_hom.of f)
 @[simp] theorem not_is_unit_zero [nonzero_comm_ring α] : ¬ is_unit (0 : α) :=
 mt is_unit_zero_iff.1 zero_ne_one
 
-@[simp] theorem is_unit_one [monoid α] : is_unit (1:α) := ⟨1, rfl⟩
-
-theorem is_unit_of_mul_one [comm_monoid α] (a b : α) (h : a * b = 1) : is_unit a :=
-⟨units.mk_of_mul_eq_one a b h, rfl⟩
-
-theorem is_unit_iff_exists_inv [comm_monoid α] {a : α} : is_unit a ↔ ∃ b, a * b = 1 :=
-⟨by rintro ⟨⟨a, b, hab, _⟩, rfl⟩; exact ⟨b, hab⟩,
- λ ⟨b, hab⟩, is_unit_of_mul_one _ b hab⟩
-
-theorem is_unit_iff_exists_inv' [comm_monoid α] {a : α} : is_unit a ↔ ∃ b, b * a = 1 :=
-by simp [is_unit_iff_exists_inv, mul_comm]
-
 lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
 
-@[simp] theorem units.is_unit_mul_units [monoid α] (a : α) (u : units α) :
-  is_unit (a * u) ↔ is_unit a :=
-iff.intro
-  (assume ⟨v, hv⟩,
-    have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [hv, units.coe_mul],
-    by rwa [mul_assoc, units.mul_inv, mul_one] at this)
-  (assume ⟨v, hv⟩, hv.symm ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
-
-theorem is_unit_of_mul_is_unit_left {α} [comm_monoid α] {x y : α}
-  (hu : is_unit (x * y)) : is_unit x :=
-let ⟨z, hz⟩ := is_unit_iff_exists_inv.1 hu in
-is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
-
-theorem is_unit_of_mul_is_unit_right {α} [comm_monoid α] {x y : α}
-  (hu : is_unit (x * y)) : is_unit y :=
-@is_unit_of_mul_is_unit_left _ _ y x $ by rwa mul_comm
-
 theorem is_unit_iff_dvd_one [comm_semiring α] {x : α} : is_unit x ↔ x ∣ 1 :=
 ⟨by rintro ⟨u, rfl⟩; exact ⟨_, u.mul_inv.symm⟩,
  λ ⟨y, h⟩, ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩
@@ -91,11 +52,6 @@ theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
 
-@[simp] theorem is_unit_nat {n : ℕ} : is_unit n ↔ n = 1 :=
-iff.intro
-  (assume ⟨u, hu⟩, match n, u, hu, nat.units_eq_one u with _, _, rfl, rfl := rfl end)
-  (assume h, h.symm ▸ ⟨1, rfl⟩)
-
 theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
 ⟨λ ⟨u, hu⟩, (int.units_eq_one_or u).elim (by simp *) (by simp *),
   λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
@@ -221,6 +177,8 @@ have hpd : p ∣ x * y, from ⟨z, by rwa [domain.mul_left_inj hp0] at h⟩,
   (λ ⟨d, hd⟩, or.inl ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
   (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
 
+/-- Two elements of a `monoid` are `associated` if one of them is another one
+multiplied by a unit on the right. -/
 def associated [monoid α] (x y : α) : Prop := ∃u:units α, x * u = y
 
 local infix ` ~ᵤ ` : 50 := associated

src/algebra/group/default.lean

@@ -16,3 +16,4 @@ import algebra.group.conj
 import algebra.group.with_one
 import algebra.group.anti_hom
 import algebra.group.units_hom
+import algebra.group.is_unit

src/algebra/group/is_unit.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Jens Wagemaker
+
+Contents of this file was cherry-picked from `algebra/associated` by Yury Kudryashov.
+I copied the original copyright header from there.
+-/
+import algebra.group.units_hom
+
+/-!
+# `is_unit` predicate
+
+In this file we define the `is_unit` predicate on a `monoid`, and
+prove a few basic properties. For the bundled version see `units`. See
+also `prime`, `associated`, and `irreducible` in `algebra/associated`.
+
+-/
+
+variables {M : Type*} {N : Type*}
+
+/-- An element `a : M` of a monoid is a unit if it has a two-sided inverse.
+The actual definition says that `a` is equal to some `u : units M`, where
+`units M` is a bundled version of `is_unit`. -/
+def is_unit [monoid M] (a : M) : Prop := ∃ u : units M, a = u
+
+@[simp] lemma is_unit_unit [monoid M] (u : units M) : is_unit (u : M) := ⟨u, rfl⟩
+
+lemma is_unit.map [monoid M] [monoid N] (f : M →* N) {x : M} (h : is_unit x) : is_unit (f x) :=
+by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
+
+lemma is_unit.map' [monoid M] [monoid N] (f : M → N) {x : M} (h : is_unit x) [is_monoid_hom f] :
+  is_unit (f x) :=
+h.map (monoid_hom.of f)
+
+@[simp] theorem is_unit_one [monoid M] : is_unit (1:M) := ⟨1, rfl⟩
+
+theorem is_unit_of_mul_one [comm_monoid M] (a b : M) (h : a * b = 1) : is_unit a :=
+⟨units.mk_of_mul_eq_one a b h, rfl⟩
+
+theorem is_unit_iff_exists_inv [comm_monoid M] {a : M} : is_unit a ↔ ∃ b, a * b = 1 :=
+⟨by rintro ⟨⟨a, b, hab, _⟩, rfl⟩; exact ⟨b, hab⟩,
+ λ ⟨b, hab⟩, is_unit_of_mul_one _ b hab⟩
+
+theorem is_unit_iff_exists_inv' [comm_monoid M] {a : M} : is_unit a ↔ ∃ b, b * a = 1 :=
+by simp [is_unit_iff_exists_inv, mul_comm]
+
+/-- Multiplication by a `u : units M` doesn't affect `is_unit`. -/
+@[simp] theorem units.is_unit_mul_units [monoid M] (a : M) (u : units M) :
+  is_unit (a * u) ↔ is_unit a :=
+iff.intro
+  (assume ⟨v, hv⟩,
+    have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [hv, units.coe_mul],
+    by rwa [mul_assoc, units.mul_inv, mul_one] at this)
+  (assume ⟨v, hv⟩, hv.symm ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
+
+theorem is_unit_of_mul_is_unit_left [comm_monoid M] {x y : M}
+  (hu : is_unit (x * y)) : is_unit x :=
+let ⟨z, hz⟩ := is_unit_iff_exists_inv.1 hu in
+is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
+
+theorem is_unit_of_mul_is_unit_right [comm_monoid M] {x y : M}
+  (hu : is_unit (x * y)) : is_unit y :=
+@is_unit_of_mul_is_unit_left _ _ y x $ by rwa mul_comm
+
+@[simp] theorem is_unit_nat {n : ℕ} : is_unit n ↔ n = 1 :=
+iff.intro
+  (assume ⟨u, hu⟩, match n, u, hu, nat.units_eq_one u with _, _, rfl, rfl := rfl end)
+  (assume h, h.symm ▸ ⟨1, rfl⟩)

src/algebra/group/units.lean

@@ -2,15 +2,19 @@
 Copyright (c) 2017 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johannes, Hölzl, Chris Hughes
-
-Units (i.e., invertible elements) of a multiplicative monoid.
 -/
-
 import tactic.basic logic.function
 
+/-!
+# Units (i.e., invertible elements) of a multiplicative monoid
+-/
+
 universe u
 variable {α : Type u}
 
+/-- Units of a monoid, bundled version. An element of a `monoid` is a unit if it has a two-sided
+inverse. This version bundles the inverse element so that it can be computed. For a predicate
+see `is_unit`. -/
 structure units (α : Type u) [monoid α] :=
 (val : α)
 (inv : α)