## Stream: general

### Topic: heq

#### 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?

#### 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.

#### Chris Hughes (Apr 09 2020 at 19:28):

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

#### 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.

#### 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.

#### Yury G. Kudryashov (Apr 09 2020 at 19:36):

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

#### Yury G. Kudryashov (Apr 09 2020 at 19:37):

And think before typing.

#### 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?

#### 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.

#### 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