English
There is an induced Algebra structure on S coming from a RingHom i: R →+* S, provided the centrality condition holds; concretely, i toAlgebra' yields an Algebra R S.
Русский
Из RingHom i: R →+* S получаем алгебраическую структуру на S над R, если выполняется условие центрации; i.toAlgebra' задаёт Algebra R S.
LaTeX
$$$\text{Algebra'}(i,h):= \text{Algebra R S with } \text{algebraMap}=i,\ \text{smul } c\; x := i c \cdot x,$$$
Lean4
/-- Creating an algebra from a morphism to the center of a semiring.
See note [reducible non-instances].
*Warning:* In general this should not be used if `S` already has a `SMul R S`
instance, since this creates another `SMul R S` instance from the supplied `RingHom` and
this will likely create a diamond. -/
abbrev toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) : Algebra R S
where
smul c x := i c * x
commutes' := h
smul_def' _ _ := rfl
algebraMap := i
