English
If f: α → α₂ is a multiplicative homomorphism preserving the action, then mapDomain f is a ring homomorphism SkewMonoidAlgebra β α → SkewMonoidAlgebra β α₂.
Русский
Если f: α → α₂ — умножаемый гомоморфизм, сохраняющий действие, то mapDomain f является гомоморфизмом колец SkewMonoidAlgebra β α → SkewMonoidAlgebra β α₂.
LaTeX
$$$mapDomain\ f : SkewMonoidAlgebra(\beta,\alpha) \to SkewMonoidAlgebra(\beta,\alpha_2)$ устанавливает кольцевой гомоморфизм, если \forall a,x, a•x = f(a)•x$$$
Lean4
/-- Like `mapDomain_zero`, but for the `1` we define in this file -/
theorem mapDomain_one [MonoidHomClass F α α₂] (f : F) :
(mapDomain f (1 : SkewMonoidAlgebra β α) : SkewMonoidAlgebra β α₂) = (1 : SkewMonoidAlgebra β α₂) := by
simp_rw [one_def, mapDomain_single, map_one]
/- Like `mapDomain_add`, but for the skewed convolutive multiplication we define in this
file. This theorem holds assuming that `(hf : ∀ (a : α) (x : β), a • x = (f a) • x)`. -/
