coe_algebraMap — Mathlib

English

The canonical algebra map from k to MonoidAlgebra k G is given by first mapping into A and then embedding as the coefficient of 1 in the basis element for the identity of G.

Русский

Канонический алгебра-гомоморфизм из k в MonoidAlgebra k G задаётся как композиция отображения в A и затем внедрения в базисный элемент единицы G.

LaTeX

$$$\\mathrm{algebraMap}\\ k\\ (\\mathrm{MonoidAlgebra}\, k\\ G) = (\\mathrm{single}\\ 1) \\circ (\\mathrm{algebraMap}\\ k\\ A)$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_algebraMap {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    ⇑(algebraMap k (MonoidAlgebra A G)) = single 1 ∘ algebraMap k A :=
  rfl

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