fullyFaithfulULift — Mathlib

English

Universe lifting is fully faithful: ULift has a FullyFaithful structure.

Русский

Поднятие вселенных полно и полнонаглядно сохраняется: ULift является полно надёжным функтором.

LaTeX

$$$\\mathrm{FullyFaithful}(\\mathrm{ULift})$$$

Lean4

/-- Universe lifting is fully faithful. -/
def fullyFaithfulULift : (ulift R).FullyFaithful where
  preimage f := ofHom <| ULift.moduleEquiv.toLinearMap ∘ₗ f.hom ∘ₗ ULift.moduleEquiv.symm.toLinearMap

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