Constructing an algebra equiv in term mode

Stream: maths

[Thomas Browning]

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]

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 }

[Thomas Browning]

True, although is this what rw is doing?

[Adam Topaz]

I don't think so.

[Mario Carneiro]

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

[Adam Topaz]

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

[Mario Carneiro]

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]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

@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]

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