English
If α has an IdemSemiring structure and f: β → α is injective with compatible structure-preserving maps, then β inherits an IdemSemiring structure by pulling back along f; f becomes an IdemSemiring homomorphism.
Русский
Если у α есть структура IdemSemiring, а f: β → α инъективна и сохраняет структуру, то β получает структуру IdemSemiring путём переносa вдоль f; при этом f является гомоморфизмом IdemSemiring.
LaTeX
$$$\exists\text{ IdemSemiring on } \beta \text{ such that } f: \beta \to \alpha \text{ is a homomorphism of IdemSemirings preserving }0,1,+,\cdot,\sqcup,\bot.$$$
Lean4
/-- Pullback an `IdemSemiring` instance along an injective function. -/
protected abbrev idemSemiring [IdemSemiring α] [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 ⊥ = ⊥) : IdemSemiring β :=
{ hf.semiring f zero one add mul nsmul npow natCast, hf.semilatticeSup _ sup,
‹Bot β› with
add_eq_sup := fun a b ↦ hf <| by rw [sup, add, add_eq_sup]
bot := ⊥
bot_le := fun a ↦ bot.trans_le <| @bot_le _ _ _ <| f a }
-- See note [reducible non-instances]
