## Stream: maths

### Topic: Constructing an algebra equiv in term mode

#### Thomas Browning (Nov 07 2020 at 02:02):

Is there a term mode construction for this?

def equiv_of_eq (R S : Type*) [field R] [field S] [algebra R S]
(X Y : subalgebra R S) (h : X = Y) : X ≃ₐ[R] Y := by rw h


I've gotten the impression that definitions shouldn't be done in tactic mode.

#### Adam Topaz (Nov 07 2020 at 02:18):

If you really want:
You can always go all the way down the rabbit hole:

def equiv_of_eq (R S : Type*) [field R] [field S] [algebra R S]
(X Y : subalgebra R S) (h : X = Y) : X ≃ₐ[R] Y :=
{ to_fun := λ x,
{ val := x,
property := by {rw ←h, exact x.2} },
inv_fun := λ x,
{ val := x,
property := by {rw h, exact x.2} },
left_inv := by tidy,
right_inv := by tidy,
map_mul' := by tidy,
commutes' := by tidy }


#### Thomas Browning (Nov 07 2020 at 02:25):

True, although is this what rw is doing?

#### Adam Topaz (Nov 07 2020 at 02:26):

I don't think so.

#### Mario Carneiro (Nov 07 2020 at 02:26):

no, rw produces a term of the form eq.rec <equality proof> <subproof>

#### Adam Topaz (Nov 07 2020 at 02:28):

For example, this works:

def equiv_of_eq (R S : Type*) [field R] [field S] [algebra R S]
(X Y : subalgebra R S) (h : X = Y) : X ≃ₐ[R] Y :=
{ to_fun := λ x,
{ val := x,
property := by {rw ←h, exact x.2} },
inv_fun := λ x,
{ val := x,
property := by {rw h, exact x.2} },
left_inv := by tidy,
right_inv := by tidy,
map_mul' := by tidy,
commutes' := by tidy }

example (R S : Type*) [field R] [field S] [algebra R S] (X Y : subalgebra R S)
(h : X = Y) (x : X) : ((equiv_of_eq R S X Y h) x : S) = x := rfl


#### Mario Carneiro (Nov 07 2020 at 02:29):

we use definitions like equiv_of_eq so that the constructed object is definitionally of the form constructor <args> rather than eq.rec ..., so that you can reduce (equiv_of_eq X Y h).to_fun x = x := rfl, which doesn't work for eq.rec terms

#### Adam Topaz (Nov 07 2020 at 02:29):

I don't think the same example would work with the by rw h

#### Bryan Gin-ge Chen (Nov 07 2020 at 02:33):

This seems like something where automation could help, though I'm not sure how.

#### Mario Carneiro (Nov 07 2020 at 02:33):

here's the compressed version:

def equiv_of_eq (R S : Type*) [field R] [field S] [algebra R S]
(X Y : subalgebra R S) (h : X = Y) : X ≃ₐ[R] Y :=
by refine { to_fun := λ x, ⟨x, _⟩, inv_fun := λ x, ⟨x, _⟩, .. }; tidy


#### Adam Topaz (Nov 07 2020 at 02:34):

There was some discussion a while back about some version of tidy that can add simple data like \lam x, x. I guess something like that would work here

#### Adam Topaz (Nov 07 2020 at 02:36):

I think @Scott Morrison mentioned a follow your nose tactic?

#### Kevin Buzzard (Nov 07 2020 at 07:31):

@Thomas Browning you're right to be very wary of your initial definition using the rewrite. If you want to see the relative merits of your definition vs Adam/Mario's, try proving something like transitivity. Given X=Y and Y=Z try proving that the equiv you get between X and Z is equal to the composite of equivs from X to Y and Y to Z. With the tidy definition you should be able to reduce this to checking that the two maps are the same and it should be easy. With the rewrite definition you might find that the goal becomes completely intractible. I might be wrong but it might be worth spending five minutes trying.

#### Bhavik Mehta (Nov 07 2020 at 12:48):

I have seen tidy fill in some basic data sometimes, usually when the goal contains the data as well as a proposition about the data, where tidy splits, makes inconclusive progress on the data, but then uses solve by elim on the proposition, which fills in the metavariable for the data

Last updated: May 19 2021 at 02:10 UTC