Zulip Chat Archive

Stream: general

Topic: heq


view this post on Zulip Sebastien Gouezel (Apr 09 2020 at 19:21):

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

view this post on Zulip Chris Hughes (Apr 09 2020 at 19:26):

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.

view this post on Zulip Chris Hughes (Apr 09 2020 at 19:28):

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

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 19:29):

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

view this post on Zulip Sebastien Gouezel (Apr 09 2020 at 19:35):

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.

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 19:36):

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

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 19:36):

I should read more carefully.

view this post on Zulip Yury G. Kudryashov (Apr 09 2020 at 19:37):

And think before typing.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 19:41):

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

view this post on Zulip Sebastien Gouezel (Apr 09 2020 at 20:00):

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.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 20:01):

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(!)


Last updated: May 11 2021 at 14:11 UTC