English
Let f: S → R be injective. If R carries a NonUnitalNonAssocRing structure, then S can be equipped with a compatible NonUnitalNonAssocRing structure via pullback along f, with f preserving addition, multiplication, negation, and other ring operations as needed.
Русский
Пусть f: S → R инъективна. Если R имеет структуру NonUnitalNonAssocRing, можно задать на S совместную структуру через перенос по f, чтобы f сохранял сложение, умножение, отрицание и другие операции кольца.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{NonUnitalNonAssocRing}(S),\\quad f(0)=0,\\quad \\forall x,y, f(x+y)=f(x)+f(y),\\quad \\forall x,y, f(x\\cdot y)=f(x)\\cdot f(y),\\quad \\forall x, f(-x)=-f(x),\\quad \\forall x,y, f(x-y)=f(x)-f(y),\\quad \\forall n,x, f(n\\cdot x)=n\\cdot f(x),\\quad \\forall n,x, f(n\\cdot x)=n\\cdot f(x).$$$
Lean4
/-- Pullback a `NonUnitalNonAssocRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0)
(add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
(sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
(zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocRing S
where
toAddCommGroup := hf.addCommGroup f zero add neg sub (swap nsmul) (swap zsmul)
__ := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
