power set injective

Stream: new members

[Joachim Breitner]

Bedtime, but before I sign off, allow me to leave this question here. How would I best go about the following lemma?

lemma helper {A B} : (A → bool) ≃ (B → bool) → (A ≃ B) := sorry,

Turn it into a statement about cardinal numbers and the power function there? Or is that too big of a hammer?

[Eric Wieser]

Note that that's a def not a lemma, as the result is an equiv which is data

[Reid Barton]

I think this isn't provable
https://mathoverflow.net/questions/67473/equality-of-cardinality-of-power-set

[Eric Wieser]

If you have [fintype A] [fintype B] is there an choice-free algorithm to construct such an equiv?

[Joachim Breitner]

Hmm, ok, so the reason why in my Isabelle development I went this way only for finite A and B was _not_ due to Isabelle somehow. Thanks for reminding me :-)
So I’ll restrict that helper to finite sets and do my main prove separately for infinite sets; that’s fine.

[Eric Wieser]

Ah, that's in the comments on that mathoverflow question too (with answer no)

[Patrick Johnson]

With fintype restrictions, the definition becomes trivial:

noncomputable def equiv_of_equiv_powerset {α β : Sort*} [fintype α] [fintype β]
  (e : (α → bool) ≃ (β → bool)) : α ≃ β :=
begin
  refine (_ : nonempty _).some, have h := (⟨e⟩ : nonempty _),
  rw ←fintype.card_eq at h ⊢, simp at h,
  exact (strict_mono_pow dec_trivial).injective h,
end

[Eric Wieser]

From the mathoverflow post, apparently "Producing New Bijections from Old" makes the claim it is impossible to make that computably.

[Eric Rodriguez]

i find that somewhat sensible; i find it surprising that A2 equiv B2 leads you to a computable A equiv B, however

[Eric Rodriguez]

Also, isn't the "canonical" way to write the powerset of A set A?

[Eric Wieser]

A → bool is the type of sets with decidable membership