chore(algebra/group/type_tags): add additive.to_mul etc (#2363)

Don't make `additive` and `multiplicative` irreducible (yet?) because
it breaks compilation here and there.

Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative`
versions are defined by the image of `1`.



Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Author: urkud

src/algebra/group/type_tags.lean

@@ -27,14 +27,54 @@ def additive (α : Type*) := α
 multiplicative structure. -/
 def multiplicative (α : Type*) := α
 
-instance [inhabited α] : inhabited (additive α) := ⟨(default _ : α)⟩
-instance [inhabited α] : inhabited (multiplicative α) := ⟨(default _ : α)⟩
+/-- Reinterpret `x : α` as an element of `additive α`. -/
+def additive.of_mul (x : α) : additive α := x
+
+/-- Reinterpret `x : additive α` as an element of `α`. -/
+def additive.to_mul (x : additive α) : α := x
+
+lemma of_mul_inj : function.injective (@additive.of_mul α) := λ _ _, id
+lemma to_mul_inj : function.injective (@additive.to_mul α) := λ _ _, id
+
+/-- Reinterpret `x : α` as an element of `multiplicative α`. -/
+def multiplicative.of_add (x : α) : multiplicative α := x
+
+/-- Reinterpret `x : multiplicative α` as an element of `α`. -/
+def multiplicative.to_add (x : multiplicative α) : α := x
+
+lemma of_add_inj : function.injective (@multiplicative.of_add α) := λ _ _, id
+lemma to_add_inj : function.injective (@multiplicative.to_add α) := λ _ _, id
+
+@[simp] lemma to_add_of_add (x : α) : (multiplicative.of_add x).to_add = x := rfl
+@[simp] lemma of_add_to_add (x : multiplicative α) : multiplicative.of_add x.to_add = x := rfl
+
+@[simp] lemma to_mul_of_mul (x : α) : (additive.of_mul x).to_mul = x := rfl
+@[simp] lemma of_mul_to_mul (x : additive α) : additive.of_mul x.to_mul = x := rfl
+
+instance [inhabited α] : inhabited (additive α) := ⟨additive.of_mul (default α)⟩
+instance [inhabited α] : inhabited (multiplicative α) := ⟨multiplicative.of_add (default α)⟩
 
 instance additive.has_add [has_mul α] : has_add (additive α) :=
-{ add := ((*) : α → α → α) }
+{ add := λ x y, additive.of_mul (x.to_mul * y.to_mul) }
 
 instance [has_add α] : has_mul (multiplicative α) :=
-{ mul := ((+) : α → α → α) }
+{ mul := λ x y, multiplicative.of_add (x.to_add + y.to_add) }
+
+@[simp] lemma of_add_add [has_add α] (x y : α) :
+  multiplicative.of_add (x + y) = multiplicative.of_add x * multiplicative.of_add y :=
+rfl
+
+@[simp] lemma to_add_mul [has_add α] (x y : multiplicative α) :
+  (x * y).to_add = x.to_add + y.to_add :=
+rfl
+
+@[simp] lemma of_mul_mul [has_mul α] (x y : α) :
+  additive.of_mul (x * y) = additive.of_mul x + additive.of_mul y :=
+rfl
+
+@[simp] lemma to_mul_add [has_mul α] (x y : additive α) :
+  (x + y).to_mul = x.to_mul * y.to_mul :=
+rfl
 
 instance [semigroup α] : add_semigroup (additive α) :=
 { add_assoc := @mul_assoc α _,
@@ -68,43 +108,63 @@ instance [add_right_cancel_semigroup α] : right_cancel_semigroup (multiplicativ
 { mul_right_cancel := @add_right_cancel _ _,
   ..multiplicative.semigroup }
 
+instance [has_one α] : has_zero (additive α) := ⟨additive.of_mul 1⟩
+
+@[simp] lemma of_mul_one [has_one α] : @additive.of_mul α 1 = 0 := rfl
+
+@[simp] lemma to_mul_zero [has_one α] : (0 : additive α).to_mul = 1 := rfl
+
+instance [has_zero α] : has_one (multiplicative α) := ⟨multiplicative.of_add 0⟩
+
+@[simp] lemma of_add_zero [has_zero α] : @multiplicative.of_add α 0 = 1 := rfl
+
+@[simp] lemma to_add_one [has_zero α] : (1 : multiplicative α).to_add = 0 := rfl
+
 instance [monoid α] : add_monoid (additive α) :=
-{ zero     := (1 : α),
+{ zero     := 0,
   zero_add := @one_mul _ _,
   add_zero := @mul_one _ _,
   ..additive.add_semigroup }
 
 instance [add_monoid α] : monoid (multiplicative α) :=
-{ one     := (0 : α),
+{ one     := 1,
   one_mul := @zero_add _ _,
   mul_one := @add_zero _ _,
   ..multiplicative.semigroup }
 
 instance [comm_monoid α] : add_comm_monoid (additive α) :=
-{ add_comm := @mul_comm α _,
-  ..additive.add_monoid }
+{ .. additive.add_monoid, .. additive.add_comm_semigroup }
 
 instance [add_comm_monoid α] : comm_monoid (multiplicative α) :=
-{ mul_comm := @add_comm α _,
-  ..multiplicative.monoid }
+{ ..multiplicative.monoid, .. multiplicative.comm_semigroup }
+
+instance [has_inv α] : has_neg (additive α) := ⟨λ x, multiplicative.of_add x.to_mul⁻¹⟩
+
+@[simp] lemma of_mul_inv [has_inv α] (x : α) : additive.of_mul x⁻¹ = -(additive.of_mul x) := rfl
+
+@[simp] lemma to_mul_neg [has_inv α] (x : additive α) : (-x).to_mul = x.to_mul⁻¹ := rfl
+
+instance [has_neg α] : has_inv (multiplicative α) := ⟨λ x, additive.of_mul (-x.to_add)⟩
+
+@[simp] lemma of_add_neg [has_neg α] (x : α) :
+  multiplicative.of_add (-x) = (multiplicative.of_add x)⁻¹ := rfl
+
+@[simp] lemma to_add_inv [has_neg α] (x : multiplicative α) :
+  (x⁻¹).to_add = -x.to_add := rfl
 
 instance [group α] : add_group (additive α) :=
-{ neg := @has_inv.inv α _,
-  add_left_neg := @mul_left_inv _ _,
-  ..additive.add_monoid }
+{ add_left_neg := @mul_left_inv α _,
+  .. additive.has_neg, .. additive.add_monoid }
 
 instance [add_group α] : group (multiplicative α) :=
-{ inv := @has_neg.neg α _,
-  mul_left_inv := @add_left_neg _ _,
-  ..multiplicative.monoid }
+{ mul_left_inv := @add_left_neg α _,
+  .. multiplicative.has_inv, ..multiplicative.monoid }
 
 instance [comm_group α] : add_comm_group (additive α) :=
-{ add_comm := @mul_comm α _,
-  ..additive.add_group }
+{ .. additive.add_group, .. additive.add_comm_monoid }
 
 instance [add_comm_group α] : comm_group (multiplicative α) :=
-{ mul_comm := @add_comm α _,
-  ..multiplicative.group }
+{ .. multiplicative.group, .. multiplicative.comm_monoid }
 
 /-- Reinterpret `f : α →+ β` as `multiplicative α →* multiplicative β`. -/
 def add_monoid_hom.to_multiplicative [add_monoid α] [add_monoid β] (f : α →+ β) :

src/algebra/group_power.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 
-import data.int.basic
+import data.int.basic data.equiv.basic
 
 /-!
 # Power operations on monoids and groups
@@ -23,8 +23,10 @@ We define instances of `has_pow M ℕ`, for monoids `M`, and `has_pow G ℤ` for
 We adopt the convention that `0^0 = 1`.
 -/
 
-variables {M : Type*} {N : Type*} {G : Type*} {H : Type*} {A : Type*} {B : Type*}
-  {R : Type*} {S : Type*}
+universes u v w x y z u₁ u₂
+
+variables {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
+  {R : Type u₁} {S : Type u₂}
 
 /-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
 def monoid.pow [has_mul M] [has_one M] (a : M) : ℕ → M
@@ -668,3 +670,41 @@ end int
 
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
+
+@[simp] lemma pow_of_add [add_monoid A] (x : A) (n : ℕ) :
+  multiplicative.of_add (n • x) = (multiplicative.of_add x)^n := rfl
+
+@[simp] lemma gpow_of_add [add_group A] (x : A) (n : ℤ) :
+  multiplicative.of_add (n •ℤ x) = (multiplicative.of_add x)^n := rfl
+
+variables (M G A)
+
+/-- Monoid homomorphisms from `multiplicative ℕ` are defined by the image
+of `multiplicative.of_add 1`. -/
+def powers_hom [monoid M] : M ≃ (multiplicative ℕ →* M) :=
+{ to_fun := λ x, ⟨λ n, x ^ n.to_add, pow_zero x, λ m n, pow_add x m n⟩,
+  inv_fun := λ f, f (multiplicative.of_add 1),
+  left_inv := pow_one,
+  right_inv := λ f, monoid_hom.ext $ λ n, by { simp [← f.map_pow, ← pow_of_add] } }
+
+/-- Monoid homomorphisms from `multiplicative ℤ` are defined by the image
+of `multiplicative.of_add 1`. -/
+def gpowers_hom [group G] : G ≃ (multiplicative ℤ →* G) :=
+{ to_fun := λ x, ⟨λ n, x ^ n.to_add, gpow_zero x, λ m n, gpow_add x m n⟩,
+  inv_fun := λ f, f (multiplicative.of_add 1),
+  left_inv := gpow_one,
+  right_inv := λ f, monoid_hom.ext $ λ n, by { simp [← f.map_gpow, ← gpow_of_add] } }
+
+/-- Additive homomorphisms from `ℕ` are defined by the image of `1`. -/
+def multiples_hom [add_monoid A] : A ≃ (ℕ →+ A) :=
+{ to_fun := λ x, ⟨λ n, n • x, add_monoid.zero_smul x, λ m n, add_monoid.add_smul _ _ _⟩,
+  inv_fun := λ f, f 1,
+  left_inv := add_monoid.one_smul,
+  right_inv := λ f, add_monoid_hom.ext $ λ n, by simp [← f.map_smul] }
+
+/-- Additive homomorphisms from `ℤ` are defined by the image of `1`. -/
+def gmultiples_hom [add_group A] : A ≃ (ℤ →+ A) :=
+{ to_fun := λ x, ⟨λ n, n •ℤ x, zero_gsmul x, λ m n, add_gsmul _ _ _⟩,
+  inv_fun := λ f, f 1,
+  left_inv := one_gsmul,
+  right_inv := λ f, add_monoid_hom.ext $ λ n, by simp [← f.map_gsmul] }

src/group_theory/submonoid.lean

@@ -729,20 +729,6 @@ lemma closure_union (s t : set M) : closure (s ∪ t) = closure s ⊔ closure t
 lemma closure_Union {ι} (s : ι → set M) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
 (submonoid.gi M).gc.l_supr
 
-/-- The submonoid generated by an element of a monoid equals the set of natural number powers of
-    the element. -/
-lemma mem_closure_singleton {x y : M} : y ∈ closure ({x} : set M) ↔ ∃ n:ℕ, x^n=y :=
-begin
-  refine ⟨λ hy, closure_induction hy _ _ _,
-    λ ⟨n, hn⟩, hn ▸ pow_mem _ (subset_closure $ mem_singleton x) n⟩,
-  { intros y hy,
-    rw [eq_of_mem_singleton hy],
-    exact ⟨1, pow_one x⟩ },
-  { exact ⟨0, rfl⟩ },
-  { rintros _ _ ⟨n, rfl⟩ ⟨m, rfl⟩,
-    exact ⟨n + m, pow_add x n m⟩ }
-end
-
 @[to_additive]
 lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → submonoid M} (hS : directed (≤) S)
   {x : M} :
@@ -896,32 +882,6 @@ def prod_equiv (s : submonoid M) (t : submonoid N) : s.prod t ≃* s × t :=
 
 end submonoid
 
-namespace add_submonoid
-
-open set
-
-lemma smul_mem (S : add_submonoid A) {x : A} (hx : x ∈ S) :
-  ∀ n : ℕ, add_monoid.smul n x ∈ S
-| 0     := S.zero_mem
-| (n+1) := S.add_mem hx (smul_mem n)
-
-/-- The `add_submonoid` generated by an element of an `add_monoid` equals the set of
-natural number multiples of the element. -/
-lemma mem_closure_singleton {x y : A} :
-  y ∈ closure ({x} : set A) ↔ ∃ n:ℕ, add_monoid.smul n x = y :=
-begin
-  refine ⟨λ hy, closure_induction hy _ _ _,
-    λ ⟨n, hn⟩, hn ▸ smul_mem _ (subset_closure $ mem_singleton x) n⟩,
-  { intros y hy,
-    rw [eq_of_mem_singleton hy],
-    exact ⟨1, add_monoid.one_smul x⟩ },
-  { exact ⟨0, rfl⟩ },
-  { rintros _ _ ⟨n, rfl⟩ ⟨m, rfl⟩,
-    exact ⟨n + m, add_monoid.add_smul x n m⟩ }
-end
-
-end add_submonoid
-
 namespace monoid_hom
 
 variables {N : Type*} {P : Type*} [monoid N] [monoid P] (S : submonoid M)
@@ -1056,6 +1016,15 @@ S.subtype.cod_restrict _ (λ x, h x.2)
 lemma range_subtype (s : submonoid M) : s.subtype.mrange = s :=
 ext' $ (coe_mrange _).trans $ set.range_coe_subtype s
 
+lemma closure_singleton_eq (x : M) : closure ({x} : set M) = (powers_hom M x).mrange :=
+closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, trivial, pow_one x⟩) $
+  λ x ⟨n, _, hn⟩, hn ▸ pow_mem _ (subset_closure $ set.mem_singleton _) _
+
+/-- The submonoid generated by an element of a monoid equals the set of natural number powers of
+    the element. -/
+lemma mem_closure_singleton {x y : M} : y ∈ closure ({x} : set M) ↔ ∃ n:ℕ, x^n=y :=
+by rw [closure_singleton_eq, mem_mrange]; refl
+
 @[to_additive]
 lemma closure_eq_mrange (s : set M) : closure s = (free_monoid.lift s M coe).mrange :=
 by rw [mrange, ← free_monoid.closure_range_of, map_mclosure,
@@ -1133,6 +1102,27 @@ by simp only [sup_eq_range, mem_mrange, coprod_apply, prod.exists, submonoid.exi
 
 end submonoid
 
+namespace add_submonoid
+
+open set
+
+lemma smul_mem (S : add_submonoid A) {x : A} (hx : x ∈ S) :
+  ∀ n : ℕ, add_monoid.smul n x ∈ S
+| 0     := S.zero_mem
+| (n+1) := S.add_mem hx (smul_mem n)
+
+lemma closure_singleton_eq (x : A) : closure ({x} : set A) = (multiples_hom A x).mrange :=
+closure_eq_of_le (set.singleton_subset_iff.2 ⟨1, trivial, add_monoid.one_smul x⟩) $
+  λ x ⟨n, _, hn⟩, hn ▸ smul_mem _ (subset_closure $ set.mem_singleton _) _
+
+/-- The `add_submonoid` generated by an element of an `add_monoid` equals the set of
+natural number multiples of the element. -/
+lemma mem_closure_singleton {x y : A} : y ∈ closure ({x} : set A) ↔ ∃ n:ℕ, add_monoid.smul n x = y :=
+by rw [closure_singleton_eq, add_monoid_hom.mem_mrange]; refl
+
+end add_submonoid
+
+
 namespace mul_equiv
 
 variables {S T : submonoid M}