English
Let f: R → S be surjective and suppose R has a CommSemiring structure. If f preserves the ring operations, then S inherits a CommSemiring structure transported along f.
Русский
Пусть f: R → S — суръекция и R имеет CommSemiring-структуру. Если f сохраняет операции кольца, то S наследует CommSemiring-структуру, перенесённую по f.
LaTeX
$$$\text{Pushforward}_{f}({\text{CommSemiring}}\,R) = {\text{CommSemiring}}\,S.$$$
Lean4
/-- Pushforward a `CommSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev commSemiring [CommSemiring 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)
(npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : CommSemiring S
where
toSemiring := hf.semiring f zero one add mul nsmul npow natCast
__ := hf.commSemigroup f mul
