Mathlib.Logic.UnivLE

Module docstring

{"# UnivLE

A proposition expressing a universe inequality. UnivLE.{u, v} expresses that u ≤ v, in the form ∀ α : Type u, Small.{v} α.

This API indirectly provides an instance for Small.{u, max u v}, which could not be declared directly due to https://github.com/leanprover/lean4/issues/2297.

See the doc-string for the comparison with an alternative stronger definition. "}

UnivLE structure

Full source

/--
A class expressing a universe inequality. `UnivLE.{u, v}` expresses that `u ≤ v`.

There used to be a stronger definition `∀ α : Type max u v, Small.{v} α` that immediately implies
`Small.{v} ((α : Type u) → (β : Type v))` which is essential for proving that `Type v` has
`Type u`-indexed limits when `u ≤ v`. However the current weaker condition
`∀ α : Type u, Small.{v} α` also implies the same, so we switched to use it for
its simplicity and transitivity.

The strong definition easily implies the weaker definition (see below),
but we can not prove the reverse implication.
This is because in Lean's type theory, while `max u v` is at least at big as `u` and `v`,
it could be bigger than both!
See also `Mathlib.CategoryTheory.UnivLE` for the statement that the stronger definition is
equivalent to `EssSurj (uliftFunctor : Type v ⥤ Type max u v)`.
-/
@[pp_with_univ, mk_iff]
class UnivLE : Prop where
  small (α : Type u) : Small.{v} α

Universe Level Inequality

Informal description

The structure `UnivLE.{u, v}` expresses a universe inequality stating that universe level `u` is less than or equal to universe level `v`. This is formulated as the property that for every type `α : Type u`, `α` is `Small.{v}` (meaning `α` can be represented in universe `v`). This is a weaker condition than the alternative definition `∀ α : Type max u v, Small.{v} α`, but suffices for proving that `Type v` has `Type u`-indexed limits when `u ≤ v`. The stronger definition would imply that the universe lifting functor `uliftFunctor : Type v → Type max u v` is essentially surjective, but this cannot be proven from the weaker condition.

univLE_max theorem

: UnivLE.{u, max u v}

Full source

theorem univLE_max : UnivLEUnivLE.{u, max u v} where small α := small_max.{v} α

Universe Level Inequality: $u \leq \max(u, v)$

Informal description

For any universe levels $u$ and $v$, the universe level $u$ is less than or equal to the maximum of $u$ and $v$, i.e., $u \leq \max(u, v)$ holds in the sense that every type in universe $u$ is small in universe $\max(u, v)$.

Small.trans_univLE theorem

(α : Type w) [hα : Small.{u} α] [h : UnivLE.{u, v}] : Small.{v} α

Full source

theorem Small.trans_univLE (α : Type w) [hα : Small.{u} α] [h : UnivLEUnivLE.{u, v}] :
    Small.{v} α :=
  let ⟨β, ⟨f⟩⟩ := hα.equiv_small
  let ⟨_, ⟨g⟩⟩ := (h.small β).equiv_small
  ⟨_, ⟨f.trans g⟩⟩

Transitivity of Smallness under Universe Level Inequality

Informal description

Let $\alpha$ be a type in universe level $w$. If $\alpha$ is $u$-small (i.e., there exists an equivalence between $\alpha$ and some type in universe level $u$) and the universe level $u$ is less than or equal to $v$ (i.e., $\text{UnivLE}.\{u, v\}$ holds), then $\alpha$ is also $v$-small.

UnivLE.trans theorem

[UnivLE.{u, v}] [UnivLE.{v, w}] : UnivLE.{u, w}

Full source

theorem UnivLE.trans [UnivLEUnivLE.{u, v}] [UnivLEUnivLE.{v, w}] : UnivLEUnivLE.{u, w} where
  small α := Small.trans_univLE α

Transitivity of Universe Level Inequality

Informal description

If universe level $u$ is less than or equal to $v$ (i.e., $\text{UnivLE}.\{u, v\}$ holds) and universe level $v$ is less than or equal to $w$ (i.e., $\text{UnivLE}.\{v, w\}$ holds), then universe level $u$ is less than or equal to $w$ (i.e., $\text{UnivLE}.\{u, w\}$ holds).

UnivLE.self instance

: UnivLE.{u, u}

Full source

instance UnivLE.self : UnivLEUnivLE.{u, u} := ⟨inferInstance⟩

Reflexivity of Universe Level Inequality

Informal description

For any universe level $u$, the universe inequality $\text{UnivLE}.\{u, u\}$ holds, meaning every type in universe $\text{Type } u$ is $u$-small.

UnivLE.zero instance

: UnivLE.{0, u}

Full source

instance UnivLE.zero : UnivLEUnivLE.{0, u} := ⟨inferInstance⟩

Smallness of Zeroth Universe Types in Any Universe

Informal description

For any universe level $u$, every type in the zeroth universe (the universe of small types) is $u$-small. In other words, $\text{UnivLE}.\{0, u\}$ holds.

UnivLE.succ theorem

[UnivLE.{u, v}] : UnivLE.{u, v + 1}

Full source

/-- This is redundant as an instance given the below. -/
theorem UnivLE.succ [UnivLEUnivLE.{u, v}] : UnivLEUnivLE.{u, v + 1} := @UnivLE.trans _ ⟨inferInstance⟩

Universe Level Inequality Preserved Under Successor

Informal description

If universe level $u$ is less than or equal to $v$ (i.e., every type in $\text{Type } u$ is $v$-small), then universe level $u$ is also less than or equal to $v + 1$ (i.e., every type in $\text{Type } u$ is $(v + 1)$-small).

univLE_of_max instance

[UnivLE.{max u v, v}] : UnivLE.{u, v}

Full source

instance univLE_of_max [UnivLEUnivLE.{max u v, v}] : UnivLEUnivLE.{u, v} := @UnivLE.trans univLE_max ‹_›

Universe Level Inequality from Maximum Condition

Informal description

If the maximum of universe levels $u$ and $v$ is less than or equal to $v$ (i.e., every type in $\text{Type } \max(u, v)$ is $v$-small), then universe level $u$ is also less than or equal to $v$ (i.e., every type in $\text{Type } u$ is $v$-small).