English
Let f: R → S be surjective and suppose R has a NonUnitalNonAssocCommSemiring structure. If f preserves addition and multiplication and aligns scalar actions, then S inherits a NonUnitalNonAssocCommSemiring structure transported along f.
Русский
Пусть f: R → S — суръекция и R обладает структурой NonUnitalNonAssocCommSemiring. Если f сохраняет сложение и умножение и согласован с действием скаляров, то S наследует структуру NonUnitalNonAssocCommSemiring, переносимую по f.
LaTeX
$$$\text{Pushforward}_{f}({\text{NonUnitalNonAssocCommSemiring}}\,R) = {\text{NonUnitalNonAssocCommSemiring}}\,S.$$$
Lean4
/-- Pushforward a `NonUnitalNonAssocCommSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommSemiring [NonUnitalNonAssocCommSemiring 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) : NonUnitalNonAssocCommSemiring S
where
toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
__ := hf.commMagma f mul
