No surjection from a set to its powerset

Stream: new members

[Gihan Marasingha]

I know mathlib has the theorem cantor_surjective, that given {α} (f : α → set α), we have ¬ function.surjective f. Can one prove a similar statement given (S : set α) (f : S → 𝒫 S)?

I've attempted this, but I come a cropper because I'm trying apply surjectivity to a term of the wrong type. Here's the start of my attempt. The problem is that I'm applying h with a term of type set ↥S rather than one of type ↥𝒫 S. Can this be fixed?

import data.set

example {α} (S : set α) (f : S → 𝒫 S) : ¬ function.surjective f :=
begin
  haveI := classical.prop_decidable,
  intro h,
  cases h { b : S | (b : α) ∉ (f b : set α)} with x hx, -- This fails.
/-  by_cases k : x ∈ f x,
  { have : x ∉ f x,
    { rwa [hx, nmem_set_of_eq, not_not_mem], },
    exact this k, },
  { have : x ∈ f x,
    { rwa [hx, mem_set_of_eq], },
    exact k this, }, -/
end

[Mario Carneiro]

why not just turn it into an instance of cantor_surjective?

[Mario Carneiro]

also #mwe

[Gihan Marasingha]

Ah sorry, I've added the import.

[Gihan Marasingha]

OK, so how would I apply cantor_surjective in this case to get the desired result?

[Mario Carneiro]

def equiv.set.powerset {α} (S : set α) : 𝒫 S ≃ set S := sorry

[Gihan Marasingha]

Thanks. I haven't come across equiv before. I'll think about this and come back if I get stuck.

[Mario Carneiro]

def equiv.set.powerset {α} (S : set α) : 𝒫 S ≃ set S :=
⟨λ x, {y | (y : α) ∈ (x : set α)},
 λ x, ⟨coe '' x, by rintro _ ⟨a, _, rfl⟩; exact a.2⟩,
 λ x, by ext y; exact ⟨λ ⟨⟨_, _⟩, h, rfl⟩, h, λ h, ⟨⟨_, x.2 h⟩, h, rfl⟩⟩,
 λ x, by ext; simp⟩

example {α} (S : set α) (f : S → 𝒫 S) : ¬ function.surjective f :=
mt (equiv.surjective _).comp (function.cantor_surjective (equiv.set.powerset S ∘ f))

[Kevin Buzzard]

When I do this with Imperial 1st years I just use types:

import data.set

open_locale classical

open set

example (S : Type) (f : S → set S) : ¬ function.surjective f :=
begin
  intro h,
  cases h { b : S | b ∉ f b} with x hx,
  by_cases k : x ∈ f x,
  { have : x ∉ f x,
    { rw hx at k, exact k },
    contradiction, },
  { have : x ∈ f x,
    { rwa hx, },
    contradiction, },
end

[Kevin Buzzard]

I just tell them that a type is a collection of stuff in type theory, like a set is a collection of stuff in set theory.

[Mario Carneiro]

Although I think it is interesting how shockingly short the mathlib proof of cantor_surjective is

[Gihan Marasingha]

@Kevin Buzzard . Thanks. I feel less bad about trying a classical proof (given that function.cantor_surjective is constructive).

[Mario Carneiro]

it actually uses that ever popular lemma from TPIL that is not obviously constructive: not (p <-> not p)

[Gihan Marasingha]

Oh, good to know! I take it then the result is not true using constructive reasoning?

Edit: I can't read. Ignore this comment.

[Kevin Buzzard]

not (p <-> not p) can be proved constructively, rather surprisingly

[Gihan Marasingha]

@Kevin Buzzard when teaching do you avoid discussing power sets entirely (treating set S as a 'power type') or do you discuss power sets then ask students to think of set S (in this situation) as being a power set? Or something else?

[Mario Carneiro]

I don't think set.powerset has been used at all in mathlib

[Mario Carneiro]

Once you have a separate notion of the type of subsets of a type, there are very few instances where the subcollection of subsets of a given subset of a type comes up

[Gihan Marasingha]

@Mario Carneiro. Trying to prove this non-surjectivity result for power sets, I can see why!

[Mario Carneiro]

Well in this case you aren't really using set.powerset as a set, so the translation to set S is natural

[Kevin Buzzard]

I say that set S is the type of subsets of S, and the reason it's not called subset S is because a term of type set S is a set of elements of S.

[Mario Carneiro]

There are uses of set.prod in mathlib (the cartesian product of sets), so conceivably a similar thing might come up for set.powerset

[Yury G. Kudryashov]

docs#filter.eventually_lift'_powerset

[Mario Carneiro]

oh that's right, filters will need this sometimes

[Mario Carneiro]

I went looking for uses of the notation

[Mario Carneiro]

Hm, should we use Iic instead of set.powerset?

[Mario Carneiro]

that would allow us to unify it with the collection of supersets {x | S \sub x}, which also comes up in filters

[Yury G. Kudryashov]

I'm not going to do this refactor!

[Mario Carneiro]

I can lump it in with that refactor I never finished to generalize filters to subsets of a poset

[Johan Commelin]

I fear that refactor might be really painful. Don't you think?
The fact that filters are filters on set X is really used all over the place now.
Not saying that it can't be done, but I think it might be one of the biggest refactors we've seen so far.

[Mario Carneiro]

You are not wrong

[Mario Carneiro]

It was one of those refactors where the size of the refactor grows exponentially with the number of touched theorems