lift — Mathlib

English

There is a canonical equivalence between functions α → R and ring homomorphisms FreeRing α →+* R; FreeRing is the free R-algebra on α.

Русский

Существует каноническое эквивалентность между отображениями α → R и кольцевыми гомоморфизмами FreeRing α →+* R; FreeRing является свободой кольца над R на α.

LaTeX

$$$$ (\alpha \to R) \cong (\mathrm{FreeRing}(\alpha) \to^{+}_* R). $$$$

Lean4

/-- The ring homomorphism `FreeRing α →+* R` induced from a map `α → R`. -/
def lift : (α → R) ≃ (FreeRing α →+* R) :=
  FreeMonoid.lift.trans FreeAbelianGroup.liftMonoid

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