ulift — Mathlib

English

Universe lifting gives a functor FGModuleCat(R) → FGModuleCat(max v w) R.

Русский

Поднятие вселенных даёт функтор FGModuleCat(R) → FGModuleCat(max v w) R.

LaTeX

$$$\\mathrm{ulift}: \\mathrm{FGModuleCat}(R) \\to \\mathrm{FGModuleCat}(max\\;v,w)(R)$$$

Lean4

/-- Universe lifting as a functor on `FGModuleCat`. -/
def ulift : FGModuleCat.{v} R ⥤ FGModuleCat.{max v w} R
    where
  obj M := .of R <| ULift M
  map f := ofHom <| ULift.moduleEquiv.symm.toLinearMap ∘ₗ f.hom ∘ₗ ULift.moduleEquiv.toLinearMap

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