equiv.cast that preserves structure

Stream: Is there code for X?

[Pierre-Alexandre Bazin]

example {ι : Type*} {β : ι → Type*} [Π i, add_monoid (β i)] {i j : ι} (h : i = j) : β i ≃+ β j := sorry do we have anything like that (and similar for other structures) ? I see equiv.cast but it doesn't preserve structure

[Kevin Buzzard]

example {ι : Type*} {β : ι → Type*} [Π i, add_monoid (β i)] {i j : ι} (h : i = j) : β i ≃+ β j :=
eq.rec (add_equiv.refl (β i)) h

No idea if it's usable

[Kevin Buzzard]

import tactic

def add_equiv_of_eq {ι : Type*} {β : ι → Type*} [Π i, add_monoid (β i)]
  {i j : ι} (h : i = j) : β i ≃+ β j :=
eq.rec (add_equiv.refl (β i)) h

variables {ι : Type*} {β : ι → Type*} [Π i, add_monoid (β i)]
  {i j : ι} (h : i = j)

-- go to j and then back again
def test : β i ≃+ β i := (add_equiv_of_eq h).trans (add_equiv_of_eq h.symm)

example (x : β i) (h : i = j) : test h x = x :=
begin
  simp [test, add_equiv_of_eq],
  /-
  ⊢ ⇑(eq.rec (add_equiv.refl (β j)) _) (⇑(eq.rec (add_equiv.refl (β i)) h) x) = x
  -/
  sorry -- no idea how to proceed
end

I can't use it, at least. Are you in a situation where all you care about is the isomorphism and you never need to "evaluate" it?

[Pierre-Alexandre Bazin]

Trying to do it using equiv.cast, I ended up with this :

example {ι : Type*} {β : ι → Type*} [Π i, add_monoid (β i)] {i j : ι} (h : i = j) : β i ≃+ β j :=
{ map_add' := λ x y, begin
  apply (equiv.cast_eq_iff_heq $ congr_arg β h).mpr, convert heq.rfl,
  repeat { exact h.symm }, repeat { apply cast_heq },
end,
  ..equiv.cast (congr_arg β h) }

I don't know if it's more usable

[Kevin Buzzard]

Why do you need it? Just to make statements of the form "these things are isomorphic", or do you ever need to "compute" the isomorphism?

[Kevin Buzzard]

If you are in a situation where you can use subst then it seems that you can reduce computations to heq:

example (x : β i) : x == add_equiv_of_eq h x :=
begin
  subst h,
  apply heq_of_eq,
  refl,
end

[Pierre-Alexandre Bazin]

Indeed this works well (and from there you should be able to prove your test h x = x, by proving first test h x == xby transitivity)

My goal was to be able to reindex a direct sum, so I have an equiv h between the indices and at some point I needed the equiv between β i and β (h (h.symm i))

[Kevin Buzzard]

I see. Yes this is exactly the situation where you need something like the construction above.