From 1db0052eb3c03e283f990ab62df4006a9114125f Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Thu, 23 Dec 2021 22:35:56 +0000 Subject: [PATCH] feat(group_theory/submonoid/membership): upgrade definition of pow from a set morphism to a monoid morphism (#10898) This comes at no extra cost. All the prerequisite definitions and lemmas were already in mathlib. --- src/group_theory/submonoid/membership.lean | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index b58f4197bdd0e..8ac01014d7eb2 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -220,7 +220,8 @@ lemma powers_subset {n : M} {P : submonoid M} (h : n ∈ P) : powers n ≤ P := λ x hx, match x, hx with _, ⟨i, rfl⟩ := P.pow_mem h i end /-- Exponentiation map from natural numbers to powers. -/ -def pow (n : M) (m : ℕ) : powers n := ⟨n ^ m, m, rfl⟩ +@[simps] def pow (n : M) (m : ℕ) : powers n := +(powers_hom M n).mrange_restrict (multiplicative.of_add m) /-- Logarithms from powers to natural numbers. -/ def log [decidable_eq M] {n : M} (p : powers n) : ℕ := @@ -237,8 +238,19 @@ theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m : log (pow n m) = m := pow_right_injective_iff_pow_injective.mp h $ pow_log_eq_self _ +/-- The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers +when it is injective. The inverse is given by the logarithms. -/ +@[simps] +def pow_log_equiv [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m)) : + multiplicative ℕ ≃* powers n := +{ to_fun := λ m, pow n m.to_add, + inv_fun := λ m, multiplicative.of_add (log m), + left_inv := log_pow_eq_self h, + right_inv := pow_log_eq_self, + map_mul' := λ _ _, by { simp only [pow, map_mul, of_add_add, to_add_mul] } } + theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.nat_abs) (m : ℕ) : log (pow x m) = m := -log_pow_eq_self (int.pow_right_injective h) _ +(pow_log_equiv (int.pow_right_injective h)).symm_apply_apply _ @[simp] lemma map_powers {N : Type*} [monoid N] (f : M →* N) (m : M) : (powers m).map f = powers (f m) :=