Using equality of types in function definition

Stream: Is there code for X?

[Daniel Morrison]

For context, I've just finished defining the wedge product as a bilinear map $\bigwedge^k V \to \bigwedge^l V \to \bigwedge^{(k+l)} V$ and I want to use it in the context of $\bigwedge^k V \to \bigwedge^{(n-k)} V \to \bigwedge^n V$ (for $k \leq n$). But Lean interprets this as a map into $\bigwedge^{(k+(n-k))} V$ and I need to tell it this is the same as $\bigwedge^n V$.

I was able to use the ▸ macro to tell Lean to do this modification, but I then ran into the problem where I need to show this map is linear and so I need something saying the casting operation is linear.

My question is, how can I work with a proof involving casted elements? I couldn't find any appropriate theorems for my case. Alternatively, is there a better way for me to get the outcome I want?

[Kevin Buzzard]

Why don't you set up the theory as linear maps from wedge a -> wedge b -> wedge a+b and then worry later on about the task of showing that if x=y then wedge x and wedge y are isomorphic?

[Jireh Loreaux]

Kevin's comment contains the key thing you're missing: you dont' want to show that $\bigwedge^{k + (n - k)} V$ is equal to $\bigwedge^n V$ (because equality of types is evil), you want to show that they are isomorphic.

[Johan Commelin]

cc @Sam Lindauer who has also been working on wedge products.

[Michael Stoll]

Maybe construct $\bigwedge^k V \to \bigwedge^l V \to \bigwedge^m V$ from a proof that $m = k + l$ instead?

[Jz Pan]

Seems that you need something looks like docs#IntermediateField.equivOfEq

[Daniel Morrison]

Thank you all! I had hoped I could avoid using more maps but it seems that would be a bad idea.

[Kyle Miller]

@Michael Stoll Since these are linear, maybe there's no need for m = k + l as a hypothesis, and it could be defined to be the zero map when that constraint doesn't hold.

[Mitchell Lee]

This message by Riccardo Brasca describes how a similar problem showed up in the formalization of chain complexes and goes into detail about how it was fixed: #maths > challenges in the translation from a set proof to DTT? @ 💬