repr_algebraMap — Mathlib

English

If B is a basis of the R-algebra S with B i = 1 for some i, then B.repr(algebraMap r) equals the singleton coordinate r at i.

Русский

Если B — базис R-алгебры S и B_i = 1 для некоторого i, то координаты B.repr(algebraMap r) равны единственному ненулевому координату r в i.

LaTeX

$$$$ B.repr(\text{algebraMap}_R^S(r)) = \mathrm{Finsupp}.single\ i\ r $$$$

Lean4

/-- If `B` is a basis of the `R`-algebra `S` such that `B i = 1` for some index `i`, then
each `r : R` gets represented as `s • B i` as an element of `S`. -/
theorem repr_algebraMap {ι : Type*} {B : Basis ι R S} {i : ι} (hBi : B i = 1) (r : R) :
    B.repr (algebraMap R S r) = Finsupp.single i r := by ext j; simp [Algebra.algebraMap_eq_smul_one, ← hBi]

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