singleOneRingHom — Mathlib

English

The map of a monoid into its skew monoid algebra is given by a ↦ single a 1; this is a monoid homomorphism with multiplication reflecting the skew product.

Русский

Вложение моноида в skew-монойдную алгебру задаётся как a ↦ single a 1 и является гомоморфизмом по умножению, отражающим skew-правило произведения.

LaTeX

$$$\mathrm{of} : G \to \mathrm{SkewMonoidAlgebra}(k,G),\quad \mathrm{of}(a) = \mathrm{single}(a,1)$$$

Lean4

/-- `single 1` as a `RingHom` -/
def singleOneRingHom : k →+* SkewMonoidAlgebra k G
    where
  __ := singleAddHom 1
  map_one' := rfl
  map_mul' x
    y := by
    simp [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, singleAddHom_apply, single_mul_single, mul_one, one_smul]

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