cardinals across universes

Stream: new members

[Pedro Sánchez Terraf]

I stumbled upon the following funny situation: a type mismatch between terms of apparently the same type.
I tried to see if the type annotations of each side of the equality showed more info by using set_option pp.all true, but both said cardinal.{u} anyway. Below is the MWE with an excerpt of the error message.

import set_theory.cardinal.ordinal

universe u

open set

namespace cardinal

open_locale cardinal

set_option pp.all true
variables (i k : ordinal.{u})

#check lift.{u+1} (# (↥(Iio.{u+1} i))) -- `cardinal.{u+1}`
#check lift.{u+1} (# (quotient.out.{u+2} i).α) -- `cardinal.{u+1}`
#check lift.{u+1} (# (↥(Iio.{u+1} i))) = lift.{u+1} (# (quotient.out.{u+2} i).α) -- type mismatch at application

/-
term
  cardinal.lift.{u+1 u} (cardinal.mk.{u} (@quotient.out.{u+2} Well_order.{u} ordinal.is_equivalent.{u} i).α)
has type
  cardinal.{u+1}
but is expected to have type
  cardinal.{u+1}
-/

end cardinal

The context of this is that I'm trying to prove an version of cardinal.mk_Union_le (btw, is there an automatic way to generate this kind of links?) for ordinal-indexed unions:

lemma mk_Union_le_of_le {β : Type u} (κ : cardinal) (i : ordinal) (hi : i ≤ κ.ord) (hκ : ℵ₀ ≤ κ)
(A : ordinal.{u} → set β) (hA : ∀ j < i, #↥(A j) ≤ κ) :
  #(↥⋃ j < i, A j) ≤ κ

[Kevin Buzzard]

I don't know what's going on, but you can fix the error by explicitly coercing:

#check lift.{u+1} (# (↥(Iio.{u+1} i))) = (lift.{u+1} (# (quotient.out.{u+2} i).α) : cardinal.{u+1})

[Pedro Sánchez Terraf]

Thank you very much. The error message, nevertheless, is misleading. Is there any way to get more information out of it?

EDIT: Explicitly coercing the lhs gives the same error (both in isolation or in the equation, disregarding if the rhs is annotated or not).

#check (lift.{u+1} (# (↥(Iio.{u+1} i))) : cardinal.{u+1})
/-
invalid type ascription, term has type
  cardinal.{u+1}
but is expected to have type
  cardinal.{u+1}
-/

[Reid Barton]

Pedro Sánchez Terraf said:

cardinal.mk_Union_le (btw, is there an automatic way to generate this kind of links?)

docs#cardinal.mk_Union_le

[Pedro Sánchez Terraf]

Reid Barton said:

Pedro Sánchez Terraf said:

cardinal.mk_Union_le (btw, is there an automatic way to generate this kind of links?)

docs#cardinal.mk_Union_le

The format is docs#theory.theorem, isn't it? I was also misled because some completion is offered when you start typing #docs.

[Johan Commelin]

• Typing #foo will complete to Zulip stream names that start with "foo".
• The syntax is docs#<declaration name>. And the declaration name could contain any amount of .s.

[Junyan Xu]

Both of the followings work:

#check let a := lift.{u+1} (# (↥(Iio.{u+1} i))) in a = lift.{u+1} (# (quotient.out.{u+2} i).α)
#check let b := lift.{u+1} (# (quotient.out.{u+2} i).α) in lift.{u+1} (# (↥(Iio.{u+1} i))) = b

looks like a bug to me (maybe in checking universe equality?)