cardinal.lift_sup

Stream: Is there code for X?

[Scott Morrison]

Is this following even true:

import set_theory.cardinal

universes u v w

lemma lift_sup {ι : Type v} (f : ι → cardinal.{max v w}) :
  cardinal.lift.{(max v w) (max u v w)} (cardinal.sup.{v w} f) =
    cardinal.sup.{v (max u w)} (λ i : ι, cardinal.lift.{(max v w) (max u v w)} (f i)) :=
sorry

If so, any advice on proving it?

[Reid Barton]

I think the math proof starts by observing that if $\alpha$ is a cardinal in universe $U$ and $\beta$ is a cardinal in a bigger universe $V$ such that $\beta \le \alpha$, then $\beta$ actually belongs to universe $U$ also. You can prove it in Lean by picking an injection $f : \beta \to \alpha$ and then using the image of $f$ to make the new $U$-sized cardinal which equals $\beta$ in $V$.

[Reid Barton]

Because the issue you might be worried about with the main statement is that the larger universe somehow has extra cardinals stuck in the middle that make the sup smaller than it would be in the small universe.

[Reid Barton]

Once you have that then you should be able to do some "they're $\le$ than the same cardinals" argument.

[Reid Barton]

I guess you can formulate the lemma like this: Every cardinal.{max u v} is either in the image of lift.{u v}, or bigger than everything in the image of lift.{u v}. (Because if there's some lift.{u v} a that it's not bigger than, apply the above argument to show it is in the image.)

[Reid Barton]

now for the main theorem, we need to prove that the lift of the sup is $\le \gamma$ iff each of the lifts is $\le \gamma$. Apply the lemma to $\gamma$. If it's "small" then we can write it as lift of something and apply docs#cardinal.lift_le. If it's "big" then it is bigger than all these lifts we care about.

[Reid Barton]

I want there to be some more orderly argument based on the fact that lift is an embedding of an initial segment of cardinal.{u} in cardinal.{v}, but it seems like the fact that sup changes the universe will get in the way

[Floris van Doorn]

@Reid Barton's lemma basically already exists as docs#cardinal.lift_down.

import set_theory.cardinal

universes u v w
namespace cardinal

protected lemma le_sup_iff {ι : Type v} {f : ι → cardinal.{max v w}} {c : cardinal} :
  (c ≤ sup f) ↔ (∀ b, (∀ i, f i ≤ b) → c ≤ b) :=
⟨λ h b hb, le_trans h (sup_le.mpr hb), λ h, h _ $ λ i, le_sup f i⟩

lemma lift_sup {ι : Type v} (f : ι → cardinal.{max v w}) :
  lift.{(max v w) (max u v w)} (sup.{v w} f) =
    sup.{v (max u w)} (λ i : ι, lift.{(max v w) (max u v w)} (f i)) :=
begin
  apply le_antisymm,
  { rw [cardinal.le_sup_iff], intros c hc, by_contra h,
    obtain ⟨d, rfl⟩ := cardinal.lift_down (not_le.mp h).le,
    simp only [lift_le, sup_le] at h hc,
    exact h hc },
  { simp only [cardinal.sup_le, lift_le, le_sup, implies_true_iff] }
end

end cardinal

[Scott Morrison]

Thanks, @Reid Barton and @Floris van Doorn! I'll PR this shortly.

[Scott Morrison]

#8675

[Scott Morrison]

(I also included the follow-up lemma lift_sup_le_lift_sup that I need in my application.)