Mathlib.Logic.Small.Defs

Small structure

(α : Type v)

Full source

/-- A type is `Small.{w}` if there exists an equivalence to some `S : Type w`.
-/
@[mk_iff, pp_with_univ]
class Small (α : Type v) : Prop where
  /-- If a type is `Small.{w}`, then there exists an equivalence with some `S : Type w` -/
  equiv_small : ∃ S : Type w, Nonempty (α ≃ S)

$w$-small type

Informal description

A type $\alpha$ is called *$w$-small* if there exists an equivalence (bijection) between $\alpha$ and some type $S$ in the universe `Type w`.

Small.mk' theorem

{α : Type v} {S : Type w} (e : α ≃ S) : Small.{w} α

Full source

/-- Constructor for `Small α` from an explicit witness type and equivalence.
-/
theorem Small.mk' {α : Type v} {S : Type w} (e : α ≃ S) : Small.{w} α :=
  ⟨⟨S, ⟨e⟩⟩⟩

Construction of $w$-small type from equivalence

Informal description

Given a type $\alpha$ and a type $S$ in universe `Type w`, if there exists an equivalence (bijection) $e : \alpha \simeq S$, then $\alpha$ is $w$-small.

Shrink definition

(α : Type v) [Small.{w} α] : Type w

Full source

/-- An arbitrarily chosen model in `Type w` for a `w`-small type.
-/
@[pp_with_univ]
def Shrink (α : Type v) [Small.{w} α] : Type w :=
  Classical.choose (@Small.equiv_small α _)

Model of a small type in a smaller universe

Informal description

For a $w$-small type $\alpha$, the type `Shrink α` is an arbitrarily chosen model in the universe `Type w` that is equivalent to $\alpha$. This means there exists a bijection between $\alpha$ and `Shrink α`.

equivShrink definition

(α : Type v) [Small.{w} α] : α ≃ Shrink α

Full source

/-- The noncomputable equivalence between a `w`-small type and a model.
-/
noncomputable def equivShrink (α : Type v) [Small.{w} α] : α ≃ Shrink α :=
  Nonempty.some (Classical.choose_spec (@Small.equiv_small α _))

Equivalence between a small type and its model

Informal description

For a $w$-small type $\alpha$, the function `equivShrink α` provides a noncomputable equivalence (bijection) between $\alpha$ and its model `Shrink α` in the universe `Type w$.

Shrink.ext theorem

{α : Type v} [Small.{w} α] {x y : Shrink α} (w : (equivShrink _).symm x = (equivShrink _).symm y) : x = y

Full source

@[ext]
theorem Shrink.ext {α : Type v} [Small.{w} α] {x y : Shrink α}
    (w : (equivShrink _).symm x = (equivShrink _).symm y) : x = y := by
  simpa using w

Injectivity of the Shrink Model via Preimages

Informal description

For any $w$-small type $\alpha$ and elements $x, y$ in the model $\text{Shrink} \alpha$, if the preimages of $x$ and $y$ under the equivalence $\text{equivShrink} \alpha$ are equal, then $x = y$.

Shrink.rec definition

{α : Type*} [Small.{w} α] {F : Shrink α → Sort v} (h : ∀ X, F (equivShrink _ X)) : ∀ X, F X

Full source

@[induction_eliminator]
protected noncomputable def Shrink.rec {α : Type*} [Small.{w} α] {F : Shrink α → Sort v}
    (h : ∀ X, F (equivShrink _ X)) : ∀ X, F X :=
  fun X => ((equivShrink _).apply_symm_apply X) ▸ (h _)

Recursor for the model of a small type

Informal description

Given a $w$-small type $\alpha$ and a dependent type $F : \text{Shrink} \alpha \to \text{Sort} v$, if for every $X : \alpha$ we have a term of type $F(\text{equivShrink} \alpha X)$, then we can construct a term of type $F(X)$ for every $X : \text{Shrink} \alpha$.

small_self instance

(α : Type v) : Small.{v} α

Full source

instance small_self (α : Type v) : Small.{v} α :=
  Small.mk' <| Equiv.refl α

Every Type is Small in its Own Universe

Informal description

For any type $\alpha$ in universe `Type v`, $\alpha$ is $v$-small.

small_map theorem

{α : Type*} {β : Type*} [hβ : Small.{w} β] (e : α ≃ β) : Small.{w} α

Full source

theorem small_map {α : Type*} {β : Type*} [hβ : Small.{w} β] (e : α ≃ β) : Small.{w} α :=
  let ⟨_, ⟨f⟩⟩ := hβ.equiv_small
  Small.mk' (e.trans f)

Preservation of $w$-smallness under equivalence

Informal description

Let $\alpha$ and $\beta$ be types, and suppose $\beta$ is $w$-small. If there exists an equivalence $e : \alpha \simeq \beta$, then $\alpha$ is also $w$-small.

small_lift theorem

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

Full source

theorem small_lift (α : Type u) [hα : Small.{v} α] : Small.{max v w} α :=
  let ⟨⟨_, ⟨f⟩⟩⟩ := hα
  Small.mk' <| f.trans (Equiv.ulift.{w}).symm

Lifting of Smallness to Larger Universe

Informal description

Let $\alpha$ be a type in universe `Type u`. If $\alpha$ is $v$-small, then $\alpha$ is also $(max\, v\, w)$-small.

small_max theorem

(α : Type v) : Small.{max w v} α

Full source

/-- Due to https://github.com/leanprover/lean4/issues/2297, this is useless as an instance.

See however `Logic.UnivLE`, whose API is able to indirectly provide this instance. -/
lemma small_max (α : Type v) : Small.{max w v} α :=
  small_lift.{v, w} α

Smallness in Maximum Universe

Informal description

For any type $\alpha$ in universe `Type v`, $\alpha$ is $(max\, w\, v)$-small.

small_zero instance

(α : Type) : Small.{w} α

Full source

instance small_zero (α : Type) : Small.{w} α := small_max α

Universally Small Types in Any Universe

Informal description

For any type $\alpha$ in any universe, $\alpha$ is $w$-small.

small_succ instance

(α : Type v) : Small.{v + 1} α

Full source

instance (priority := 100) small_succ (α : Type v) : Small.{v+1} α :=
  small_lift.{v, v+1} α

Smallness in Successor Universe

Informal description

For any type $\alpha$ in universe `Type v`, $\alpha$ is $(v + 1)$-small.

small_ulift instance

(α : Type u) [Small.{v} α] : Small.{v} (ULift.{w} α)

Full source

instance small_ulift (α : Type u) [Small.{v} α] : Small.{v} (ULift.{w} α) :=
  small_map Equiv.ulift

$w$-smallness of Lifted Types

Informal description

For any type $\alpha$ in universe `Type u`, if $\alpha$ is $v$-small, then the lifted type `ULift.{w} α` is also $v$-small.

small_type theorem

: Small.{max (u + 1) v} (Type u)

Full source

theorem small_type : Small.{max (u + 1) v} (Type u) :=
  small_max.{max (u + 1) v} _

Smallness of Type Universes: $\text{Type}\, u$ is $(max (u + 1) v)$-small

Informal description

For any universe level $u$, the type universe `Type u` is $(max (u + 1) v)$-small for any universe level $v$.

small_congr theorem

{α : Type*} {β : Type*} (e : α ≃ β) : Small.{w} α ↔ Small.{w} β

Full source

theorem small_congr {α : Type*} {β : Type*} (e : α ≃ β) : SmallSmall.{w} α ↔ Small.{w} β :=
  ⟨fun h => @small_map _ _ h e.symm, fun h => @small_map _ _ h e⟩

Equivalence Preserves $w$-smallness

Informal description

For any types $\alpha$ and $\beta$, given an equivalence $e : \alpha \simeq \beta$, the type $\alpha$ is $w$-small if and only if $\beta$ is $w$-small.

small_sigma instance

{α} (β : α → Type*) [Small.{w} α] [∀ a, Small.{w} (β a)] : Small.{w} (Σ a, β a)

Full source

instance small_sigma {α} (β : α → Type*) [Small.{w} α] [∀ a, Small.{w} (β a)] :
    Small.{w} (Σa, β a) :=
  ⟨⟨Σa' : Shrink α, Shrink (β ((equivShrink α).symm a')),
      ⟨Equiv.sigmaCongr (equivShrink α) fun a => by simpa using equivShrink (β a)⟩⟩⟩

$w$-smallness of Dependent Sum Types

Informal description

For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}^*$, if $\alpha$ is $w$-small and each $\beta(a)$ is $w$-small for all $a \in \alpha$, then the dependent sum type $\Sigma a, \beta(a)$ is also $w$-small.

not_small_type theorem

: ¬Small.{u} (Type max u v)

Full source

theorem not_small_type : ¬Small.{u} (Type max u v)
  | ⟨⟨S, ⟨e⟩⟩⟩ =>
    @Function.cantor_injective (Σα, e.symm α) (fun a => ⟨_, cast (e.3 _).symm a⟩) fun a b e => by
      dsimp at e
      injection e with h₁ h₂
      simpa using h₂

Non-$u$-smallness of `Type (max u v)`

Informal description

The type `Type (max u v)` is not $u$-small, i.e., there does not exist an equivalence between `Type (max u v)` and any type in the universe `Type u`.