English
Let R be a commutative semiring and A a semiring with an R-module structure. If (r • x) * y = x * (r • y) = r • (x * y) for all r ∈ R and x,y ∈ A, then A admits an Algebra structure over R; i.e., A becomes an R-algebra with the given compatibility.
Русский
Пусть R — коммутативное полугранство, A — полуринг с R-структурой модуля. Если выполняются условия совместимости (r • x) * y = x * (r • y) = r • (x * y) для всех r ∈ R и x,y ∈ A, тогда A становится алгеброй над R.
LaTeX
$$$\text{If } (r \cdot x) \cdot y = x \cdot (r \cdot y) = r \cdot (x \cdot y) \;\text{ for all } r,x,y, \text{ then } A \text{ has an } R\text{-algebra structure}.$$$
Lean4
/-- To prove two algebra structures on a fixed `[CommSemiring R] [Semiring A]` agree,
it suffices to check the `algebraMap`s agree.
-/
@[ext]
theorem algebra_ext {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] (P Q : Algebra R A)
(h :
∀ r : R,
(haveI := P;
algebraMap R A r) =
haveI := Q;
algebraMap R A r) :
P = Q := by
replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h
have h' :
(haveI := P;
(· • ·) :
R → A → A) =
(haveI := Q;
(· • ·) :
R → A → A) :=
by
funext r a
rw [P.smul_def', Q.smul_def', h]
rcases P with @⟨⟨P⟩⟩
congr
