English
Let f: R → S be surjective and suppose R is equipped with a nonassociative ring structure. If f preserves the ring operations (addition, multiplication, negation, subtraction, as well as scalar actions and cast maps) and f(0)=0, f(1)=1, then S can be endowed with a compatible nonassociative ring structure transported along f. Analogous pushforwards hold for other ring-like structures (with or without units, and with various distributive or additive properties).
Русский
Пусть f: R → S — суръекция и R задано структурой немоноидного кольца. Если f сохраняет операции кольца (сложение, умножение, отрицание, вычитание, скаляры и приведения), и f(0)=0, f(1)=1, то S может быть наделено совместимой структурой немоноидного кольца, транспортированной по f. Аналогично существуют переносы и для других подобных структур.
LaTeX
$$$\text{Pushforward along } f\;:\; R\to S \text{ endows } S \text{ with a compatible NonAssocRing structure from } R.$$$
Lean4
/-- Pushforward a `NonAssocRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocRing [NonAssocRing 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) (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)
(natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocRing S
where
toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
__ := hf.nonAssocSemiring f zero one add mul nsmul natCast
__ := hf.addCommGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast
