# Zulip Chat Archive

## Stream: new members

### Topic: fintype.card of coerced set

#### Eric Wieser (Dec 12 2020 at 20:45):

This looks like a fairly trivial statement, but I can't work out how to eliminate the coercion to sort:

```
example {ιa : Type*} {ιb : Type*}
[decidable_eq ιa]
[decidable_eq ιb]
[fintype ιa]
[fintype ιb] :
fintype.card (set_of
(λ (σ : equiv.perm (ιa ⊕ ιb)),
∃ (sl : equiv.perm ιa) (sr : equiv.perm ιb),
σ = sl.sum_congr sr)) =
fintype.card (equiv.perm ιa) * fintype.card (equiv.perm ιb) :=
begin
sorry,
end
```

#### Eric Wieser (Dec 12 2020 at 20:46):

(I know that I'll need to show that docs#equiv.perm.sum_congr is injective in each argument, but I can't see how to actually apply that here)

#### Kevin Buzzard (Dec 12 2020 at 20:59):

Why not just construct the equiv between your set and perm ia x perm ib?

#### Kevin Buzzard (Dec 12 2020 at 21:00):

The card thing is just noise because we have equiv -> same card

#### Kevin Buzzard (Dec 12 2020 at 21:00):

And card of prod is prod of cards

#### Kevin Buzzard (Dec 12 2020 at 21:01):

Oh I see you're not asking how to prove it

#### Kevin Buzzard (Dec 12 2020 at 21:02):

Why not just make the subtype or the subgroup or whatever. Maybe I don't understand the question

#### Eric Wieser (Dec 12 2020 at 21:11):

Put simply, I want to show the cardinality of the range of `sum_congr`

is the product of the cardinality of the domains

#### Eric Wieser (Dec 12 2020 at 21:12):

I have the subgroup (docs#equiv.perm.sum_congr_subgroup), and getting the card of that is really what I want to prove

#### Kevin Buzzard (Dec 12 2020 at 22:55):

Prove an equiv between the range and the product of the domains

#### Eric Wieser (Dec 12 2020 at 22:57):

The range as a subtype, I assume

#### Kevin Buzzard (Dec 12 2020 at 22:59):

Sure

#### Eric Wieser (Dec 13 2020 at 13:14):

Defining that obvious equivalence is proving to be frustrating: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Getting.20a.20hypothesis.20that.20agrees.20with.20the.20match.20branch/near/219760278

#### Reid Barton (Dec 13 2020 at 13:43):

Do you need to ever introduce this `{σ | ∃ (sl : equiv.perm ιa) (sr : equiv.perm ιb), σ = sl.sum_congr sr}`

at all?

#### Eric Wieser (Dec 13 2020 at 13:45):

No, it just arises from unfolding `sum_congr_subgroup`

#### Eric Wieser (Dec 13 2020 at 13:45):

I thought that it might make the problem simpler

#### Reid Barton (Dec 13 2020 at 13:46):

I mean why introduce the subgroup in the first place

#### Reid Barton (Dec 13 2020 at 13:46):

Working with a subset forces you to throw away data, the `sl`

and `sr`

#### Eric Wieser (Dec 13 2020 at 13:47):

I need the subgroup in order to work with it's quotient group

#### Reid Barton (Dec 13 2020 at 13:47):

Well, if you need it for some reason I would try to replace it by `equiv.perm ιa \x equiv.perm ιb`

as soon as possible

#### Reid Barton (Dec 13 2020 at 13:49):

obviously there's no problem in proving that `sum_congr`

is injective as a function on `equiv.perm ιa \x equiv.perm ιb`

, so this is just as good as the subgroup

#### Reid Barton (Dec 13 2020 at 13:49):

but you haven't thrown away the information of `sl`

and `sr`

that you're trying to recover in the other thread

#### Eric Wieser (Dec 13 2020 at 13:50):

But I can't take the quotient group by that product, without passing through `sum_congr`

first

#### Reid Barton (Dec 13 2020 at 13:53):

well if the answer to "what do you use X for" is always literally a single Lean term applied to X then this conversation will be rather inefficient

#### Eric Wieser (Dec 13 2020 at 13:54):

I have a PR pushed showing how I use this subgroup, I think~~ #5279~~ #5269

#### Reid Barton (Dec 13 2020 at 13:54):

but what I'm trying to get across is that an object like `{σ | ∃ (sl : equiv.perm ιa) (sr : equiv.perm ιb), σ = sl.sum_congr sr}`

, while it looks fine for a human because we know that `σ`

determines `sl`

and `sr`

, is actually pretty awkward to deal with in Lean

#### Eric Wieser (Dec 13 2020 at 13:58):

What I want to use in #5269 is the permutations under an equivalence class that ignores internal permutations within a and b

#### Eric Wieser (Dec 13 2020 at 13:58):

And the quotient by this awkward-to-deal-with subgroup seemed the easiest way to do that

#### Reid Barton (Dec 13 2020 at 14:01):

So for example the question which started this thread is trivial and doesn't require writing down a formula for the inverse, because `sum_congr`

is injective so it's a bijection onto its image

#### Eric Wieser (Dec 13 2020 at 14:02):

Right, but Kevin's suggestion to construct the cardinality via an equiv suggested I did need the inverse

#### Reid Barton (Dec 13 2020 at 14:02):

And classically you could conjure up an inverse using choice, so logically it's not necessary to have a formula for the inverse at all

#### Reid Barton (Dec 13 2020 at 14:03):

Well, you're not required to do everything Kevin suggests

#### Reid Barton (Dec 13 2020 at 14:03):

Actually you could conjure up an inverse even without choice, since everything is finite and decidable

#### Eric Wieser (Dec 13 2020 at 14:04):

That's what I'd really like to know how to do

#### Reid Barton (Dec 13 2020 at 14:10):

Clearly it must be possible to implement this `inv_sum_congr`

, but it seems easier to just avoid needing it in the first place.

#### Eric Wieser (Dec 13 2020 at 14:13):

Is there an easy way to convert my subgroup with a fintype instance into the finset that is its carrier? Then I assume I could use some lemmas about finset.card_image or something

Last updated: Dec 20 2023 at 11:08 UTC