Stuck (again) with typecasting in dependent direct sums

Stream: new members

[Marcus Zibrowius]

Given a direct sum indexed by ι₁ and a map f : ι₁ → ι₂, I want to rearrange the the terms into a double sum with the outer sum indexed by ι₂. That is, I want to construct an isomorphism that looks as follows:
image.png

I have some definition of this isomorphism, but I cannot show that the following diagram commutes:
image.png

My idea is to define the isomorphism as a composition of two isos, to prove as lemmas that each iso is compatible with inclusions of summands (“lof”), and then to piece these two lemmas together. It's the last step (piecing them together) that fails. I post below the code I have, diagrams explaining my definition and my two lemmas (to myself if not to anyone else) and the error message I get.

import Mathlib

open Classical
namespace DirectSum
variable (R : Type) [CommRing R]

lemma sigmaLcurry_lof
  {ι : Type} [DecidableEq ι]
  {α : ι → Type} [∀ j : ι, DecidableEq (α j)]
  {M : (j : ι) → α j → Type}  [∀ j : ι, ∀ a : α j, AddCommMonoid (M j a)] [∀ j : ι, ∀ a : α j, Module R (M j a)]
  (x : (j : ι) × α j) (m : M x.fst x.snd) :
  (sigmaLcurry R) ((lof R ((j : ι) × α j) (fun x' ↦ M x'.fst x'.snd) x ) m)
= (lof R ι (fun j' ↦ ⨁ (a' : α j'), M j' a') x.fst) ((lof R (α x.fst) (fun a' ↦ M x.fst a') x.snd ) m) := by
  exact DFinsupp.sigmaCurry_single x m

lemma lequivCongrLeft_lof {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (k : κ) (m : M (h.symm k)) :
  (lequivCongrLeft R h) ((lof R ι M (h.symm k)) m )  = (lof R κ (fun k ↦ M (h.symm k)) k) m := by exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv k m

lemma lequivCongrLeft_lof' {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (i : ι) (m : M i) :
  (lequivCongrLeft R h) ((lof R ι M i) m )  = (lof R κ (fun k ↦ M (h.symm k)) (h i)) ((h.symm_apply_apply i).symm ▸ m) := by sorry -- [I have some convoluted proof of this]

variable {ι₁ ι₂: Type} [DecidableEq ι₂]
variable {M : ι₁ → Type} [∀ i : ι₁, AddCommMonoid (M i)] [∀ i : ι₁, Module R (M i)]

def DirectSum.sigmaFiberLinearEquiv (f : ι₁ → ι₂) :
    (DirectSum ι₁ fun i ↦ M i) ≃ₗ[R] DirectSum ι₂ fun j ↦ (DirectSum { i : ι₁ // f i = j} fun i ↦ M i) := by
  let h := (Equiv.sigmaFiberEquiv f).symm
  have iso₁ := DirectSum.lequivCongrLeft R h (M := M)
  have iso' : (DirectSum (Σ j : ι₂, { i : ι₁ // f i = j }) fun k ↦ M (h.symm k)) ≃ₗ[R] (DirectSum (Σ j : ι₂, { i : ι₁ // f i = j }) fun k ↦ M ↑k.snd) := by rfl
  have iso₂ := DirectSum.sigmaLcurryEquiv R (δ := fun (j : ι₂) ↦ (fun (i : { i : ι₁ // f i = j}) ↦ M i))
  exact iso₁.trans (iso'.trans iso₂)


lemma DirectSum.sigmaFiberLinearEquiv_lof (f : ι₁ → ι₂) (i : ι₁) (m : M i) :
  (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m) = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by
  simp only [DirectSum.sigmaFiberLinearEquiv,LinearEquiv.trans_apply,Equiv.symm_symm]
  rw [DirectSum.lequivCongrLeft_lof' (R := R) (m := m) (h := (Equiv.sigmaFiberEquiv f).symm)]

Goal in last line:

⊢ (sigmaLcurryEquiv R)
    ((LinearEquiv.refl R (⨁ (k : (j : ι₂) × { i // f i = j }), M ((Equiv.sigmaFiberEquiv f) k)))
      ((lequivCongrLeft R (Equiv.sigmaFiberEquiv f).symm) ((lof R ι₁ M i) m))) =
  (lof R ι₂ (fun i => ⨁ (i_1 : { i_1 // f i_1 = i }), M ↑i_1) (f i))
    ((lof R { i' // f i' = f i } (fun i' => M ↑i') ⟨i, ⋯⟩) m)

Error message in last line:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  (lequivCongrLeft R (Equiv.sigmaFiberEquiv f).symm) ((lof R ι₁ M i) m)

I'm pretty sure it's a typecasting problem related to the difference between (Equiv.sigmaFiberEquiv f).symm x and x.snd, but I cannot find a way to deal with it. I thought it might help to introduced the auxiliary isomorphism iso' in my definition, but that does not appear to make any difference.

image.png
image.png
image.png

[Kenny Lau]

@Marcus Zibrowius you have lost all information when you used have in a def

[Kenny Lau]

if you want to make the code readable, you should use calc instead of let/have.

[Marcus Zibrowius]

Indeed, I don’t know why I used have for something that's not a proposition. But why shouldn’t I use let? In any case, I don’t think this is related to my problem. Even if I write the whole definition of sigmaFiberLinearEquiv in one line, I still get the same proof state and error at the end:

import Mathlib

open Classical
namespace DirectSum
variable (R : Type) [CommRing R]

lemma sigmaLcurry_lof
  {ι : Type} [DecidableEq ι]
  {α : ι → Type} [∀ j : ι, DecidableEq (α j)]
  {M : (j : ι) → α j → Type}  [∀ j : ι, ∀ a : α j, AddCommMonoid (M j a)] [∀ j : ι, ∀ a : α j, Module R (M j a)]
  (x : (j : ι) × α j) (m : M x.fst x.snd) :
  (sigmaLcurry R) ((lof R ((j : ι) × α j) (fun x' ↦ M x'.fst x'.snd) x ) m)
= (lof R ι (fun j' ↦ ⨁ (a' : α j'), M j' a') x.fst) ((lof R (α x.fst) (fun a' ↦ M x.fst a') x.snd ) m) := by
  exact DFinsupp.sigmaCurry_single x m

lemma lequivCongrLeft_lof {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (k : κ) (m : M (h.symm k)) :
  (lequivCongrLeft R h) ((lof R ι M (h.symm k)) m )  = (lof R κ (fun k ↦ M (h.symm k)) k) m := by exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv k m

lemma lequivCongrLeft_lof' {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (i : ι) (m : M i) :
  (lequivCongrLeft R h) ((lof R ι M i) m )  = (lof R κ (fun k ↦ M (h.symm k)) (h i)) ((h.symm_apply_apply i).symm ▸ m) := by sorry -- [I have some convoluted proof of this]

variable {ι₁ ι₂: Type} [DecidableEq ι₂]
variable {M : ι₁ → Type} [∀ i : ι₁, AddCommMonoid (M i)] [∀ i : ι₁, Module R (M i)]

def sigmaFiberLinearEquiv (f : ι₁ → ι₂) :
    (DirectSum ι₁ fun i ↦ M i) ≃ₗ[R] DirectSum ι₂ fun j ↦ (DirectSum { i : ι₁ // f i = j} fun i ↦ M i) :=
    DirectSum.lequivCongrLeft R (Equiv.sigmaFiberEquiv f).symm (M := M).trans
    (DirectSum.sigmaLcurryEquiv R (δ := fun (j : ι₂) ↦ (fun (i : { i : ι₁ // f i = j}) ↦ M i)))

lemma sigmaFiberLinearEquiv_lof (f : ι₁ → ι₂) (i : ι₁) (m : M i) :
  (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m) = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by
  simp only [DirectSum.sigmaFiberLinearEquiv,LinearEquiv.trans_apply,Equiv.symm_symm]
  rw [DirectSum.lequivCongrLeft_lof' (R := R) (m := m) (h := (Equiv.sigmaFiberEquiv f).symm)]

[Marcus Zibrowius]

If I attempt to prove the lemma with calc, then the rewriting step that gives an error above works, but does not close the intermediate goal. What is printed as intermediate goal looks like an identity of the form A = A to me, but rfl doesn’t close it. I guess this is still the same problem as before, in a different guise.

import Mathlib

open Classical
namespace DirectSum
variable (R : Type) [CommRing R]

lemma sigmaLcurry_lof
  {ι : Type} [DecidableEq ι]
  {α : ι → Type} [∀ j : ι, DecidableEq (α j)]
  {M : (j : ι) → α j → Type}  [∀ j : ι, ∀ a : α j, AddCommMonoid (M j a)] [∀ j : ι, ∀ a : α j, Module R (M j a)]
  (x : (j : ι) × α j) (m : M x.fst x.snd) :
  (sigmaLcurry R) ((lof R ((j : ι) × α j) (fun x' ↦ M x'.fst x'.snd) x ) m)
= (lof R ι (fun j' ↦ ⨁ (a' : α j'), M j' a') x.fst) ((lof R (α x.fst) (fun a' ↦ M x.fst a') x.snd ) m) := by
  exact DFinsupp.sigmaCurry_single x m

lemma lequivCongrLeft_lof {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (k : κ) (m : M (h.symm k)) :
  (lequivCongrLeft R h) ((lof R ι M (h.symm k)) m )  = (lof R κ (fun k ↦ M (h.symm k)) k) m := by exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv k m

lemma lequivCongrLeft_lof' {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (i : ι) (m : M i) :
  (lequivCongrLeft R h) ((lof R ι M i) m )  = (lof R κ (fun k ↦ M (h.symm k)) (h i)) ((h.symm_apply_apply i).symm ▸ m) := by sorry -- [I have some convoluted proof of this]

variable {ι₁ ι₂: Type} [DecidableEq ι₂]
variable {M : ι₁ → Type} [∀ i : ι₁, AddCommMonoid (M i)] [∀ i : ι₁, Module R (M i)]

def sigmaFiberLinearEquiv (f : ι₁ → ι₂) :
    (DirectSum ι₁ fun i ↦ M i) ≃ₗ[R] DirectSum ι₂ fun j ↦ (DirectSum { i : ι₁ // f i = j} fun i ↦ M i) :=
    DirectSum.lequivCongrLeft R (Equiv.sigmaFiberEquiv f).symm (M := M).trans
    (DirectSum.sigmaLcurryEquiv R (δ := fun (j : ι₂) ↦ (fun (i : { i : ι₁ // f i = j}) ↦ M i)))


lemma sigmaFiberLinearEquiv_lof (f : ι₁ → ι₂) (i : ι₁) (m : M i) :
  (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m) = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by
  let h := (Equiv.sigmaFiberEquiv f).symm
  calc (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m)
     _ = (sigmaLcurryEquiv R) ((lequivCongrLeft R (Equiv.sigmaFiberEquiv f).symm) ((lof R ι₁ M i) m)) := by simp [sigmaFiberLinearEquiv]
     _ = (sigmaLcurryEquiv R) ((lof R ((y : ι₂) × { x // f x = y }) (fun k => M ((Equiv.sigmaFiberEquiv f).symm.symm k)) ((Equiv.sigmaFiberEquiv f).symm i)) ((h.symm_apply_apply i).symm ▸ m)) := by
         rw [lequivCongrLeft_lof']
         sorry -- proof state here looks like `A = A` to me
     _ = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by sorry

[Aaron Liu]

Marcus Zibrowius said:

What is printed as intermediate goal looks like an identity of the form A = A to me, but rfl doesn’t close it.

If I congr I get the goal

⊢ (fun a b => propDecidable (a = b)) = fun a b => a.instDecidableEqSigma b

don't just put open Classical at the top of your file and expect it to solve all your decidability problems

[Aaron Liu]

anyways you can fix this with Subsingleton.elim

[Aaron Liu]

or you can use the subsingleton tactic which I just learned about now

[Marcus Zibrowius]

Aaron Liu said:

don't just put open Classical at the top of your file and expect it to solve all your decidability problems

Well, I never knew this was an decidabilty problem. And I don’t think I would ever have found out on my own … Thanks a lot!

[Aaron Liu]

What gave you the idea to start out with open Classical?

[Marcus Zibrowius]

I don’t remember where I saw this, but I simply found it a bite tiresome to spell out [DecidableEq ι] every time I introduce a new indexing set. And I thought “I’m anyways only interested in classical logic, so this can’t do any harm.”

[Marcus Zibrowius]

Is there an easy way I could have found out that I have a “decidabilty problem” in the initial proof attempt, without calc, where rw gave me an error of the form “cannot find A in … A … ”?

[Aaron Liu]

I ran the congr tactic

[Aaron Liu]

It told me what needed to be equal that wasnt equal

[Aaron Liu]

Also useful is convert, for when supplying a term that looks the same but isn't

[Marcus Zibrowius]

You mean, you ran cong here??

lemma sigmaFiberLinearEquiv_lof (f : ι₁ → ι₂) (i : ι₁) (m : M i) :
  (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m) = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by
  simp only [DirectSum.sigmaFiberLinearEquiv,LinearEquiv.trans_apply,Equiv.symm_symm]
  congr

And then looked through the 13 goals it produced?

I thought you ran congr in the middle of the calc proof, where it immediately produces the line you shared.

[Aaron Liu]

Marcus Zibrowius said:

I don’t remember where I saw this, but I simply found it a bite tiresome to spell out [DecidableEq ι] every time I introduce a new indexing set. And I thought “I’m anyways only interested in classical logic, so this can’t do any harm.”

Well now you know the harm it can do, so be a bit more careful in the future when you have open Classical I guess

[Aaron Liu]

Marcus Zibrowius said:

I thought you ran congr in the middle of the calc proof, where it immediately produces the line you shared.

I went to the place you had sorry -- proof state here looks like `A = A` to me and I put congr before the sorry

[Marcus Zibrowius]

Yes, ok. That’s what I thought.

[Marcus Zibrowius]

My question was whether I could already have found out what’s wrong in the middle of the previous proof attempt. I’ll post it again for clarity.

import Mathlib

open Classical
namespace DirectSum
variable (R : Type) [CommRing R]

lemma sigmaLcurry_lof
  {ι : Type} [DecidableEq ι]
  {α : ι → Type} [∀ j : ι, DecidableEq (α j)]
  {M : (j : ι) → α j → Type}  [∀ j : ι, ∀ a : α j, AddCommMonoid (M j a)] [∀ j : ι, ∀ a : α j, Module R (M j a)]
  (x : (j : ι) × α j) (m : M x.fst x.snd) :
  (sigmaLcurry R) ((lof R ((j : ι) × α j) (fun x' ↦ M x'.fst x'.snd) x ) m)
= (lof R ι (fun j' ↦ ⨁ (a' : α j'), M j' a') x.fst) ((lof R (α x.fst) (fun a' ↦ M x.fst a') x.snd ) m) := by
  exact DFinsupp.sigmaCurry_single x m

lemma lequivCongrLeft_lof {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (k : κ) (m : M (h.symm k)) :
  (lequivCongrLeft R h) ((lof R ι M (h.symm k)) m )  = (lof R κ (fun k ↦ M (h.symm k)) k) m := by exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv k m

lemma lequivCongrLeft_lof' {ι : Type} {M : ι → Type}
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type} (h : ι ≃ κ) (i : ι) (m : M i) :
  (lequivCongrLeft R h) ((lof R ι M i) m )  = (lof R κ (fun k ↦ M (h.symm k)) (h i)) ((h.symm_apply_apply i).symm ▸ m) := by sorry -- [I have some convoluted proof of this]

variable {ι₁ ι₂: Type} [DecidableEq ι₂]
variable {M : ι₁ → Type} [∀ i : ι₁, AddCommMonoid (M i)] [∀ i : ι₁, Module R (M i)]

def sigmaFiberLinearEquiv (f : ι₁ → ι₂) :
    (DirectSum ι₁ fun i ↦ M i) ≃ₗ[R] DirectSum ι₂ fun j ↦ (DirectSum { i : ι₁ // f i = j} fun i ↦ M i) :=
    DirectSum.lequivCongrLeft R (Equiv.sigmaFiberEquiv f).symm (M := M).trans
    (DirectSum.sigmaLcurryEquiv R (δ := fun (j : ι₂) ↦ (fun (i : { i : ι₁ // f i = j}) ↦ M i)))

lemma sigmaFiberLinearEquiv_lof (f : ι₁ → ι₂) (i : ι₁) (m : M i) :
  (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m) = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by
  simp only [DirectSum.sigmaFiberLinearEquiv,LinearEquiv.trans_apply,Equiv.symm_symm]
  rw [DirectSum.lequivCongrLeft_lof' (R := R) (m := m) (h := (Equiv.sigmaFiberEquiv f).symm)]

[Marcus Zibrowius]

Writing out these long equations in calc blocks feels like typing a lot of redundancy.

[Aaron Liu]

Here's what I got

lemma sigmaFiberLinearEquiv_lof (f : ι₁ → ι₂) (i : ι₁) (m : M i) :
  (sigmaFiberLinearEquiv R f) ((lof R ι₁ _ i) m) = (lof R ι₂ _ (f i)) ((lof R { i' : ι₁ // f i' = f i} (fun i' ↦ M i') ⟨i, rfl⟩) m) := by
  simp only [DirectSum.sigmaFiberLinearEquiv,LinearEquiv.trans_apply,Equiv.symm_symm]
  conv =>
    enter [1, 2]
    -- rw [DirectSum.lequivCongrLeft_lof' (R := R) (m := m) (h := (Equiv.sigmaFiberEquiv f).symm)]
    -- now it works (weird)
    exact DirectSum.lequivCongrLeft_lof' (R := R) (m := m) (h := (Equiv.sigmaFiberEquiv f).symm)
  sorry

[Aaron Liu]

and now it works so I can continue with what I was doing before and maybe if I remember I'll come back and try to figure out why rw was being so weird

[Marcus Zibrowius]

OK, thanks a lot for helping me!