map — Mathlib

English

For any f: α → β, there is a ring hom map: FreeCommRing α → FreeCommRing β sending generators to generators via f.

Русский

Для любого отображения f: α → β существует кольцевой гомоморфизм FreeCommRing α → FreeCommRing β, который переводит генераторы по f.

LaTeX

$$$ \\text{map } f : \\mathrm{FreeCommRing}(\\alpha) \\to\\!+* \\mathrm{FreeCommRing}(\\beta) $$$

Lean4

/-- A map `f : α → β` produces a ring homomorphism `FreeCommRing α →+* FreeCommRing β`. -/
def map : FreeCommRing α →+* FreeCommRing β :=
  lift <| of ∘ f

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