# Zulip Chat Archive

## 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 hom := λ a b, units.ext $ by have X := h.hom; exact X} -- works end mul_equiv

In the perfectoid project we have a bunch of groups, rings, linearly ordered commutative monoids etc which are canonically isomorphic, so I've been trying to extend `equiv`

to more general situations (see #789). Why am I having trouble with the last line here?

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

Could it be the case that the `hom`

field in the structure might need different brackets to the def? I should get this right now because I want to build a bunch of equivs on top of this.

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

import order.basic #check @monotone -- monotone : Π {α : Type u_1} {β : Type u_2} [_inst_1 : preorder α] [_inst_2 : preorder β], -- (α → β) → Prop #print monotone -- ∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b

In #789 Chris encouraged me to define `mul_equiv`

for two types with `has_mul`

as a bijection which preserved `*`

. I want `le_equiv`

and I was going to use `monotone`

but this needs a preorder, rather than just a `has_le`

.

What is the best idea here? Can I weaken the definition of `monotone`

to only demand `has_le`

? Should I not define `le_equiv`

and instead stick to `preorder_equiv`

?

#### Patrick Massot (Mar 17 2019 at 16:26):

I think you should PR a modification of `monotone`

which assumes only `has_le`

#### Patrick Massot (Mar 17 2019 at 16:28):

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 _ _`

)

#### 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?

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

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):

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