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]. The class is the algebraic structure underlying the annotated query semantics of Section IV-A of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data (Definition 5).

References

• Amer, Equationally complete classes of commutative monoids with monus
• Geerts & Poggi, On database query languages for K-relations
• Sen, Maniu & Senellart, ProvSQL (Definition 5)

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.

In addition to monus, the class carries a δ : α → α operator subject to three axioms (delta_zero, delta_natCast_pos, and delta_absorb). This is the duplicate-eliminating support operator used to interpret aggregation in the framework of Amsterdamer, Deutch & Tannen, Provenance for aggregate queries, mirroring ProvSQL's Semiring::delta.

• zero : α
• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : α) : (n + 1) • x = n • x + x
• add_comm (a b : α) : a + b = b + a
• one : α
• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : α) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• 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
• delta : α → α

  Duplicate-eliminating support operator. Sends 0 to 0 and any positive integer iterate of 1 to 1.

• delta_zero : delta 0 = 0

  δ sends 0 to 0.

• delta_natCast_pos {n : ℕ} : 0 < n → delta ↑n = 1

  δ sends every positive integer iterate of 1 (i.e., every positive natural-number cast) to 1.

• delta_absorb (a b : α) : a * delta (a + b) = a

  A δ-guard is absorbed by any multiple of one of its summands: a ⊗ δ(a ⊕ b) = a. This is what makes a group-existence factor redundant next to any provenance that already contains an occurrence of the group: δ really acts as “the group exists” and nothing more. Both usual choices of δ satisfy it in their natural habitat: the indicator (δ x = 𝟙 for x ≠ 𝟘) in any canonically ordered semiring (delta_absorb_indicator), and the identity in lattice-like semirings, where it is absorption a ⊓ (a ⊔ b) = a.

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_unique {α : Type} [K : SemiringWithMonus α] (s : α → α → α) (hs : ∀ (a b c : α), s a b ≤ c ↔ a ≤ b + c) (a b : α) : s a b = a - b

Uniqueness of monus. The monus operation is determined by its adjunction property: any binary operation s satisfying s a b ≤ c ↔ a ≤ b + c coincides with ⊖. Consequently, a naturally ordered semiring admits at most one monus operation.

theorem delta_one {α : Type} [K : SemiringWithMonus α] : SemiringWithMonus.delta 1 = 1

In a SemiringWithMonus, δ 1 = 1.

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 monus_zero {α : Type} [K : SemiringWithMonus α] (a : α) : a - 0 = a

In a SemiringWithMonus, a - 0 = a.

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 = 1.

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

@[reducible, inline]

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

A SemiringWithMonus is exclusive when every element is orthogonal to what 𝟙 retains after removing it: a ⊗ (𝟙 ⊖ a) = 𝟘.

This is weaker than asking 𝟙 ⊖ a to be a complement of a, which would also require a ⊕ (𝟙 ⊖ a) = 𝟙: ℕ is exclusive, and there 𝟙 ⊖ 2 = 𝟘 joins with 2 to 2, not to 𝟙.

Exclusivity is what makes two distinct possible worlds of one occurrence family annihilate each other (worldAnn_mul_eq_zero_of_ne), hence what makes the alternatives of an occurrence exclude each other. It holds in Bool, BoolFunc, Nat, Which and IntervalUnion, and fails in How, Why, Viterbi, MinMax, Lukasiewicz, Tropical and ChainFive (the catalog theorems named exclusive and not_exclusive in Provenance.Semirings.*).

Those five are not five independent facts. Exclusivity is a unary equation, so it passes both to subalgebras and to the elements reached by a homomorphism out of an exclusive semiring. Bool and IntervalUnion inherit it from BoolFunc on those two routes: Bool embeds in BoolFunc as the constant functions (Bool.exclusive_of_boolFunc, by exclusive_of_injective_homomorphism_exclusive), while every interval union is the image of a variable under a homomorphism from BoolFunc (IntervalUnion.exclusive_of_boolFunc, by mul_one_monus_self_eq_zero_of_range – that homomorphism has a finite domain and is never onto, so the element-by-element form is what applies, not the surjective one). Nat and Which are beyond that reach, neither being absorptive (BoolFunc.no_hom_of_not_absorptive), and are exclusive for the other of the two reasons: their monus against 𝟙 collapses to 𝟘 rather than complementing.

Note that How – the universal semiring, in which provenance circuits are built – is not exclusive, so the terms exclusivity cancels are carried by a circuit and vanish only on evaluation into a semiring that has the property, homomorphisms commuting with ⊖.

Independence

Exclusivity is independent of each of the three properties above, every combination being realized in the catalog:

	exclusive	not exclusive
absorptive	Bool	Viterbi
not absorptive	Nat	How
idempotent	Bool	Why
not idempotent	Nat	How
mul_sub_left_distributive	Bool	Viterbi
not mul_sub_left_distributive	Which	Why

Independence is not absence of interaction: absorptivity and exclusivity constrain each other jointly without either implying the other, by eq_zero_or_one_of_exclusive_of_absorptive.

Equations

• exclusive α = ∀ (a : α), a * (1 - a) = 0

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 add_monus_of_idempotent_multiset {α : Type} [SemiringWithMonus α] (h : idempotent α) (s : Multiset α) (c : α) : s.sum - c = (Multiset.map (fun (x : α) => x - c) s).sum

Finite-family version of add_monus_of_idempotent: in an idempotent SemiringWithMonus, monus distributes over the sum of any multiset of annotations, (⨁ᵢ aᵢ) ⊖ c = ⨁ᵢ (aᵢ ⊖ c).

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

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

theorem monus_antitone {α : Type} [SemiringWithMonus α] {b b' : α} (h : b ≤ b') (a : α) : a - b' ≤ a - b

Monus is antitone in its second argument: subtracting more leaves less. Together with monus_le this is what lets a subtrahend be replaced by a larger one inside an upper bound.

Exclusivity

exclusive says a ⊗ (𝟙 ⊖ a) = 𝟘. The possible-world arguments consume a two-argument form, a ⊗ (𝟙 ⊖ (a ⊕ b)) = 𝟘: an occurrence present in one world and absent from another contributes a to the first world's annotation and 𝟙 ⊖ (a ⊕ b) to the second's. The two forms are equivalent, so the one-argument form is what a semiring is checked against and the two-argument form is what the proofs use.

theorem mul_le_mul_left_of_le {α : Type} [SemiringWithMonus α] {x y : α} (h : x ≤ y) (z : α) : z * x ≤ z * y

Multiplication is monotone: the order of a SemiringWithMonus is the natural one, so a larger factor differs from a smaller one by a summand that multiplication distributes over.

theorem mul_one_monus_add_eq_zero {α : Type} [SemiringWithMonus α] (h : exclusive α) (a b : α) : a * (1 - (a + b)) = 0

In an exclusive m-semiring an element is orthogonal to the complement of any sum containing it, not only of itself. Monus is antitone in its subtrahend, so the larger subtrahend a ⊕ b leaves a smaller complement than a does, and multiplication by a preserves that.

theorem exclusive_of_mul_one_monus_add {α : Type} [SemiringWithMonus α] (h : ∀ (a b : α), a * (1 - (a + b)) = 0) : exclusive α

The two-argument form is no stronger: exclusivity is its instance at b = 𝟘.

Exclusivity against absorptivity

An absorptive m-semiring has 𝟙 at the top of its natural order, so 𝟙 ⊖ a is the least element joining with a to 𝟙 – the least relative complement. Exclusivity then asks that least complement to be orthogonal to a, which a chain cannot deliver: there the join of two elements is one of them, so the only complement of a non-𝟙 element is 𝟙 itself.

theorem le_one_of_absorptive {α : Type} [SemiringWithMonus α] (h : absorptive α) (a : α) : a ≤ 1

In an absorptive semiring 𝟙 is the greatest element of the natural order.

theorem add_one_monus_eq_one_of_absorptive {α : Type} [SemiringWithMonus α] (h : absorptive α) (a : α) : a + (1 - a) = 1

In an absorptive m-semiring, 𝟙 ⊖ a joins with a to 𝟙; by monus_smallest it is the least element that does.

theorem one_join_irreducible_of_total {α : Type} [SemiringWithMonus α] (hidem : idempotent α) (htot : ∀ (a b : α), a ≤ b ∨ b ≤ a) (a z : α) (h : a + z = 1) : a = 1 ∨ z = 1

𝟙 is join-irreducible whenever addition is idempotent and the natural order is total: the sum is then the join of a chain, hence one of its two arguments.

theorem eq_zero_or_one_of_exclusive_of_absorptive {α : Type} [SemiringWithMonus α] (habs : absorptive α) (hirr : ∀ (a z : α), a + z = 1 → a = 1 ∨ z = 1) (hexcl : exclusive α) (a : α) : a = 0 ∨ a = 1

Absorptivity and exclusivity together are restrictive. If 𝟙 is join-irreducible – as it is in every absorptive m-semiring whose natural order is total – then an exclusive one has no element besides 𝟘 and 𝟙.

theorem not_exclusive_of_absorptive_of_total {α : Type} [SemiringWithMonus α] (habs : absorptive α) (htot : ∀ (a b : α), a ≤ b ∨ b ≤ a) {a : α} (h0 : a ≠ 0) (h1 : a ≠ 1) : ¬exclusive α

The contrapositive, in the form the catalog uses: a totally ordered absorptive m-semiring with an element other than 𝟘 and 𝟙 is not exclusive. This one argument covers Viterbi, MinMax, Lukasiewicz, Tropical and ChainFive.

Characteristic of idempotent semirings

In an idempotent semiring (a + a = a), every positive natural-number cast collapses to 1. With 1 ≠ 0 this yields CharP K 0. Note that this is strictly weaker than CharZero K, which fails for idempotent semirings since the cast ℕ → K is not injective.

theorem natCast_pos_eq_one_of_idempotent {K : Type} [Semiring K] (h : idempotent K) {n : ℕ} : 0 < n → ↑n = 1

In a semiring with idempotent addition, the cast of any positive natural number equals 1.

theorem CharP.zero_of_idempotent {K : Type} [Semiring K] [Nontrivial K] (h : idempotent K) : CharP K 0

A nontrivial idempotent semiring has characteristic 0 in the CharP sense. Unlike CharZero, this does not require the natural-number cast to be injective: in an idempotent semiring every positive natural maps to 1, but 1 ≠ 0 still suffices to give CharP K 0.

Generic constructions of δ

In the m-semirings used for provenance the δ operator is invariably realized in one of two ways: as the identity (when the semiring is idempotent, so every positive natural cast already equals 1) or as the indicator-of-nonzero (a ↦ if a = 0 then 0 else 1). The lemmas below package the proofs of the δ axioms for both candidates so each concrete instance can plug them in directly.

theorem delta_natCast_pos_id {K : Type} [Semiring K] (h : idempotent K) {n : ℕ} (hn : 0 < n) : id ↑n = 1

δ := id satisfies delta_natCast_pos in any idempotent semiring: every positive natural-number cast collapses to 1.

structure IsDeltaIndicator {K : Type} [Zero K] [One K] (δ : K → K) : Prop

The “indicator-of-nonzero” recipe: δ a = 0 when a = 0 and δ a = 1 otherwise. Captured abstractly so a single set of axioms can serve all the concrete instances that use it (ℕ, ℕ[X], Tropical, Viterbi, Lukasiewicz).

• zero : δ 0 = 0
• nonzero (a : K) : a ≠ 0 → δ a = 1

theorem delta_natCast_pos_indicator {K : Type} [Semiring K] [Nontrivial K] [CharP K 0] {δ : K → K} (h : IsDeltaIndicator δ) {n : ℕ} (hn : 0 < n) : δ ↑n = 1

Any δ matching the indicator recipe satisfies delta_natCast_pos in a nontrivial semiring of characteristic 0 (in the CharP sense): positive natural-number casts are nonzero, so δ sends them to 1.

theorem delta_absorb_indicator {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] {δ : K → K} (h : IsDeltaIndicator δ) (a b : K) : a * δ (a + b) = a

Any δ matching the indicator recipe satisfies delta_absorb in a canonically ordered semiring: if a ⊕ b = 𝟘 then a = 𝟘 by zero-sum freeness, and otherwise δ(a ⊕ b) = 𝟙.

Admissibility of a candidate δ

δ is not determined by the axioms, and the two operators used in practice are the identity and the support indicator. IsDelta states the axioms as a predicate on a candidate operator, so that a semiring can record which of the two it must use: the identity is preferred where it is admissible, and the indicator is forced exactly where ¬ IsDelta id holds. The three not_isDelta_id_of_* lemmas below cover the three ways the identity fails, in increasing order of subtlety.

structure IsDelta {K : Type} [Semiring K] (δ : K → K) : Prop

A candidate operator δ : K → K satisfies the δ-axioms of SemiringWithMonus.

• zero : δ 0 = 0

  δ sends 𝟘 to 𝟘.

• natCast_pos {n : ℕ} : 0 < n → δ ↑n = 1

  δ sends every positive natural-number cast to 𝟙.

• absorb (a b : K) : a * δ (a + b) = a

  A δ-guard is absorbed by any multiple of one of its summands.

theorem isDelta_delta {α : Type} [K : SemiringWithMonus α] : IsDelta SemiringWithMonus.delta

The δ carried by a SemiringWithMonus is admissible, by definition of the class. In particular, in a semiring whose instance takes δ := id this gives IsDelta id for free.

theorem not_isDelta_id_of_absorb_ne {K : Type} [Semiring K] {a b : K} (h : a * (a + b) ≠ a) : ¬IsDelta id

To refute δ := id, exhibit a pair violating the lattice absorption law a ⊗ (a ⊕ b) = a, which is what delta_absorb demands of the identity.

theorem not_isDelta_id_of_not_idempotent {K : Type} [Semiring K] (h : ¬idempotent K) : ¬IsDelta id

δ := id requires the semiring to be idempotent: delta_natCast_pos at n = 2 reads 𝟙 ⊕ 𝟙 = 𝟙, whence a ⊕ a = a ⊗ (𝟙 ⊕ 𝟙) = a. This is the crudest of the three obstructions, and the one that rules the identity out of the counting semirings (ℕ, ℕ[X]).

theorem not_isDelta_id_of_not_mul_idempotent {K : Type} [Semiring K] (hadd : idempotent K) (h : ¬∀ (a : K), a * a = a) : ¬IsDelta id

δ := id requires multiplicative idempotence as soon as addition is idempotent: delta_absorb at b = a reads a ⊗ (a ⊕ a) = a ⊗ a = a. This is the obstruction in the absorptive semirings whose ⊗ is a genuine product (Viterbi, Łukasiewicz), where the two coarser tests below say nothing.

theorem not_isDelta_id_of_not_absorptive {K : Type} [Semiring K] (h : ¬absorptive K) : ¬IsDelta id

δ := id requires absorptivity: delta_absorb at a = 𝟙 reads 𝟙 ⊗ (𝟙 ⊕ b) = 𝟙, i.e., 𝟙 ⊕ b = 𝟙.

Existence of a δ-like operator

This is the abstract counterpart of the SemiringWithMonus δ-axioms: we characterize, in an arbitrary nontrivial semiring (no order assumed), when a function δ : K → K satisfying δ 0 = 0 and δ ((n : K)) = 1 for 0 < n can exist. The class also demands delta_absorb, which the iff below ignores, so it should be read as a statement about how much of the ProvSQL δ interface is consistent with a given characteristic, not as a full existence proof for the class. (Constructing a witness for delta_absorb requires more structure: in a canonically ordered semiring the indicator works, see delta_absorb_indicator.)

theorem delta_exists_iff_charP_zero {K : Type} [Semiring K] [Nontrivial K] : (∃ (δ : K → K), δ 0 = 0 ∧ ∀ {n : ℕ}, 0 < n → δ ↑n = 1) ↔ CharP K 0

In any nontrivial semiring, a function δ : K → K satisfying δ 0 = 0 and δ ((n : K)) = 1 for every positive natural cast n exists if and only if K has characteristic 0 in the CharP sense. The forward direction follows because δ 0 = 0 and δ ((n : K)) = 1 are inconsistent when (n : K) = 0 for some 0 < n (it would force 0 = 1). The backward direction defines δ as the indicator of being nonzero.

Note that the δ operator is not uniquely determined by these axioms: they only pin its values on the image of ℕ. Two typical choices are δ as the indicator of being nonzero (δ x = if x = 0 then 0 else 1, used in the backward direction below) and, in an idempotent semiring, δ as the identity (since every positive natural cast then equals 1, see natCast_pos_eq_one_of_idempotent). Both are idempotent (δ (δ a) = δ a); adding idempotence as a third requirement would leave the statement unchanged, since the forward direction never uses it and the indicator witness satisfies it.

theorem isDelta_exists_of_natCast_axioms {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] [Nontrivial K] {δ : K → K} (h0 : δ 0 = 0) (hpos : ∀ {n : ℕ}, 0 < n → δ ↑n = 1) : ∃ (δ' : K → K), IsDelta δ'

The third axiom is free. In a canonically ordered semiring, a full IsDelta operator exists as soon as some function satisfies the first two axioms: the indicator witnessing delta_exists_iff_charP_zero satisfies delta_absorb as well (delta_absorb_indicator). So the admissibility question for a candidate δ is never one of existence – it is only about whether the preferred candidate, the identity, is among the admissible ones (not_isDelta_id_of_*).

theorem isDelta_exists_iff_charP_zero {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] [Nontrivial K] : (∃ (δ : K → K), IsDelta δ) ↔ CharP K 0

The companion of delta_exists_iff_charP_zero for the full axiom set: in a nontrivial canonically ordered semiring, an admissible δ exists if and only if the characteristic is 0.

Commutative SemiringWithMonuss

SemiringWithMonus is intentionally not assumed to be commutative; however, every provenance semiring used in this library is in fact commutative, and the algebraic identities that drive HAVING-style aggregate provenance (see Provenance.Having) require it. CommSemiringWithMonus packages a SemiringWithMonus together with the commutativity axiom, producing a CommMonoid instance whose Mul matches the one already supplied by SemiringWithMonus, so no Mul diamond appears when Finset.prod is used.

class CommSemiringWithMonus (K : Type) extends SemiringWithMonus K : Type

A SemiringWithMonus whose multiplication is commutative.

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

  Multiplication on K is commutative.

@[instance_reducible, instance 100]

instance instCommMonoidOfCommSemiringWithMonus {K : Type} [h : CommSemiringWithMonus K] : CommMonoid K

A CommSemiringWithMonus is automatically a CommMonoid, sharing its multiplicative structure with the underlying SemiringWithMonus. This makes Finset.prod usable without introducing a separate CommSemiring hypothesis that would cause a Mul diamond.

Equations

• instCommMonoidOfCommSemiringWithMonus = { toMonoid := h.toMonoid, mul_comm := ⋯ }

Homomorphisms of SemiringWithMonuss

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

Definition of a homomorphism of SemiringWithMonuss. Preserves the semiring structure (via RingHom), the monus (map_sub), and the δ operator (map_delta). The latter is required for hom commutation of the aggregation operator, where δ appears on the row-annotation column (Definition 7 / R5 of Sen, Maniu & Senellart).

• 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
• map_delta (a : α) : self.toRingHom (SemiringWithMonus.delta a) = SemiringWithMonus.delta (self.toRingHom a)

  The hom preserves δ: h (δ a) = δ (h a).

@[instance_reducible]

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 β.

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

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

theorem mul_one_monus_self_eq_zero_of_range {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hα : exclusive α) {x : β} (a : α) (ha : (fun (x : α) => ν.toRingHom x) a = x) : x * (1 - x) = 0

Exclusivity is a unary equation, so it holds of every element in the range of a homomorphism out of an exclusive m-semiring – surjectivity is not needed, one preimage of the element is enough.

This is what makes several entries of the exclusive column of the catalog forced rather than independent: wherever every element of a semiring is the image of a variable under some homomorphism from BoolFunc, exclusivity follows from BoolFunc.exclusive and nothing else (IntervalUnion.exclusive_of_boolFunc).

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

If ν is an m-semiring homomorphism from α onto β, and α is exclusive, so is β. Exclusivity passes to quotients as idempotence and distributivity do, being likewise an equation.

Miscellaneous

theorem natural_preorder_not_antisymm : ∃ (a : ℤ), ∃ (b : ℤ), (∃ (c : ℤ), b = a + c) ∧ (∃ (c : ℤ), a = b + c) ∧ a ≠ b

On an arbitrary semiring the natural relation a ≼ b ↔ ∃ c, b = a + c is always a preorder (reflexive by c = 0, transitive by adding witnesses) but not always antisymmetric: on ℤ, any two elements are related in both directions, e.g., 0 ≼ 1 ≼ 0 with 0 ≠ 1. This is why SemiringWithMonus assumes the canonically ordered structure instead of deriving an order from +.

class HasAltLinearOrder (α : Type u) : Type u

• altOrder : LinearOrder α

Home · Documentation · Publications · Contributors · Source · Cite