Zulip Chat Archive

Stream: maths

Topic: Constructing an algebra equiv in term mode


view this post on Zulip 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.

view this post on Zulip 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,
  map_add' := by tidy,
  commutes' := by tidy }

view this post on Zulip Thomas Browning (Nov 07 2020 at 02:25):

True, although is this what rw is doing?

view this post on Zulip Adam Topaz (Nov 07 2020 at 02:26):

I don't think so.

view this post on Zulip Mario Carneiro (Nov 07 2020 at 02:26):

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

view this post on Zulip 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,
  map_add' := 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 07 2020 at 02:29):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2020 at 02:33):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 07 2020 at 02:36):

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

view this post on Zulip 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.

view this post on Zulip 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