Creating iso from equiv

Stream: general

[Yaël Dillies]

Compare docs#mul_equiv.to_Group_iso and docs#Preorder.iso.mk:

/-- Build an isomorphism in the category `Group` from a `mul_equiv` between `group`s. -/
def mul_equiv.to_Group_iso {X Y : Type*} [group X] [group Y] (e : X ≃* Y) : Group.of X ≅ Group.of Y :=
{ hom := e.to_monoid_hom,
  inv := e.symm.to_monoid_hom }

/-- Constructs an equivalence between preorders from an order isomorphism between them. -/
def Preorder.iso.mk {X Y : Preorder} (e : X ≃o Y) : X ≅ Y :=
{ hom := e,
  inv := e.symm,
  hom_inv_id' := by { ext, exact e.symm_apply_apply x },
  inv_hom_id' := by { ext, exact e.apply_symm_apply x } }

[Yaël Dillies]

The first bundles X and Y as Groups on the fly while the second takes X Y : Preorder directly. The destruction-construction happening in the first case is making me eat my hat because it breaks defeq:

import algebra.category.Group.basic

example (X : Group) : Group.of ↥X = X := rfl -- fails
example (X : Group) : Group.of ↥X = X := by { cases X, refl } --works

[Yaël Dillies]

Is there any reason why it is so? Does anyone mind if I change mul_equiv.to_Group_iso to take X Y : Group directly?

[Yaël Dillies]

cc the usual suspect, @Scott Morrison

[Reid Barton]

Yes, I agree X Y : Group is the right way to set up the first one. (As a bonus, it's shorter too!)

[Scott Morrison]

I can't recall immediately anything that this change would break.

[Yaël Dillies]

From trying it out quickly now, it breaks more uses of Group.of downstream, whose fix is the same.

[Scott Morrison]

I suspect this was just because in the "early days", there was less of an audience for API in terms of Group, because no one was actually using it, and so I may have written it this way just to have the argument all live in the "classical"/"unbundled" world.

[Reid Barton]

Hmm, I'm a little surprised that change would break anything--can you give an example?

[Yaël Dillies]

If e : X ≃* Y, then e.to_Group_iso doesn't work. You need (e : ↥(Group.of X) ≃* ↥(Group.of Y)).to_Group_iso or something.

[Yaël Dillies]

It's really benign.

[Reid Barton]

Most of the time inference should be outside-in, so this won't be a problem

[Yaël Dillies]

It just breaks dot notation in my case due to order of elaboration. But the alternative is undefeqness pain, so I'll take it :smile:

[Eric Wieser]

Just to be clear, it works fine with non-dot notation?

[Yaël Dillies]

#12407