English
Let f: S → R be injective. If R has a NonAssocSemiring structure (with 0, 1, +, •, etc. as appropriate) and f preserves the relevant operations, then S can be endowed with a NonAssocSemiring structure pulled back along f, so that f is a homomorphism of NonAssocSemirings.
Русский
Пусть f: S → R инъективна. Если R обладает структурой NonAssocSemiring и f сохраняет соответствующие операции, то S может быть снабжён структурой NonAssocSemiring, переносимой через f, так что f является гомоморфизмом NonAssocSemirings.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{NonAssocSemiring}(S),\\quad \\text{zero}=f(0),\\quad \\text{add}:\\forall x,y, f(x+y)=f(x)+f(y),\\quad \\text{mul}:\\forall x,y, f(x*y)=f(x)f(y),\\quad \\text{nsmul}:\\forall n,x, f(n\\cdot x)=n\\cdot f(x),$$$
Lean4
/-- Pullback a `NonAssocSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocSemiring [NonAssocSemiring R] (zero : f 0 = 0) (one : f 1 = 1)
(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) (natCast : ∀ n : ℕ, f n = n) : NonAssocSemiring S
where
toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
__ := hf.mulZeroOneClass f zero one mul
__ := hf.addMonoidWithOne f zero one add nsmul natCast
