definition of is_mul_hom

Stream: general

[Kevin Buzzard]

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]

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]

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]

I think you should PR a modification of monotone which assumes only has_le

[Patrick Massot]

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]

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]

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]

it does

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?