uSwitchEquiv — Mathlib

English

For any finite type X, there is a canonical equivalence between its switched-universe object and X.

Русский

Для любого X существует каноническое эквивалентное отображение между объектом с переключённой вселенной и самим X.

LaTeX

$$$uSwitchEquiv(X) : (uSwitch.obj X) \\simeq X$$$

Lean4

/-- Switching the universe of an object `X : FintypeCat.{u}` does not change `X` up to equivalence
of types. This is natural in the sense that it commutes with `uSwitch.map f` for
any `f : X ⟶ Y` in `FintypeCat.{u}`. -/
noncomputable def uSwitchEquiv (X : FintypeCat.{u}) : uSwitch.{u, v}.obj X ≃ X :=
  Equiv.ulift.trans (Fintype.equivFin X).symm

Похожие утверждения