English
The map over a ring homomorphism induces a multiplicative structure: it is a monoid homomorphism from variable changes to variable changes over the target ring.
Русский
Отображение, проходящее через гомоморфизм колец, порождает гомоморфизм моноидной структуры между переменными смены переменных.
LaTeX
$$$$\mathrm{mapHom}: \text{VariableChange } R \to^* \text{VariableChange } A \quad\text{with}\quad \text{mapHom}(C_1) \cdot \text{mapHom}(C_2) = \text{mapHom}(C_1 \cdot C_2). $$$$
Lean4
/-- The map over a ring homomorphism of a change of variables is a group homomorphism. -/
def mapHom : VariableChange R →* VariableChange A
where
toFun := map φ
map_one' := by
simp only [one_def, map]
ext <;> simp only [map_one, Units.val_one, map_zero]
map_mul' C
C' := by
simp only [mul_def, map]
ext <;> map_simp <;> simp only [Units.coe_map, MonoidHom.coe_coe]
