English
If R is a commutative semiring, A is a semiring with an R-module structure, and (h1) and (h2) hold relating r • 1 and multiplications, then A carries an Algebra R A structure with algebraMap given by r ↦ r • 1.
Русский
Если R — коммутативное полуринг, A — полуринг с R-структурой модуля и выполнены условия (h1),(h2), то A получает структуру Algebra R A с алгебраической картой r ↦ r • 1.
LaTeX
$$$\text{Algebra.ofModule'}(h_1,h_2):\ Algebra\ R\ A$ with $\text{algebraMap } r = r \cdot (1_A)$.$$
Lean4
/-- Let `R` be a commutative semiring, let `A` be a semiring with a `Module R` structure.
If `(r • x) * y = x * (r • y) = r • (x * y)` for all `r : R` and `x y : A`, then `A`
is an `Algebra` over `R`.
See note [reducible non-instances]. -/
abbrev ofModule [CommSemiring R] [Semiring A] [Module R A] (h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y))
(h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)) : Algebra R A :=
ofModule' (fun r x => by rw [h₁, one_mul]) fun r x => by rw [h₂, mul_one]
