Transfinite recursion

Stream: new members

[Lucas Polymeris]

Hi. I'm again having troubles with my set-theoretic view. I've defined a function f : ordinal → set C. I would like
to argue that there must be α,β ∈ ordinal such that f(α) = f(β). Mathematically I'd do this by actually defining f with
domain ν where ν is any ordinal that does not inject to ℘(C).
Any Idea how this should be done here? I've skimmed through set_theory.ordinal, set_theory.cardinal (and others) and have not had any success.

[Eric Wieser]

Can you give a #mwe of the statement you want to prove?

[Lucas Polymeris]

I guess something like this should be close enough:

import data.set set_theory.ordinal
open set ordinal

universe u

section
parameters {C : Type u} (g : set C → set C)

def f : ordinal → set C
  | ξ := ⋃ η < ξ, g (f η)
  using_well_founded { dec_tac := `[assumption] }

lemma some_lemma: ∃ {α β : ordinal}, f α = f β := by sorry

end

But keep in mind that so far, defining f from ordinal is the only thing that I've managed to accomplish, If the way to go is to define f some other way, that would be ok too. I'v also tried to define it on the well order of something like cardinal.ord (cardinal.succ (cardinal.mk (set C)))), which should be an ordinal that does not inject to set C, but I did not manage to pull it of.

[Eric Wieser]

I assume you're missing an α ≠ β component somewhere, else that statement is trivially true

[Reid Barton]

You probably want to write explicit universe variables like def f : ordinal.{u} → set C, and maybe use set_option pp.universes true to check that your universe levels are what you expect.

[Eric Wieser]

I'm very surprised this doesn't work:

lemma some_lemma: ∃ {α β : ordinal}, f α = f β := ⟨0, 0, begin
  refl,
end⟩

[Eric Wieser]

Ah, @Reid Barton's comment reveals the issue with that attempt; your statement is actually ∃ {α : ordinal.{u}} {b : ordinal.{v}}

[Reid Barton]

This is ugly (I wrote it in the online Lean editor), but it works:

import data.set set_theory.ordinal
open set ordinal

universe u

section

lemma {v} up_injective {X : Type u} :
  function.injective (ulift.up.{v} : X → ulift X) :=
begin
  rintros x1 x2 h, cc,
end

lemma some_lemma (X : Type u) (f : ordinal.{u} → X) :
  ¬ function.injective f := begin
  let g : ordinal.{u} → ulift.{u+1} X := λ o, ulift.up (f o),
  suffices : ¬ function.injective g,
  { intro hf, exact this (up_injective.comp hf) },
  intro hg,
  replace hg := cardinal.mk_le_of_injective hg,
  rw ← cardinal.lift_mk at hg,
  replace hg := lt_of_le_of_lt hg (cardinal.lift_lt_univ _),
  contrapose! hg,
  rw cardinal.univ_id
end

end

[Reid Barton]

Basically cardinal.lift_lt_univ is the key fact, and the rest is shuffling which I probably didn't do very efficiently.

[Reid Barton]

up_injective already exists as equiv.ulift.symm.injective

[Lucas Polymeris]

Eric Wieser said:

I assume you're missing an α ≠ β component somewhere, else that statement is trivially true

Yes of course, my bad.

[Lucas Polymeris]

Reid Barton said:

Basically cardinal.lift_lt_univ is the key fact, and the rest is shuffling which I probably didn't do very efficiently.

I'll have a look at cardinal.lift_lt_univ. Thanks.

[Lucas Polymeris]

It worked nicely thanks. Shouldn't something like this or similar be in mathlib? It is quite a common thing to do, I believe.

[Reid Barton]

I actually meant to ask what you were using this for--a lot of the time you can use an inductive predicate (or impredicative-style definition) for a subset that you might define by transfinite induction in a set-theoretic setting.

[Reid Barton]

By impredicative-style definition I mean something like "the intersection of all sets s such that s contains g s"

[Reid Barton]

I guess I should say that I'm more familiar with transfinite constructions in category theory where you're building a sequence of objects so you can't conclude that the sequence stabilizes for size reasons, and have to use some accessibility of g instead (and so you know in advance when to stop).

[Reid Barton]

But anyways this statement about ¬ function.injective f does seem useful for mathlib, and maybe some lemmas that would simplify the proof are missing too.

[Lucas Polymeris]

@Reid Barton I'm doing something similar to https://core.ac.uk/download/pdf/4886291.pdf (lemma 1). I'm not familiar with category theory, but what you describe sounds similar to what I'm doing.

[M.G.]

Lucas Polymeris said:

Reid Barton I'm doing something similar to https://core.ac.uk/download/pdf/4886291.pdf (lemma 1). I'm not familiar with category theory, but what you describe sounds similar to what I'm doing.

Awesome, I just started Christopher Allen, Julie Moronuki - Haskell Programming from first principles (2016), I can share my notes if you are interested.