English
Let f: T → R and g: R → S be ring homomorphisms. The construction that sends a matrix from the general linear group to the base ring via a RingHom is compatible with composition: applying g ∘ f is the same as first applying f and then g to every entry. Consequently, GL_n(T) maps to GL_n(S) functorially with respect to ring homomorphisms.
Русский
Пусть f: T → R и g: R → S — гомоморфизмы колец. Конструкция, которая отображает элемент из общеполной линейной группы в соответствующую матрицу над базовым кольцом через RingHom, совместима с композициями: применение g ∘ f по каждому элементу эквивалентно последовательному применению f затем g ко всем элементам. Следовательно, GL_n(T) отображается в GL_n(S энтовально по гомоморфизмам колец.
LaTeX
$$$\\mathrm{map}(g \\circ f) = \\mathrm{map}(g) \\circ \\mathrm{map}(f)$$$
Lean4
@[simp]
theorem map_comp (f : T →+* R) (g : R →+* S) : map (g.comp f) = (map g).comp (map (n := n) f) :=
rfl
