## Stream: general

### Topic: definition of is_mul_hom

#### Kevin Buzzard (Mar 17 2019 at 15:05):

import data.equiv.basic algebra.group

def is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop :=
-- Should this be {x y} or (x y) or ⦃x y⦄?
∀ {x y}, f (x * y) = f x * f y

structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β :=
(hom : is_mul_hom to_fun)

infix  ≃* :50 := mul_equiv

variables {α : Type*} {β : Type*} [monoid α] [monoid β]

namespace mul_equiv

@[symm] def symm (h : α ≃* β) : β ≃* α :=
{ hom := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
rw h.hom, unfold equiv.symm, rw [h.right_inv, h.right_inv, h.right_inv], end
..h.to_equiv.symm}

lemma one (h : equiv α β) (hom : ∀ x y, h (x * y) = h x * h y) :
h 1 = 1 :=
by rw [←mul_one (h 1), ←h.apply_symm_apply 1, ←hom]; simp

instance is_monoid_hom (h : α ≃* β) : is_monoid_hom h.to_equiv := {
map_one := mul_equiv.one h.to_equiv h.hom,
map_mul := h.hom }

open units

def map_equiv (h : α ≃* β) : units α ≃* units β :=
{ to_fun := map h.to_equiv,
inv_fun := map h.symm.to_equiv,
left_inv := λ u, ext $h.left_inv u, right_inv := λ u, ext$ h.right_inv u,
--  hom := λ a b, units.ext $h.hom} -- fails -- hom := λ a b, units.ext$ by exact h.hom} -- fails

#### Kevin Buzzard (Mar 17 2019 at 17:08):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/bounds/near/147878878 is the reason why I don't just PR this modification of monotone. I already observed that some stuff in mathlib only needed has_le but Mario seemed to think it was better to have it defined on preorders. I remember being surprised at the time.

#### Kevin Buzzard (Mar 17 2019 at 17:14):

In your def is_mul_hom I don't see any reason to have implicit x and y. Make them explicit and your problem in map_equiv will disappear (using hom := λ a b, units.ext \$ h.hom _ _)

Mario wrote monotone and he used {{ }}. Note that is_mul_hom is "forall x y, P = Q" whereas monotone is "forall {{x y}}, P -> Q". Does the implication make a difference?

it does

#### Mario Carneiro (Mar 17 2019 at 17:25):

you could use {{ }} for is_mul_hom but it wouldn't make a difference

#### Kevin Buzzard (Mar 17 2019 at 17:42):

Ok, PR updated, although I don't really understand what's going on.

#### Kevin Buzzard (Mar 17 2019 at 18:07):

https://github.com/leanprover-community/mathlib/blob/e8bdc7fc14c6d56d4040892d16929f310e9d03d5/src/algebra/group.lean#L597

Mathlib currently has implicits for map_mul there. If I change them then algebra.big_operators breaks . Is it worth changing?

Last updated: Aug 03 2023 at 10:10 UTC