heq

Stream: general

[Sebastien Gouezel]

Suppose that I have f : fin k -> alpha and g : fin n -> alpha, and I know f == g. Can I deduce k = n?

[Chris Hughes]

I think only if alpha is finite and has cardinality at least 2. You know the types are equal, but types with the same cardinality are not provably unequal.

[Chris Hughes]

If nonempty types are equal, then they must have a pair of elements that are heq.

[Yury G. Kudryashov]

It's fin k and fin n, so their cardinalities are the same only if k = n.

[Sebastien Gouezel]

Yes, if alpha is finite I can do it by cardinality arguments. I guess that if alpha is infinite then this does not follow from Lean's axioms, but I might be wrong on this.

[Yury G. Kudryashov]

Ah, it's fin k → α, not fin k.

[Yury G. Kudryashov]

I should read more carefully.

[Yury G. Kudryashov]

And think before typing.

[Kevin Buzzard]

You're a mathematician so if you have f == g then you already went wrong somewhere earlier, right?

[Sebastien Gouezel]

No, it's when building an equiv between some objects, you start from a function fin k -> alpha, then you apply to_fun, then inv_fun, and in the end you get a function fin n -> alpha, and you need to prove that it is the same function as the one you started with. You get into == quickly with this, but it's not really bad, you can prove that k = n and then do induction on the equality and you are back on track. If I could have deduced k = n from f == g, this would have saved me a few lines, but I can prove it directly in my context.

[Kevin Buzzard]

I was in this situation with quotient groups at some point in the perfectoid project and just proved some stupid lemmas, like e.g. I defined a map from G/N to G/K if K and N were normal subgroups and N=K(!)