Zulip Chat Archive

Stream: general

Topic: Infinity Hotel

Reid Barton (Sep 19 2019 at 15:46):

This Proof Ground problem is actually almost exactly a lemma I want. Would somebody (@Floris van Doorn?) like to PR a solution to mathlib?
Maybe as a mathlib lemma, it is more natural to use equiv in place of bijective, and replace the target nat by denumerable

Mario Carneiro (Sep 19 2019 at 15:58):

I discussed this with floris after the competition. I think it generalizes to embedding B < A when A is an infinite cardinal

Kevin Buzzard (Sep 19 2019 at 16:17):

Assuming AC, a+b=max(a,b) so A-B bijects with A-f(B)

Floris van Doorn (Sep 19 2019 at 18:19):

Yes, I'm going to PR this to mathlib. The current statement I am proving is

theorem extend_function_of_lt {α β : Type*} {s : set α} (f : s ↪ β) (hs : #s < #α)
  (h : nonempty (α ≃ β)) : ∃ (g : α ≃ β), ∀ x : s, g x = f x

Floris van Doorn (Sep 19 2019 at 18:20):

Here # means cardinal.mk

Floris van Doorn (Sep 19 2019 at 18:26):

I have already proved this in the case where #α is infinite.

Now that I think of this, when α is infinite, I should probably replace the assumption #s < #α with the weaker condition #(-s : set α) = #α (I already proved the lemma that the former implies the latter).
EDIT: Oh wait, then it's false.

Mario Carneiro (Sep 20 2019 at 04:20):

@Kevin Buzzard Could you elaborate on that proof? a+b=a does not imply a-b=a for cardinals

Kevin Buzzard (Sep 20 2019 at 07:21):

I was imagining the generalisation being this: if B<A is a subset, and |B|<|A|, then any injection f:B -> A can be extended to a bijection A -> A. The proof is: write C=A\B and D=A\f(B) and observe that |C|=|A|=|D|. Did I slip up?

Mario Carneiro (Sep 20 2019 at 07:39):

Those facts are all true but I'm not sure how you are arguing them

Mario Carneiro (Sep 20 2019 at 07:40):

actually you forgot to assume A is infinite, else |C|=|A| fails

Chris Hughes (Sep 20 2019 at 07:41):

I proved something similar as part of algebraic closure.

import set_theory.schroeder_bernstein

open set function
universes u v w
noncomputable theory
local attribute [instance] classical.dec

lemma thing_aux {X : Type u} {Y : Type v} {Z : Type w} (fxy : X ↪ Y) (fxz : X ↪ Z)
  (hYZ : (Z ↪ Y) → false) : ↥-range fxy.1 ↪ ↥-range fxz.1 :=
classical.choice $ or.resolve_left embedding.total $
  λ ⟨f⟩, hYZ $
    calc Z ↪ range fxz ⊕ ↥-range fxz :
      (equiv.set.sum_compl _).symm.to_embedding
    ... ↪ range fxy ⊕ ↥-range fxy :
      embedding.sum_congr
        (((equiv.set.range _ fxz.2).symm.to_embedding).trans
          (equiv.set.range _ fxy.2).to_embedding)
        f
    ... ↪ Y : (equiv.set.sum_compl _).to_embedding

def thing {X : Type u} {Y : Type v} {Z : Type w} (fxy : X ↪ Y) (fxz : X ↪ Z)
  (hYZ : (Z ↪ Y) → false) : Y ↪ Z :=
calc Y ↪ range fxy ⊕ ↥-range fxy : (equiv.set.sum_compl _).symm.to_embedding
... ↪ range fxz ⊕ ↥-range fxz : embedding.sum_congr
  ((equiv.set.range _ fxy.2).symm.to_embedding.trans
    (equiv.set.range _ fxz.2).to_embedding)
  (thing_aux fxy fxz hYZ)
... ↪ Z : (equiv.set.sum_compl _).to_embedding

lemma thing_commutes {X : Type u} {Y : Type v} {Z : Type w}  (fxy : X ↪ Y) (fxz : X ↪ Z)
  (hYZ : (Z ↪ Y) → false) (x : X) : thing fxy fxz hYZ (fxy x) = fxz x :=
have (⟨fxy x, mem_range_self _⟩ : range fxy) = equiv.set.range _ fxy.2 x, from rfl,
begin
  dsimp only [thing, embedding.trans_apply, equiv.trans_apply, function.comp,
    equiv.to_embedding_coe_fn],
  simp only [equiv.set.sum_compl_symm_apply_of_mem (mem_range_self _),
    embedding.sum_congr_apply_inl, equiv.set.sum_compl_apply_inl,
    embedding.trans_apply, equiv.to_embedding_coe_fn, this, equiv.symm_apply_apply],
  refl
end

Chris Hughes (Sep 20 2019 at 07:43):

Somehow the assumption (Z ↪ Y) → false should be turned into (Z ↪ X) → false

Mario Carneiro (Sep 20 2019 at 07:43):

isn't that just transitivity?

Mario Carneiro (Sep 20 2019 at 07:46):

@Kevin Buzzard I think your proof sketch is basically what floris did in the competition

Mario Carneiro (Sep 20 2019 at 07:47):

it would be nice to reduce it to a one liner of mathlib lemmas though

Mario Carneiro (Sep 20 2019 at 07:50):

Unfortunately I don't see how to apply chris's lemma directly here

Mario Carneiro (Sep 20 2019 at 07:51):

it only seems to construct an injection from Y to Z where |Y|<|Z|, and the only obvious candidates are Y=B and Z=A, or Y=f(B) and Z=A, and neither is particularly helpful

Mario Carneiro (Sep 20 2019 at 07:54):

In this situation, we want Y=Z=A, but then (Z ↪ Y) → false fails

Chris Hughes (Sep 20 2019 at 07:56):

But in the infinite case can we weaken the assumption to (Z ↪ X) → false?

Kevin Buzzard (Sep 20 2019 at 07:57):

@Mario Carneiro I don't understand why you're calling it a sketch ;-)

Mario Carneiro (Sep 20 2019 at 07:57):

you have to reference actual theorems, and also prove the side conditions

Mario Carneiro (Sep 20 2019 at 07:58):

ideally the formal proof should actually be that short, but the side conditions are messy here

Kevin Buzzard (Sep 20 2019 at 07:58):

The argument would convince any mathematician. That's the level where we operate. What we really need is an interface where I can just say what I said to you and then let tactics do the rest.

Kevin Buzzard (Sep 20 2019 at 07:59):

we can try cases, refl on the side conditions or whatever. It's all noise.

Mario Carneiro (Sep 20 2019 at 07:59):

you also didn't prove what you claimed to... there are lots of issues with treating that literally as a proof

Kevin Buzzard (Sep 20 2019 at 08:00):

Can you give me specific examples of issues? I'd be happy to talk about this but I have to run

Kevin Buzzard (Sep 20 2019 at 08:00):

I think my proof is "math-complete"

Mario Carneiro (Sep 20 2019 at 08:00):

it's absolutely a sketch, but it's enough hints for a competent mathematician to fill in the rest of the proof

Mario Carneiro (Sep 20 2019 at 08:00):

but you should never confuse "enough to communicate the main ideas" with "proof"

Johan Commelin (Sep 20 2019 at 08:01):

Isn't that the definition of proof?

Mario Carneiro (Sep 20 2019 at 08:02):

for one thing, communication depends on the target audience; computers should be treated as a particularly dumb student

Mario Carneiro (Sep 20 2019 at 08:04):

it is not really possible to give an actual definition of "proof" if you take that position seriously... in the limit, anything that is logically derivable can be considered "proof by trivial"

Mario Carneiro (Sep 20 2019 at 08:06):

This is trending philosophical, but one property I want the word "proof" to have is that it's objective or at least societally defined, whereas "communication" is context dependent

Mario Carneiro (Sep 20 2019 at 08:09):

Really, I prefer to just sidestep the whole matter and only talk about formal proof, which has a proper definition, but it makes it difficult for me to interpret Kevin when he wants a raised eyebrow to constitute a valid proof

Patrick Massot (Sep 20 2019 at 08:21):

It depends whose eyebrow it is.

Mario Carneiro (Sep 20 2019 at 08:53):

Here's the closest I got to Kevin's sketch, modulo the cardinality fact:

import set_theory.cardinal

local prefix `#` := cardinal.mk
theorem mk_eq_mk {α β} (h : α ≃ β) : #α = #β := quotient.sound ⟨h⟩
theorem foo {α} {S : set α} (h : #S < #α) : #(-S : set α) = #α := sorry

example {X Y Z} (f : X ↪ Y) (g : X ↪ Z) (h₁ : #X < #Y) (h₂ : #Y = #Z) :
  ∃ e : Y ≃ Z, ∀ x, e (f x) = g x :=
begin
  have e1 : #(-set.range f : set _) = #Y := foo (by rwa [← mk_eq_mk (equiv.set.range f f.2)]),
  have e2 : #(-set.range g : set _) = #Z := foo (by rwa [← h₂, ← mk_eq_mk (equiv.set.range g g.2)]),
  rw [h₂, ← e2] at e1,
  cases quotient.exact e1 with e1,
  classical,
  refine ⟨(equiv.set.sum_compl _).symm.trans ((equiv.sum_congr _ e1).trans (equiv.set.sum_compl _)), λ x, _⟩,
  { exact (equiv.set.range f f.2).symm.trans (equiv.set.range g g.2) },
  { simp [equiv.set.sum_compl_symm_apply_of_mem, set.mem_range_self],
    rw (equiv.symm_apply_eq _).2, simp }
end

Kevin Buzzard (Sep 20 2019 at 09:18):

the cardinal fact is proved like this: If b<a then a=b+(a-b)=max(b,a-b), hence a-b=a.

Kevin Buzzard (Sep 20 2019 at 09:19):

Maybe some automatic theorem prover can find that fact about cardinals given what is in mathlib?

Kevin Buzzard (Sep 20 2019 at 09:22):

I'm taking a look at your proof. It's annoying that hovering over equiv.set.sum_compl doesn't show me its type -- I think this is because we're in tactic mode.

Mario Carneiro (Sep 20 2019 at 09:30):

Note that the cardinal fact as I've stated it is false, so if you think you have proved it you should not trust your proof

Mario Carneiro (Sep 20 2019 at 09:31):

it would be pretty difficult to get nitpick or whatever counterexample generator to find why the statement is false too

Mario Carneiro (Sep 20 2019 at 09:32):

actually scratch that - the problem is with finite sets so they can probably handle it

Mario Carneiro (Sep 20 2019 at 09:34):

In chris's proof he uses calc blocks instead to build the equivs, which looks a bit nicer

Kevin Buzzard (Sep 20 2019 at 09:34):

I thought we were talking about the infinite case now. All this a+b=max(a,b) is only true in the infinite case, I've been assuming infinite.

Your proof is extraordinary.

⊢ ⇑(equiv.trans (equiv.symm (equiv.set.sum_compl (set.range ⇑f)))
         (equiv.trans (equiv.sum_congr (equiv.trans (equiv.symm (equiv.set.range ⇑f _)) (equiv.set.range ⇑g _)) e1)
            (equiv.set.sum_compl (set.range ⇑g))))
      (⇑f x) =
    ⇑g x

We prove this by saying "...and the diagram obviously commutes". What is going on? This is trivial stuff.

Mario Carneiro (Sep 20 2019 at 09:35):

there are side conditions

Kevin Buzzard (Sep 20 2019 at 09:35):

I can prove this whole thing by drawing one picture.

Mario Carneiro (Sep 20 2019 at 09:35):

no, you can state the problem by drawing a picture

Kevin Buzzard (Sep 20 2019 at 09:36):

There aren't any side conditions. Assuming foo, we can prove the existence theorem. This is a really great example of a proof which can be done by a simple picture.

Mario Carneiro (Sep 20 2019 at 09:36):

The only thing I wrote in the proof are side conditions

Mario Carneiro (Sep 20 2019 at 09:36):

everything else is indeed being handled by simp

Kevin Buzzard (Sep 20 2019 at 09:36):

wow

Mario Carneiro (Sep 20 2019 at 09:37):

The proof sketch you gave me essentially covers the first two lines of the proof

Mario Carneiro (Sep 20 2019 at 09:37):

you never said what the bijection is or how to build it

Mario Carneiro (Sep 20 2019 at 09:38):

that's all "type tetris"

Mario Carneiro (Sep 20 2019 at 09:38):

with side conditions in the middle of it all

Mario Carneiro (Sep 20 2019 at 09:40):

I think side conditions are the bane of any theorem prover, because there is no good way to write them, which makes it easy to ignore them for expositional purposes in math

Kevin Buzzard (Sep 20 2019 at 09:42):

IMG_20190920_104043021.jpg

Kevin Buzzard (Sep 20 2019 at 09:44):

Where is equiv.set.sum_compl_symm_apply_of_mem in my picture? What is going on?

Mario Carneiro (Sep 20 2019 at 09:44):

Where's the bijection? I'm not even sure where f is in the picture

Kevin Buzzard (Sep 20 2019 at 09:44):

Two down arrows are f and g.

Kevin Buzzard (Sep 20 2019 at 09:45):

The bijection is because I identified the two sets Y and Z, the top halves are the same, and the bottom halves biject by a trivial lemma which I proved elsewhere on the board.

Mario Carneiro (Sep 20 2019 at 09:45):

equiv.set.sum_compl_symm_apply_of_mem says that if you are on the top half of the picture then you can go from y to the top half of y

Kevin Buzzard (Sep 20 2019 at 09:45):

I am working in the category of sets equipped with a map from X, so somehow the commutativity of the diagrams just all gets swallowed up by the machine.