English
Let f: S → R be injective. If R carries a NonUnitalSemiring structure and f preserves zero, addition, multiplication, and natural-number scalar action, then S can be equipped with a compatible NonUnitalSemiring structure pulled back along f, so that f becomes a homomorphism of NonUnitalSemirings.
Русский
Пусть f: S → R инъективна. Если R имеет структуру NonUnitalSemiring и f сохраняет ноль, сложение, умножение и скалярное умножение по натуральным числам, то на S можно породить совместную структуру NonUnitalSemiring путём переноса через f, так что f будет гомоморфизмом NonUnitalSemiring.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{NonUnitalSemiring}(S),\\quad f(0)=0,\\quad \\forall x,y\\in S\\,(f(x+y)=f(x)+f(y)),\\quad \\forall x,y\\in S\\,(f(xy)=f(x)f(y)),\\quad \\forall n\\in\\mathbb{N},\\forall x\\in S\\,(f(n\\cdot x)=n\\cdot f(x)).$$$
Lean4
/-- Pullback a `NonUnitalSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalSemiring [NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
(mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalSemiring S
where
toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
__ := hf.semigroupWithZero f zero mul
