uliftFunctor — Mathlib

English

The universe-lift functor for finitely generated algebras is fully faithful.

Русский

Функтор подъема вселенной для конечно порожденных алгебр полно и верен на отображениях.

LaTeX

$$$\text{FullyFaithful}(\mathrm{FGAlgCat.uliftFunctor}(R))$$$

Lean4

/-- Universe lift functor for finitely generated algebras. -/
def uliftFunctor : FGAlgCat.{v} R ⥤ FGAlgCat.{max v w} R
    where
  obj A := ⟨.of R <| ULift A.1, .equiv inferInstance ULift.algEquiv.symm⟩
  map {A B} f := CommAlgCat.ofHom <| ULift.algEquiv.symm.toAlgHom.comp <| f.hom.comp ULift.algEquiv.toAlgHom

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