## Stream: general

### Topic: Creating iso from equiv

#### Yaël Dillies (Feb 24 2022 at 21:55):

/-- Build an isomorphism in the category Group from a mul_equiv between groups. -/
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 (Feb 24 2022 at 21:55):

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 (Feb 24 2022 at 21:55):

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 (Feb 24 2022 at 21:56):

cc the usual suspect, @Scott Morrison

#### Reid Barton (Feb 24 2022 at 22:00):

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 (Feb 24 2022 at 22:00):

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

#### Yaël Dillies (Feb 24 2022 at 22:00):

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

#### Scott Morrison (Feb 24 2022 at 22:01):

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 (Feb 24 2022 at 22:02):

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

#### Yaël Dillies (Feb 24 2022 at 22:05):

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 (Feb 24 2022 at 22:05):

It's really benign.

#### Reid Barton (Feb 24 2022 at 22:16):

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

#### Yaël Dillies (Feb 24 2022 at 22:20):

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 (Feb 24 2022 at 23:05):

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

#### Yaël Dillies (Mar 02 2022 at 17:03):

#12407

Last updated: Aug 03 2023 at 10:10 UTC