lift — Mathlib

English

There exists a natural bijection between functions f: X → A and nonunital nonassociative R-algebra homomorphisms Free_R X →ₙₐ[R] A, given by F ↦ F ∘ of_R and f ↦ lift_R f.

Русский

Существует естественная биекция между функциями f: X → A и гомоморфизмами ненулевой неассоциативной R-алгебры Free_R X →ₙₐ[R] A, заданная F ↦ F ∘ of_R и f ↦ lift_R f.

LaTeX

$$$ X \to A \cong \mathrm{Hom}_{\mathrm{NAAlg}_R}(Free_R X, A). $$$

Lean4

/-- The functor `X ↦ FreeNonUnitalNonAssocAlgebra R X` from the category of types to the
category of non-unital, non-associative algebras over `R` is adjoint to the forgetful functor in the
other direction. -/
def lift : (X → A) ≃ (FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) :=
  FreeMagma.lift.trans (MonoidAlgebra.liftMagma R)

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