Equiv.cast for structures

Stream: mathlib4

[loooong]

I want to show that if given a family of structures, then equal index implies equivalent structures. the example is following:

import Mathlib.Algebra.Hom.Equiv.Basic

variable (α : Type _)(f : α → Type _)[∀i, AddCommGroup (f i)]

def AddEquiv.cast (a b: α)(p:a=b): f a ≃+ f b := by
  constructor
  swap
  apply Equiv.cast
  rw [p]
  intro x y
  simp
  unfold cast
  simp
  sorry

what should I do?

[Eric Wieser]

This is false in general, I think

[loooong]

Why? I think it should be right in usual math.

[Eric Wieser]

Oh you're right, I'm thinking of something different:

import Mathlib.Algebra.Hom.Equiv.Basic

variable (α : Type _) (f : α → Type _) [∀i, AddCommGroup (f i)]

def AddEquiv.cast (a b : α)(p : a = b) : f a ≃+ f b where
  __ := Equiv.cast (congr_arg _ p)
  map_add' x y := by cases p; rfl

[Eric Wieser]

This is the false one:

variable (A B : Type _) [AddCommGroup A] [AddCommGroup B]

def AddEquiv.cast (p : A = B) : A ≃+ B where
  __ := Equiv.cast p
  map_add' x y := sorry

[loooong]

Thank you, I'm considering a version of this theorem for modules.

[loooong]

I think this kind of theorem can be added in mathlib

[Anatole Dedecker]

Could you tell us a bit more about what you'd need that for? The reason we don't have those is because the statement is not super natural (because you're not only using that the types are equal, also that the structures are equal), so that may be an #xy problem

[loooong]

I'm trying to formalize spectral sequence for filtered complex (module version), where I meet a lot of index. we know complex can be viewed as function from Z to Modules, so I want the fact that equal index induces equivalent modules. In particular, I want C (p - r + (q + r - 1)) ≃ₗ[R] C (p + q - 1) for a complex C.

[loooong]

Lean cannot replace these index automatically, this is very surprise me.

[Anatole Dedecker]

For this kind of thing you probably want to used the type of bundled modules docs#ModuleCat used in the category theory part of the library. Then you no longer have the issue Eric mentioned above, since the structure comes with the type. But I'll let people more familiar with the category theory library comment more on that.

[Eric Wieser]

Often in concrete cases there is a better implementation than the cast above; for instance, docs#Fin.cast when f = Fin, docs#PiTensorProduct.reindex, etc

[loooong]

Your comment is helpful, I will try to use CategoryTheory.iso.refl fix the problem.

[Eric Wieser]

You might find some of the discussion in Section 2.1 of my "Graded Rings in Lean’s Dependent Type Theory" interesting

[Anatole Dedecker]

Eric Wieser said:

Often in concrete cases there is a better implementation than the cast above; for instance, docs#Fin.cast when f = Fin, docs#PiTensorProduct.reindex, etc

Well in this context you definitely want to allow any module (ignoring universe issues) so I'm not sure if that applies

[Eric Wieser]

I misread "for a complex C" as "for a complicated C"