fintype.card of coerced set

Stream: new members

[Eric Wieser]

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]

(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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

And card of prod is prod of cards

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

The range as a subtype, I assume

[Kevin Buzzard]

Sure

[Eric Wieser]

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]

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

[Eric Wieser]

No, it just arises from unfolding sum_congr_subgroup

[Eric Wieser]

I thought that it might make the problem simpler

[Reid Barton]

I mean why introduce the subgroup in the first place

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

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]

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]

but you haven't thrown away the information of sl and sr that you're trying to recover in the other thread

[Eric Wieser]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Eric Wieser]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

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]

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