English
If f: α → β preserves zero and maps algebraMap R α r to algebraMap R β r for all r ∈ R, then applying f entrywise to matrices commutes with algebraMap.
Русский
Если f сохраняет ноль и переводит algebraMap R α r в algebraMap R β r для всех r, то отображение по элементам матрицы сохраняет совместимость с algebraMap.
LaTeX
$$$(algebraMap R (Matrix n n α) r).map f = algebraMap R (Matrix n n β) r$ under suitable hf, hf₂$$
Lean4
@[simp]
theorem map_algebraMap (r : R) (f : α → β) (hf : f 0 = 0) (hf₂ : f (algebraMap R α r) = algebraMap R β r) :
(algebraMap R (Matrix n n α) r).map f = algebraMap R (Matrix n n β) r :=
by
rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]
simp [hf₂]
