English
If α is IdemCommSemiring and f: β → α is injective with compatible data, then β inherits an IdemCommSemiring structure via pullback along f; f becomes an IdemCommSemiring morphism.
Русский
Если у α есть структура IdemCommSemiring и имеется инъекция f: β → α с совместимыми данными, то β получает структуру IdemCommSemiring путём переноса вдоль f; f становится гомоморфизмом IdemCommSemiring.
LaTeX
$$$\exists\text{ IdemCommSemiring on } \beta \text{ with } f: \beta \to \alpha \text{ a homomorphism preserving }0,1,+,\cdot,\sqcup,\bot.$$$
Lean4
/-- Pullback an `IdemCommSemiring` instance along an injective function. -/
protected abbrev idemCommSemiring [IdemCommSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β]
[Max β] [Bot β] (f : β → α) (hf : Injective f) (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) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
(bot : f ⊥ = ⊥) : IdemCommSemiring β :=
{ hf.commSemiring f zero one add mul nsmul npow natCast,
hf.idemSemiring f zero one add mul nsmul npow natCast sup bot with }
-- See note [reducible non-instances]
