Semirings with monus

This file defines semirings with monus and introduces their main properties.

Many semirings relevant for provenance can be equipped with a monus - operator, resulting in what is called a semiring with monus, or m-semiring. This is standard in semiring theory [Ame84] and was introduced in the setting of provenance semirings by Geerts and Poggi [GP10].

References

• Amer, Equationally complete classes of commutative monoids with monus
• Geerts & Poggi, On database query languages for K-relations

Definition of a SemiringWithMonus

class SemiringWithMonus (α : Type) extends Semiring α, PartialOrder α, IsOrderedAddMonoid α, CanonicallyOrderedAdd α, Sub α : Type

A SemiringWithMonus is a naturally ordered semiring with a monus operation that is compatible with the natural order. We do not require the semiring to be necessarily commutative.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
• le_add_self (a b : α) : a ≤ b + a
• le_self_add (a b : α) : a ≤ a + b
• sub : α → α → α
• monus_spec (a b c : α) : a - b ≤ c ↔ a ≤ b + c

Main properties

theorem monus_smallest {α : Type} [K : SemiringWithMonus α] (a b : α) : a ≤ b + (a - b) ∧ ∀ (c : α), a ≤ b + c → a - b ≤ c

In a SemiringWithMonus, a - b is the smallest element c satisfying a ≤ b + c.

theorem monus_self {α : Type} [K : SemiringWithMonus α] (a : α) : a - a = 0

In a SemiringWithMonus, a - a = 0.

theorem zero_monus {α : Type} [K : SemiringWithMonus α] (a : α) : 0 - a = 0

In a SemiringWithMonus, 0 - a = 0.

theorem add_monus {α : Type} [K : SemiringWithMonus α] (a b : α) : a + (b - a) = b + (a - b)

In a SemiringWithMonus, a + (b -a) = b + (a - b).

theorem monus_add {α : Type} [K : SemiringWithMonus α] (a b c : α) : a - (b + c) = a - b - c

In a SemiringWithMonus, monus is left-distributive over plus.

Additional properties

The following properties do not always hold in an arbitrary m-semiring.

@[reducible, inline]

abbrev idempotent (α : Type u_1) [Semiring α] : Prop

A Semiring is idempotent if a + a = a.

Equations

• idempotent α = ∀ (a : α), a + a = a

@[reducible, inline]

abbrev absorptive (α : Type u_1) [Semiring α] : Prop

A Semiring is absorptive (also called 0-closed or 0-bounded) if 1 + a = a.

Equations

• absorptive α = ∀ (a : α), 1 + a = 1

@[reducible, inline]

abbrev mul_sub_left_distributive (α : Type) [SemiringWithMonus α] : Prop

We define left-distributivity of times over monus in a SemiringWithMonus.

Equations

• mul_sub_left_distributive α = ∀ (a b c : α), a * (b - c) = a * b - a * c

theorem idempotent_of_absorptive {α : Type u_1} [K : Semiring α] : absorptive α → idempotent α

Absorptivity implies idempotence

theorem le_iff_add_eq {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b : α) : a ≤ b ↔ a + b = b

In an idempotent SemiringWithMonus, a ≤ b iff a + b = b.

theorem plus_is_join {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b : α) : (a ≤ a + b ∧ b ≤ a + b) ∧ ∀ (u : α), a ≤ u ∧ b ≤ u → a + b ≤ u

In an idempotent SemiringWithMonus, plus is the join of the semilattice

theorem idempotent_of_add_monus {α : Type} [K : SemiringWithMonus α] (h : ∀ (a b c : α), a + b - c = a - c + (b - c)) : idempotent α

In a SemiringWithMonus, right-distributivity of monus over plus implies idempotence.

theorem add_monus_of_idempotent {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b c : α) : a + b - c = a - c + (b - c)

In a SemiringWithMonus, idempotence implies right-distributivity of monus over plus.

theorem idempotent_iff_add_monus {α : Type} [SemiringWithMonus α] : idempotent α ↔ ∀ (a b c : α), a + b - c = a - c + (b - c)

A SemiringWithMonus is idempotent iff monus is right-distributive over plus.

theorem monus_le {α : Type} [SemiringWithMonus α] (a b : α) : a - b ≤ a

theorem le_plus_monus {α : Type} [SemiringWithMonus α] (a b : α) : a ≤ b + (a - b)

Homomorphisms of SemiringWithMonuss

class SemiringWithMonusHom (α β : Type) [SemiringWithMonus α] [SemiringWithMonus β] extends α →+* β : Type

Definition of a homomorphism of SemiringWithMonuss

• toFun : α → β
• map_one' : (↑↑self.toRingHom).toFun 1 = 1
• map_mul' (x y : α) : (↑↑self.toRingHom).toFun (x * y) = (↑↑self.toRingHom).toFun x * (↑↑self.toRingHom).toFun y
• map_zero' : (↑↑self.toRingHom).toFun 0 = 0
• map_add' (x y : α) : (↑↑self.toRingHom).toFun (x + y) = (↑↑self.toRingHom).toFun x + (↑↑self.toRingHom).toFun y
• map_sub (x y : α) : self.toRingHom (x - y) = self.toRingHom x - self.toRingHom y

instance instCoeFunSemiringWithMonusHomForall (α β : Type) [SemiringWithMonus α] [SemiringWithMonus β] : CoeFun (SemiringWithMonusHom α β) fun (x : SemiringWithMonusHom α β) => α → β

Equations

• instCoeFunSemiringWithMonusHomForall α β = { coe := fun (f : SemiringWithMonusHom α β) (x : α) => f.toRingHom x }

theorem idempotent_of_injective_homomorphism_idempotent {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνi : Function.Injective fun (x : α) => ν.toRingHom x) : idempotent β → idempotent α

If ν is an injective m-semiring homomorphism from α to β, and β is idempotent, so is α.

theorem idempotent_of_surjective_homomorphism_idempotent {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνs : Function.Surjective fun (x : α) => ν.toRingHom x) : idempotent α → idempotent β

If ν is an m-semiring homomorphism from α onto β, and α is idempotent, so is β.

theorem mul_sub_left_of_injective_homomorphism_mul_sub_left {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνi : Function.Injective fun (x : α) => ν.toRingHom x) : mul_sub_left_distributive β → mul_sub_left_distributive α

If ν is an injective m-semiring homomorphism from α to β, and β has left-distributivity of times over monus, so has α.

theorem mul_sub_left_of_surjective_homomorphism_mul_sub_left {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνs : Function.Surjective fun (x : α) => ν.toRingHom x) : mul_sub_left_distributive α → mul_sub_left_distributive β

If ν is an m-semiring homomorphism from α onto β, and α has left-distributivity of times over monus, so has β.

Miscellaneous

class HasAltLinearOrder (α : Type u) : Type u

• altOrder : LinearOrder α